BEGIN:VCALENDAR
VERSION:2.0
CALSCALE:GREGORIAN
PRODID:UW-Madison-Physics-Events
BEGIN:VEVENT
SEQUENCE:1
UID:UW-Physics-Event-6875
DTSTART:20220406T160000Z
DTEND:20220406T171500Z
DTSTAMP:20260414T152657Z
LAST-MODIFIED:20220324T193626Z
LOCATION:Chamberlin 5280 (Zoom link also available for online particip
 ants who signed up on our mailing list)
SUMMARY:Formal Mathematics Statement Curriculum Learning\, Physics ∩
  ML Seminar\, Stanislas Polu\, OpenAI
DESCRIPTION:We explore the use of expert iteration in the context of l
 anguage modeling applied to formal mathematics. We show that at same c
 ompute budget\, expert iteration\, by which we mean proof search inter
 leaved 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 findi
 ng and solving a curriculum of increasingly difficult problems\, witho
 ut 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 olympiad
 s.
URL:https://www.physics.wisc.edu/events/?id=6875
END:VEVENT
END:VCALENDAR