Formal Mathematics Statement Curriculum Learning
Formal Mathematics Statement Curriculum LearningStanislas Polu1Jesse Michael Han1Kunhao Zheng2Mantas Baksys3Igor Babuschkin1Ilya Sutskever1AbstractWe explore the use of expert iteration in the con-text of language modeling applied to Formal math-ematics. We show that at same compute bud-get, expert iteration, by which we mean proofsearch interleaved with Learning , dramatically out-performs proof search only. We also observe thatwhen applied to a collection of Formal statementsof sufficiently varied difficulty, expert iteration iscapable of finding and solving a Curriculum of in-creasingly difficult problems, without the need forassociated ground-truth proofs. Finally, by apply-ing this expert iteration to a manually curated setof problem statements, we achieve state-of-the-arton theminiF2Fbenchmark, automatically solvingmultiple challenging problems drawn from highschool IntroductionDeep Learning has enjoyed spectacular success in many do-mains, including language (Brown et al.)
ment learning to formal mathematics unlikely to succeed. Past work proposed to address the infinite action space prob-lem by sampling from a language model (Polu & Sutskever, 2020). This paper focuses on this second problem and our basis for addressing it is the observation that the key role of self-play is to provide an unsupervised curriculum. We
Download Formal Mathematics Statement Curriculum Learning
Information
Domain:
Source:
Link to this page:
Please notify us if you found a problem with this document: