Formal Mathematics Statement Curriculum Learning
Stanislas Polu, OpenAIAbstract:
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.