新智元报道

编辑：桃子 好困

迄今为止最强大的开源定理证明器登场！Goedel-Prover-V2仅用8B参数击败671B的DeepSeek-Prover，并再次夺下数学PutnamBench冠军。十位核心贡献者，八大顶尖机构，让AI形式化证明再破纪录。

全球最强的开源「定理证明器」诞生了！

来自普林斯顿、清华、英伟达、斯坦福等八大顶尖机构联手，祭出了第二版Goedel-Prover-V2模型。

项目地址：https://blog.goedel-prover.com/

初代Goedel-Prover已被COLM 2025顶会录用，曾在miniF2F Pass@32刷新SOTA，位列PutnamBench榜首。

这一次，新版模型一共有两个参数版本：32B和8B。

历经数月迭代，Goedel-Prover-V2再次在PutnamBench上夺冠，用更少的算力，解决了64道数学难题。

而且，在IMO级别的基准——MathOlympiadBench，新模型刷爆SOTA，一举攻克了73个问题。

相比之下，DeepSeek-Prover-671B仅解决了50个问题。

另外，在汇集三大国际奥数竞赛难题的MiniF2F基准上，32B在Pass@32上拿下90.4%成绩，击败了DeepSeek-Prover-V2-671B（82.4%），8B模型与之实力相当。

它的出世，标志着AI又在在自动形式化证明生成领域实现了全新技术突破。

对此，有网友期待地表示，「当前，IMO 2025正在激烈比拼中，不知接下来Goedel-Prover-V2的实战表现如何」？

8B模型

一举击败671B DeepSeek Prover

目前，研究团队暂未放出arXiv论文。

不过，在项目主页和Hugging Face，对最新Goedel-Prover-V2模型背后技术和性能基准，展开了详实的介绍。

那么，小参数的模型是如何超越了671B？

这里，Goedel-Prover-V2以Qwen3‑8B 和Qwen3‑32B 作为基座模型，采用了标准的「专家迭代与强化学习」框架。

具体来说，研究团队在一个完整流程中——形式化问题、生成并验证证明，再利用新发现的正确证明训练下一代模型，并通过RL进一步提升性能。

接下来，他们还融入了三大创新技术：

1. 分层式数据合成（Scaffolded data synthesis）

生成难度逐步递增的合成证明任务，对模型进行渐进式训练，使其能够掌握愈发复杂的定理；

自动生成介于已解决简单问题与未解复杂问题之间的中级难度题目，形成更平滑的难度递进，为训练提供更密集、信息量更高的信号。

2. 验证器引导的自我修正（Verifier-guided self-correction）

训练模型有效利用 Lean 编译反馈，反复修订自身证明，高度模拟人类完善证明的过程，并将这一任务融入监督微调与强化学习阶段。

3. 模型平均（Model averaging）

为防止后期训练导致多样性丧失，将已训练的检查点与基座模型进行平均。

这一简洁技术能够恢复多样性，并在更大的 K 值下显著提升 Pass@K 表现。

简言之，融合多个模型检查点，提升鲁棒性与整体性能。

极少算力刷爆SOTA，Scaling超强

Goedel-Prover-V2首先会生成一个初始候选证明，再借助 Lean 编译器的反馈进行迭代修正，以提高证明质量。

研究中，模型进行了两轮自我修正，但计算开销依然可控——总输出长度（包含初始证明及两次修正）仅从标准的 32K  token适度增加到40K  token。

如下表所示，展示了Goedel-Prover-V2在Pass@32下的所有结果。

首先，在全部三个数据集中，旗舰32B 模型均显著超越此前SOTA模型，即DeepSeek‑Prover‑V2‑671B与Kimina‑Prover‑72B。

其次，在miniF2F数据集上，8B模型在性能上与DeepSeek‑Prover‑V2‑671B相当，但模型规模仅为其 1/100。

如下成绩是，Goedel-Prover-V2在PutnamBench基准上，用更少的算力，击败所有SOTA位居榜首。

下面的Scaling曲线表明，在整个推理计算范围内，Goedel-Prover-V2-32B始终优于所有的顶尖模型。

也就意味着，新模型具备了出色的Scaling能力。

论文核心贡献者之一Chi Jin称，Goedel-Prover只用了高校实验室里的GPU，就实现了超强性能。

十位核心作者，清北上交在列

Yong Lin

Yong Lin是普林斯顿大学语言与智能（PLI）的博士后研究员，导师是Chi Jin、Sanjeev Arora和Danqi Chen。

此前，他在香港科技大学获得博士学位，师从张潼教授；在浙江大学获得学士和硕士学位，专业排名1/207。

在攻读博士学位之前，他于2017年至2021年在阿里担任高级机器学习工程师。

他的研究聚焦于机器学习和LLM的后训练技术。主要研究方向包括：

形式化数学推理：让大语言模型能够使用可验证的语言（即形式化语言，如 LEAN）进行推理。

LLM后训练：提升模型的有益性、无害性与诚实性等特质。

Shange Tang

Shange Tang是普林斯顿大学运筹学与金融工程系的博士生，导师是Jianqing Fan教授与金驰教授。

此前，他在北京大学数学科学学院获得学士学位。

他的研究兴趣为统计学和机器学习的理论与应用。

Bohan Lyu

Bohan Lyu目前在普林斯顿大学PLI，从事基于大语言模型与形式化语言的自动化数学定理证明研究，师从金驰教授。

此前，他在清华大学获得学士学位。并曾在清华大学NLP实验室（导师是刘知远教授）和加州大学圣地亚哥分校Rose-STL-Lab（导师是虞琦教授）进行科研实习。

他的研究兴趣为机器学习（ML）和自然语言处理（NLP）。

Ziran Yang（杨子然）

杨子然是普林斯顿大学电子与计算机工程系的博士生，师从金驰教授。

此前，他在北京大学元培学院获得学士学位，到时是朱毅鑫教授、朱松纯教授。

Jui-Hui Chung（钟瑞辉）

钟瑞辉是普林斯顿大学应用与计算数学项目的博士生，师从Jacob Shapiro教授。

他本科及硕士毕业于台湾大学物理系，师从Ying-Jer Kao教授，期间主要从事计算物理研究。

他的研究方向是拓扑绝缘体的数学物理特性。近期在Chi Jin教授指导下，开展基于LLM的自动定理证明研究。

Haoyu Zhao

Haoyu Zhao是普林斯顿大学的博士生，师从Sanjeev Arora教授。

此前，他在清华大学计算机科学实验班（姚班）获得学士学位，导师是陈卫教授。

他的研究兴趣横跨数学、算法与学习的交叉领域。

Lai Jiang

上海交通大学。

Yihan Geng

北京大学。

Hongzhou Lin

Hongzhou Lin是亚马逊应用研究科学家，隶属于AGI基础团队。

此前，他在法国INRIA格勒诺布尔中心获得了博士学位，师从Zaid Harchaoui和Julien Mairal教授。期间，他首创了一阶优化算法的通用加速框架，为后续应用科学研究奠定了重要理论基础。

随后在MIT的Stefanie Jegelka教授指导下完成机器学习方向的博士后研究。

目前，他主要从事LLM开发工作，专注于数学推理与问题解决能力的研究，涵盖非形式化与形式化（如LEAN）两大方向。

Chi Jin（金驰）

金驰是普林斯顿大学电气与计算机工程学系助理教授，计算机科学系联合聘任教员。

此前，他在加州大学伯克利分校获得计算机科学博士学位，在北京大学获得物理学学士学位。

他的研究方向包括，大模型推理与智能体、博弈论与多智能体学习、强化学习、统计学习理论、优化方法。

参考资料：

https://blog.goedel-prover.com/