论文标题
正式的数学语句课程学习
Formal Mathematics Statement Curriculum Learning
论文作者
论文摘要
我们探讨了专家迭代在应用于形式数学的语言建模的背景下的使用。我们表明，在相同的计算预算，专家迭代中，我们的意思是证明搜索与学习交织在一起，仅优于证明搜索。我们还观察到，当应用于足够多种难度的正式陈述时，专家迭代能够找到和解决日益困难的问题的课程，而无需相关的基本真相证明。最后，通过将此专家迭代应用于手动策划的一组问题陈述，我们在Minif2F基准测试上实现了最先进的问题，从而自动解决了来自高中奥运会的多个挑战性问题。
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.
