世界上最强大的开源“定理鄙分”已经诞生了！

来自普林斯顿，Tsinghua，Nvidia，Stanford和其他主要组织的八个顶级机构已联手推出了Goedel-Prover-V2模型的第二版。

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

第一代Goedel-Prover已被Colm 2025 Top Club雇用，并在Minif2F Pass@32刷新了Sota，在Putnambench中排名第一。

这次，该模型的新版本中有两个参数版本：32B和8B。

经过几个月的迭代，Goedel-Prover-V2再次在Putnambench上赢得了冠军，使用较少的计算能力来解决64个数学问题。

此外，在IMO级别的基准3—— Matholympiadbench中，新型模型击败了Sota并克服了73个问题。

相反，DeepSeek-Prover-671b仅解决了50个问题。

此外，在汇集了三个主要国际奥林匹克竞赛问题的Minif2F基准上，32B在Pass@32上得分90.4，击败了DeepSeek-Prover-V2-671b（82.4），而8B模型则与之相当。

它在自动正式证明生成领域取得了新的技术突破。

为此，一些网民表达了人们的表达：“目前，IMO 2025处于激烈的竞争中。我想知道将来Goedel-Prover-V2的实际表现如何”？

8B型号

击败671B DeepSeek称者一口气

目前，研究小组尚未发布Arxiv论文。

但是，在最新的Goedel-Prover-V2模型背后的技术和性能基准的详细介绍中，在项目主页和拥抱面孔上进行了详细的介绍。

那么，小参数模型如何超过671b？

在这里，Goedel-Prover-V2使用Qwen3-8b和Qwen3-32b作为基本模型，并采用了标准的“专家迭代和增强学习”框架。

具体而言，研究团队在完整的过程中正式化了该问题，生成和验证证明，然后使用新发现的正确证明来训练下一代模型，并通过RL进一步提高性能。

接下来，他们还结合了三种创新技术：

1。脚手架数据合成

生成综合证明任务，逐渐增加难度，并在模型上进行逐步训练，以便它可以掌握日益复杂的定理；

自动在解决的简单问题和未解决的复杂问题之间会自动产生中间的难题，形成更平滑的渐进难度，从而提供更密集和更有信息的信号。

2。验证者引导的自我纠正

培训模型有效地使用了精益汇编反馈，反复修改了自己的证据，高度模拟了人类完善证明的过程，并将这项任务纳入监督的微调和强化学习阶段。

3。平均模型

为了防止晚期训练中的多样性丧失，训练有素的检查站与基座模型平均。

这项简化的技术恢复了多样性，并在更大的K值下显着改善了通过@K性能。

简而言之，多个模型检查点已集成以提高鲁棒性和整体性能。

很少有计算能力击败SOTA，缩放是超级强大的

Goedel-Prover-V2将首先生成初始候选证明，然后使用精益编译器的反馈进行迭代校正，以提高证明的质量。

在研究期间，该模型进行了两轮自校正，但计算开销仍然是可控制的。总输出长度（包括初始证明和两个校正）从标准的32K代币略有增加到40k令牌。

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

首先，在所有三个数据集中，旗舰32B模型都显着超过了先前的SOTA模型，即DeepSeek -Prover -V2 671B和Kimina -Prover -72b。

其次，在Minif2F数据集上，8B模型在性能中与DeepSeek -Prover -V2-671B相当，但模型大小仅为其大小的1/100。

以下结果是Goedel-Prover-V2在Putnambench基准上以较少的计算能力击败了所有SOTA。

下面的缩放曲线显示，Goedel-Prover-V2-32B在整个推理计算范围内总是优于所有顶级模型。

这意味着新模型具有出色的缩放功能。

该论文的核心贡献者之一Chi Jin说，Goedel-Prover仅在大学实验室中使用GPU来实现超级绩效。

Yong Lin

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

之前，他获得了博士学位。来自香港科学技术大学，在张教教授的领导下学习；并获得了他的学士学位和硕士学位，并获得了1/207的主要排名。

在获得博士学位之前，他从2017年到2021年在阿里巴巴担任高级机器学习工程师。

他的研究重点是LLM的机器学习和培训后技术。主要研究指示包括：

正式的数学推理：使大型语言模型能够使用可验证的语言（即形式语言，例如精益）进行推理。训练后培训：改善模型的好处，无害和诚实。

Shange Tang

Shang Tang是普林斯顿大学运营研究与金融工程系的博士生。他的主管是Jianqing教授和Jin Chi教授。

以前，他获得了北京大学数学科学学院的学士学位。

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

Bohan Lyu

Bohan Lyu目前在普林斯顿大学PLI上，根据大语言模型和形式语言进行了自动数学定理的证明，并根据Jin Chi教授进行了研究。

此前，他获得了Tsinghua大学的学士学位。他还曾在Tsinghua大学的NLP实验室（主管是Liu Zhiyuan教授）和加利福尼亚大学圣地亚哥分校的Rose-STL-LAB（主管是Yu Qi教授）。

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

Ziran Yang（杨子然）

Yang Ziran是普林斯顿大学电子和计算机工程系的博士生，并在Jin Chi教授的领导下进行了研究。

此前，他获得了北京大学Yuanpei学院的学士学位，然后是朱Yixin教授和Zhu Songchun教授。

Jui-Hui Chung（钟瑞辉）

Zhong Ruihui是普林斯顿大学应用和计算数学课程的博士生，在Jacob Shapiro教授的领导下学习。

他毕业于台湾大学物理学系，并获得了本科和硕士学位，并在Ying-Jer Kao教授的领导下学习。在他的期间，他主要从事计算物理学的研究。

他的研究方向是拓扑绝缘子的数学和物理特性。最近，在Chi Jin教授的指导下，进行了基于LLM的自动定理研究。

Haoyu Zhao

Haoyu Zhao是普林斯顿大学的博士生，在Sanjeev Arora教授的领导下学习。

此前，他获得了Tsinghua University的计算机科学实验课（YAO课）的学士学位，他的导师是Chen Wei教授。

他的研究兴趣跨越了数学，算法和学习的交集。

Lai Jiang

上海Jiaotong大学。

Yihan Geng

北京大学。

洪林

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

此前，他从法国的Inria Grenoble中心获得了博士学位，在那里他在Zaid Harchaoui教授和Julien Mairal的领导下学习。在此期间，他开创了一阶优化算法的一般加速框架，为随后的应用科学研究奠定了重要的理论基础。

然后，在麻省理工学院的Stefanie Jegelka教授的指导下，他完成了有关机器学习的博士后研究。

目前，他主要从事LLM开发，专注于数学推理和解决问题能力的研究，涵盖了两个主要方向：非正规化和形式化（例如精益）。

Chi Jin（金驰）

Jin Chi是普林斯顿大学电气和计算机工程系的助理教授，也是计算机科学系的联合教职员工。

此前，他获得了加利福尼亚大学伯克利分校的计算机科学博士学位，并获得了北京大学的物理学学士学位。

他的研究方向包括大型模型推理和代理，游戏理论和多代理学习，强化学习，统计学习理论和优化方法。