Goedel Prover V2——由普林斯顿、清华等联合开发的开源定理证明模型

2 0 0

Goedel-Prover-V2：引领数学定理证明的新一代开源工具

Goedel-Prover-V2是由全球顶尖学府普林斯顿大学、清华大学以及科技巨头英伟达等机构联合推出的最新开源定理证明器。这款工具通过创新的分层式数据合成技术、验证器引导的自我修正机制和模型平均策略，显著提升了自动形式化证明生成的效率和质量。

Goedel-Prover-V2提供两种参数规模的版本：32B和8B，分别在不同性能级别上实现了高效的证明生成。其中，32B模型在MiniF2F基准测试中以90.4%的Pass@32成绩超越了671B的DeepSeek-Prover-V2，展现出卓越的推理能力。此外，在PutnamBench和MathOlympiadBench等权威测试中，Goedel-Prover-V2均取得了优异的成绩，进一步巩固了其在数学定理证明领域的领先地位。

这一突破性的工具不仅为AI在数学研究中的应用树立了新的标杆，更为学术界和工业界提供了强大的技术支持。

Goedel-Prover-V2的核心优势

智能自动生成证明： 能够为复杂的数学问题生成严谨的形式化证明，显著提升数学研究的效率。
自我优化与学习： 通过集成Lean编译器的反馈机制，模型能够持续改进自身的证明过程，不断接近人类专家的推理水平。
高效训练与优化： 创新的分层式数据合成和模型平均技术，不仅提升了训练效率，还显著增强了模型在不同复杂度任务上的表现稳定性。
开源协作与扩展性： 提供全面的开源模型和丰富的数据集资源，为全球研究者提供了便捷的研究平台，推动数学定理证明技术的持续进步。

Goedel-Prover-V2的技术创新

分层式数据合成（Scaffolded Data Synthesis）： 通过自动生成难度逐步递增的训练任务，帮助模型循序渐进地掌握从简单到复杂的证明技巧。这种策略填补了不同难度层级之间的空白区域，提供了更为密集和有针对性的训练信号。
验证器引导的自我修正（Verifier-Guided Self-Correction）： 模型在生成证明的过程中，会实时接收来自Lean编译器的反馈信息。基于这些反馈，模型能够不断调整和优化自身的推理策略，模拟人类专家完善证明的过程。
模型平均（Model Averaging）： 通过整合不同训练阶段的多个模型参数，保持了模型预测结果的多样性。这种方法在较大的Pass@K值场景下表现尤为突出，显著提升了整体性能和系统的鲁棒性。

Goedel-Prover-V2的性能表现

Goedel-Prover-V2在多个权威基准测试中展现了卓越的能力：

MiniF2F 基准测试：
- 32B模型：
  - Pass@32：达到90.4%，远超DeepSeek-Prover-V2-671B的82.4%。
  - 自校正模式下，Pass@32成绩同样保持在90.4%。
- 8B模型：
  - Pass@32：达到83.3%，与DeepSeek-Prover-V2-671B的82.4%不相上下，但模型规模却小了近100倍。
PutnamBench 基准测试：
- 32B模型：
  - Pass@64：解决64个问题，位居第一。
  - Pass@32：解决了57个问题，显著优于DeepSeek-Prover-V2-671B的47个问题。
- 8B模型：
  - Pass@32：表现同样出色，与DeepSeek-Prover-V2-671B相当。
MathOlympiadBench 基准测试：
- 32B模型：解决73个问题，显著优于DeepSeek-Prover-V2-671B的50个问题。
- 8B模型：表现也非常接近，展现出强大的定理证明能力。