新一代开源数学定理证明模型Goedel-Prover-V2发布，性能超越前代SOTA

近日，由普林斯顿大学牵头，联合清华大学、北京大学、上海交通大学、斯坦福大学及英伟达、亚马逊、Meta FAIR等机构的研究团队正式发布新一代开源数学定理证明模型Goedel-Prover-V2。该模型在自动化数学定理证明领域取得突破性进展，其32B参数版本在多个核心基准测试中显著超越此前最优开源模型DeepSeek-Prover-V2-671B。

技术性能方面，32B旗舰模型在MiniF2F测试集的Pass@32指标上正确率提升8.0%，8B精简版则在特定任务中与671B规模的DeepSeek-Prover-V2表现相当。值得注意的是，新模型在PutnamBench数学竞赛题库中成功解决64道难题，并在国际数学奥林匹克级别的MathOlympiadBench基准上攻克73个问题，较前代SOTA模型DeepSeek-Prover-V2多解决23题。

该模型采用专家迭代训练方法，通过将自然语言数学命题转化为Lean 4等形式化语言，有效缓解了形式化证明数据稀缺的挑战。项目已开源32B和8B双版本模型权重，用户可通过HuggingFace平台获取。初代Goedel-Prover研究成果此前已被COLM 2025顶会收录。

此次发布标志着开源社区在形式化数学推理领域取得重要突破，其小参数模型展现的高效特性，为数学教育辅助工具和科研验证系统的开发提供了新的技术路径。研究团队表示，将持续优化模型在复杂数学命题中的泛化能力。