Goedel-Prover-V2：通过支架式数据合成与自我校正扩展形式化定理证明

Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction

August 5, 2025

作者: Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, Jiayun Wu, Jiri Gesi, Ximing Lu, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, Chi Jin

cs.AI

摘要

我们推出Goedel-Prover-V2系列开源语言模型，在自动定理证明领域树立了新的标杆。基于标准的专家迭代与强化学习流程，我们的方法融合了三大创新点：(1) 阶梯式数据合成：通过生成难度递增的合成任务，训练模型逐步掌握更复杂的定理；(2) 验证器引导的自我修正：利用Lean编译器的反馈，使模型能够迭代修正其证明；(3) 模型平均：合并模型检查点，以缓解训练后期模型输出多样性的下降。我们的轻量级模型Goedel-Prover-V2-8B在MiniF2F上达到了84.6%的pass@32成绩，以80倍小的规模超越了DeepSeek-Prover-V2-671B的同等指标。旗舰模型Goedel-Prover-V2-32B在标准模式下以88.1%的pass@32成绩，在自我修正模式下更是达到90.4%，大幅领先于之前的SOTA。此外，该旗舰模型在PutnamBench上以pass@184解决了86道问题，在开源模型排行榜上位居榜首，以显著更小的模型规模和计算预算，超越了DeepSeek-Prover-V2-671B以pass@1024解决47道问题的记录。Goedel-Prover-V2在发布之时（2025年7月至8月），在所有开源定理证明器中展现了最强的综合性能。在受限的测试计算预算下，它也跻身于包括公开报告性能的闭源系统在内的顶尖模型之列。我们的模型、代码及数据已发布于https://github.com/Goedel-LM/Goedel-Prover-V2。

English

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 leveraging feedback from the Lean compiler; (3) Model averaging: We merge model checkpoints to mitigate the decrease in model output diversity in later stages of training. Our small model, Goedel-Prover-V2-8B, reaches 84.6% pass@32 on MiniF2F and outperforms DeepSeek-Prover-V2-671B under the same metric, despite being 80X smaller. Our flagship model, Goedel-Prover-V2-32B, achieves 88.1% on MiniF2F at pass@32 in standard mode and 90.4% in self-correction mode, outperforming prior SOTA by a large margin. Additionally, our flagship model solves 86 problems on PutnamBench at pass@184, securing the first place among open-source models on the leaderboard, surpassing DeepSeek-Prover-V2-671B's record of solving 47 problems by pass@1024 with a significantly smaller model size and compute budget. At the time of its release (July-August 2025), Goedel-Prover-V2 achieves the strongest overall performance among all open-source theorem provers. It also ranks among the top-performing models--including closed-source systems with publicly reported performance--under a constrained test-time compute budget. Our models, code, and data are released at https://github.com/Goedel-LM/Goedel-Prover-V2.