Formal Mathematics Statement Curriculum Learning
Stanislas Polu Jesse Michael Han Kunhao Zheng Mantas Baksys Igor Babuschkin Ilya Sutskever
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.
中文速览
形式化数学证明长期面临"搜索空间无限大"和"没有对手可以自我对弈"两大难题，这项研究提出用「专家迭代（expert iteration）」来突破第二个瓶颈：让语言模型反复进行证明搜索，把搜索中成功找到的证明作为新训练数据来迭代提升模型，如此循环往复。研究者还发现，只要给模型提供一批难度参差不齐的数学命题（无需附带答案证明），专家迭代就能自动形成一条"由易到难"的课程，逐步攻克更难的问题。在相同算力预算下，这种"搜索+学习"交替进行的方式远胜于单纯的证明搜索，最终在衡量数学竞赛题形式化证明能力的 miniF2F 基准测试上刷新了最优成绩，甚至自动证明了多道高中奥林匹克竞赛题。这项工作表明，让 AI 在形式化数学中持续自我进化，关键在于构建足够多样的命题集合，为未来通过自动化手段大规模生成此类命题、进一步提升数学推理能力奠定了基础。
原文 arXiv:2202.01344;中英对照 + 大白话阅读 https://aha.fim.ai/paper/2202.01344v1