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

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