Formal Mathematics Statement Curriculum Learning
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor, Babuschkin, Ilya Sutskever

TL;DR
This paper demonstrates that expert iteration, combining proof search with learning, significantly improves formal mathematics problem solving, enabling curriculum learning and achieving state-of-the-art results on challenging benchmarks.
Contribution
It introduces expert iteration for formal mathematics, showing its effectiveness in curriculum learning and surpassing previous methods on the miniF2F benchmark.
Findings
Expert iteration outperforms proof search alone at the same compute budget.
It enables curriculum learning over a range of problem difficulties.
Achieves state-of-the-art results on miniF2F, solving high school olympiad problems.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
First Author Interview: AI & formal math (Formal Mathematics Statement Curriculum Learning)· youtube
OpenAI tackles Math - Formal Mathematics Statement Curriculum Learning (Paper Explained)· youtube
[ML News] DeepMind AlphaCode | OpenAI math prover | Meta battles harmful content with AI· youtube
Taxonomy
TopicsNatural Language Processing Techniques · Mathematics, Computing, and Information Processing · Topic Modeling
