BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//CMSA - ECPv6.17.1//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:CMSA
X-ORIGINAL-URL:https://cmsa.fas.harvard.edu
X-WR-CALDESC:Events for CMSA
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:America/New_York
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20210314T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20211107T060000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20220313T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20221106T060000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20230312T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20231105T060000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/New_York:20220323T140000
DTEND;TZID=America/New_York:20220323T150000
DTSTAMP:20240515T202339Z
CREATED:20230808T183247Z
LAST-MODIFIED:20240515T202339Z
UID:10001208-1648044000-1648047600@cmsa.fas.harvard.edu
SUMMARY:Formal Mathematics Statement Curriculum Learning
DESCRIPTION:Speaker: Stanislas Polu\, OpenAI \nTitle: Formal Mathematics Statement Curriculum Learning \nAbstract: We explore the use of expert iteration in the context of language modeling applied to formal mathematics. We show that at same compute budget\, expert iteration\, by which we mean proof search interleaved with learning\, dramatically outperforms proof search only.  We also observe that when applied to a collection of formal statements of sufficiently varied difficulty\, expert iteration is capable of finding and solving a curriculum of increasingly difficult problems\,  without the need for associated ground-truth proofs. Finally\, by applying this expert iteration to a manually curated set of problem statements\, we achieve state-of-the-art on the miniF2F benchmark\,  automatically solving multiple challenging problems drawn from high school olympiads.
URL:https://cmsa.fas.harvard.edu/event/3-23-2022-new-technologies-in-mathematics-seminar/
LOCATION:MA
CATEGORIES:New Technologies in Mathematics Seminar
ATTACH;FMTTYPE=image/jpeg:https://cmsa.fas.harvard.edu/media/CMSA-NTM-Seminar-03.23.2022-1553x2048-1.jpg
END:VEVENT
END:VCALENDAR