Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction
Yong Lin and Shange Tang and Bohan Lyu and Ziran Yang and Jui-Hui Chung and Haoyu Zhao and Lai Jiang and Yihan Geng and Jiawei Ge and Jingruo Sun and Jiayun Wu and Jiri Gesi and Ximing Lu and David Acuna and Kaiyu Yang and Hongzhou Lin and Yejin Choi and Danqi Chen and Sanjeev Arora and Chi Jin
我们推出Goedel-Prover-V2系列开源语言模型，在自动定理证明领域创造了新的技术标杆。基于标准的专家迭代和强化学习流程，我们的方法包含三项关键创新：(1)支架式数据合成：通过生成难度递增的合成任务，训练模型掌握日益复杂的定理；(2)验证器引导的自我校正：利用Lean编译器的反馈使模型能够迭代修正其证明；(3)模型平均：合并模型检查点以缓解训练后期模型输出多样性的下降。我们的小型模型Goedel-Prover-V2-8B达到了84.6
We introduce Goedel-Prover-V2, a series of open-source language models that set a new state-of-the-art in automated theorem proving. Built on the standard expert iteration and reinforcement learning pipeline, our approach incorporates three key innovations: (1) Scaffolded data synthesis: We generate synthetic tasks of increasing difficulty to train the model to master increasingly complex theorems; (2) Verifier-guided self-correction: We enable the model to iteratively revise its proofs by lever...