Formal Mathematics Statement Curriculum Learning
This work addresses the challenge of automated theorem proving in formal mathematics, offering a method that can learn and solve increasingly difficult problems without ground-truth proofs, though it is incremental in its application to a specific domain.
The paper tackled the problem of applying language models to formal mathematics by introducing expert iteration, which interleaves proof search with learning, and demonstrated that this approach outperforms proof-search-only methods at the same compute budget, achieving state-of-the-art results on the miniF2F benchmark by automatically solving multiple challenging high school olympiad problems.
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.