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

我们推出了Goedel-Prover-V2，这是一系列开源语言模型，在自动定理证明领域树立了新的最先进水平。我们的方法基于标准的专家迭代和强化学习流程，融合了三项关键创新：（1）支架式数据合成——我们生成难度递增的合成任务，以训练模型掌握日益复杂的定理；（2）验证器引导的自我修正——我们利用Lean编译器的反馈，使模型能够迭代修改其证明；（3）模型平均——我们合并模型检查点，以缓解训练后期模型输出多样性下降的问题。我们的小型模型Goedel-Prover-V2-8B在MiniF2F上的pass@32指标达到84.6%，在相同指标下表现优于DeepSeek-Prover-V2-671B，尽管其规模仅为后者的1/80。我们的旗舰模型Goedel-Prover-V2-32B在标准模式下MiniF2F的pass@32得分为88.1%，在自我修正模式下达到90.4%，大幅超越了之前的最先进水平。此外，该旗舰模型在PutnamBench测试中pass@184解决了86个问题，在排行榜上位列开源模型首位，超过了DeepSeek-Prover-V2-671B在pass@1024下解决47个问题的记录，同时使用的模型规模和计算资源显著更少。在发布之时（2025年7月至8月），Goedel-Prover-V2在所有开源定理证明系统中实现了最强的综合性能。即使在有限的测试计算预算下，它也跻身表现最佳的模型之列，包括那些公开报告性能的闭源系统。我们的模型、代码和数据已发布在https://github.com/Goedel-LM/Goedel-Prover-V2。

这篇论文旨在解决自动定理证明（Automated Theorem Proving, ATP）中的核心挑战：如何在有限的计算资源下，提升语言模型在形式化数学推理任务中的性能与泛化能力。具体目标包括提高模型在MiniF2F和PutnamBench等权威数学推理基准上的证明通过率（pass@k），同时控制模型规模和训练成本。这是一个持续受到关注的问题，但论文通过结合多种创新策略，在开源模型中首次达到接近甚至超过闭源系统的性能，具有显著的新颖性和实际意义。

论文提出Goedel-Prover-V2，基于标准的专家迭代和强化学习流程，引入三项关键技术：(1) 分层任务合成（Scaffolded data synthesis）：生成难度递增的合成任务，逐步训练模型掌握复杂定理；(2) 编译器反馈驱动的自修正机制（Verifier-guided self-correction）：利用Lean编译器反馈迭代优化证明过程；(3) 模型集成策略（Model averaging）：融合多个训练阶段的检查点，缓解后期训练中输出多样性下降的问题。这些方法的组合在开源模型中实现了显著的性能突破，尤其在模型规模远小于竞品的情况下。

1. Goedel-Prover-V2-8B在MiniF2F上以84.6%的pass@32超越了DeepSeek-Prover-V2-671B，尽管后者规模大80倍 2. 旗舰模型Goedel-Prover-V2-32B在标准模式下pass@32达到88.1%，自修正模式下提升至90.4% 3. 在PutnamBench上，Goedel-Prover-V2-32B以pass@184解出86题，远超DeepSeek-Prover-V2-671B的47题（pass@1024） 4. 模型、代码和数据均已开源，发布于GitHub（https://github.com/Goedel-LM/Goedel-Prover-V2） 5. 在受限的测试计算预算下，表现优于包括闭源系统在内的多数模型 6. 未来可探索将模型迁移到其他形式化验证任务或结合更多交互式定理证明系统

1. DeepSeek-Prover-V2 (2024): 基于大规模语言模型的自动定理证明系统，曾为开源模型中的SOTA 2. AlphaProof (2024): DeepMind提出的基于强化学习的自动定理证明系统 3. LeanChat & ProofNet (2023): 探索基于语言模型的交互式定理证明与数据增强方法 4. MetaMath: 用于数学推理的预训练语言模型，强调形式化数学语料库的应用 5. HellasWard & Isabelle/ML (2024): 针对交互式定理证明环境的模型增强与集成研究