新智元報道

編輯：桃子 好困

迄今為止最強大的開源定理證明器登場！Goedel-Prover-V2僅用8B參數(shù)擊敗671B的DeepSeek-Prover，并再次奪下數(shù)學(xué)PutnamBench冠軍。十位核心貢獻者，八大頂尖機構(gòu)，讓AI形式化證明再破紀(jì)錄。

全球最強的開源「定理證明器」誕生了！

來自普林斯頓、清華、英偉達、斯坦福等八大頂尖機構(gòu)聯(lián)手，祭出了第二版Goedel-Prover-V2模型。

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

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

這一次，新版模型一共有兩個參數(shù)版本：32B和8B。

歷經(jīng)數(shù)月迭代，Goedel-Prover-V2再次在PutnamBench上奪冠，用更少的算力，解決了64道數(shù)學(xué)難題。

而且，在IMO級別的基準(zhǔn)——MathOlympiadBench，新模型刷爆SOTA，一舉攻克了73個問題。

相比之下，DeepSeek-Prover-671B僅解決了50個問題。

另外，在匯集三大國際奧數(shù)競賽難題的MiniF2F基準(zhǔn)上，32B在Pass@32上拿下90.4%成績，擊敗了DeepSeek-Prover-V2-671B（82.4%），8B模型與之實力相當(dāng)。

它的出世，標(biāo)志著AI又在在自動形式化證明生成領(lǐng)域?qū)崿F(xiàn)了全新技術(shù)突破。

對此，有網(wǎng)友期待地表示，「當(dāng)前，IMO 2025正在激烈比拼中，不知接下來Goedel-Prover-V2的實戰(zhàn)表現(xiàn)如何」？

8B模型

一舉擊敗671B DeepSeek Prover

目前，研究團隊暫未放出arXiv論文。

不過，在項目主頁和Hugging Face，對最新Goedel-Prover-V2模型背后技術(shù)和性能基準(zhǔn)，展開了詳實的介紹。

那么，小參數(shù)的模型是如何超越了671B？

這里，Goedel-Prover-V2以Qwen3?8B?和Qwen3?32B?作為基座模型，采用了標(biāo)準(zhǔn)的「專家迭代與強化學(xué)習(xí)」框架。

具體來說，研究團隊在一個完整流程中——形式化問題、生成并驗證證明，再利用新發(fā)現(xiàn)的正確證明訓(xùn)練下一代模型，并通過RL進一步提升性能。

接下來，他們還融入了三大創(chuàng)新技術(shù)：

1. 分層式數(shù)據(jù)合成（Scaffolded data synthesis）

生成難度逐步遞增的合成證明任務(wù)，對模型進行漸進式訓(xùn)練，使其能夠掌握愈發(fā)復(fù)雜的定理；

自動生成介于已解決簡單問題與未解復(fù)雜問題之間的中級難度題目，形成更平滑的難度遞進，為訓(xùn)練提供更密集、信息量更高的信號。

2. 驗證器引導(dǎo)的自我修正（Verifier-guided self-correction）

訓(xùn)練模型有效利用?Lean?編譯反饋，反復(fù)修訂自身證明，高度模擬人類完善證明的過程，并將這一任務(wù)融入監(jiān)督微調(diào)與強化學(xué)習(xí)階段。

3. 模型平均（Model averaging）

為防止后期訓(xùn)練導(dǎo)致多樣性喪失，將已訓(xùn)練的檢查點與基座模型進行平均。

這一簡潔技術(shù)能夠恢復(fù)多樣性，并在更大的?K?值下顯著提升?Pass@K?表現(xiàn)。

簡言之，融合多個模型檢查點，提升魯棒性與整體性能。

極少算力刷爆SOTA，Scaling超強

Goedel-Prover-V2首先會生成一個初始候選證明，再借助?Lean?編譯器的反饋進行迭代修正，以提高證明質(zhì)量。

研究中，模型進行了兩輪自我修正，但計算開銷依然可控——總輸出長度（包含初始證明及兩次修正）僅從標(biāo)準(zhǔn)的?32K? token適度增加到40K? token。

如下表所示，展示了Goedel-Prover-V2在Pass@32下的所有結(jié)果。

首先，在全部三個數(shù)據(jù)集中，旗艦32B?模型均顯著超越此前SOTA模型，即DeepSeek?Prover?V2?671B與Kimina?Prover?72B。

其次，在miniF2F數(shù)據(jù)集上，8B模型在性能上與DeepSeek?Prover?V2?671B相當(dāng)，但模型規(guī)模僅為其?1/100。

如下成績是，Goedel-Prover-V2在PutnamBench基準(zhǔn)上，用更少的算力，擊敗所有SOTA位居榜首。

下面的Scaling曲線表明，在整個推理計算范圍內(nèi)，Goedel-Prover-V2-32B始終優(yōu)于所有的頂尖模型。

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

論文核心貢獻者之一Chi Jin稱，Goedel-Prover只用了高校實驗室里的GPU，就實現(xiàn)了超強性能。

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

Yong Lin

Yong Lin是普林斯頓大學(xué)語言與智能（PLI）的博士后研究員，導(dǎo)師是Chi Jin、Sanjeev Arora和Danqi Chen。

此前，他在香港科技大學(xué)獲得博士學(xué)位，師從張潼教授；在浙江大學(xué)獲得學(xué)士和碩士學(xué)位，專業(yè)排名1/207。

在攻讀博士學(xué)位之前，他于2017年至2021年在阿里擔(dān)任高級機器學(xué)習(xí)工程師。

他的研究聚焦于機器學(xué)習(xí)和LLM的后訓(xùn)練技術(shù)。主要研究方向包括：

形式化數(shù)學(xué)推理：讓大語言模型能夠使用可驗證的語言（即形式化語言，如 LEAN）進行推理。

LLM后訓(xùn)練：提升模型的有益性、無害性與誠實性等特質(zhì)。

Shange Tang

Shange Tang是普林斯頓大學(xué)運籌學(xué)與金融工程系的博士生，導(dǎo)師是Jianqing Fan教授與金馳教授。

此前，他在北京大學(xué)數(shù)學(xué)科學(xué)學(xué)院獲得學(xué)士學(xué)位。

他的研究興趣為統(tǒng)計學(xué)和機器學(xué)習(xí)的理論與應(yīng)用。

Bohan Lyu

Bohan Lyu目前在普林斯頓大學(xué)PLI，從事基于大語言模型與形式化語言的自動化數(shù)學(xué)定理證明研究，師從金馳教授。

此前，他在清華大學(xué)獲得學(xué)士學(xué)位。并曾在清華大學(xué)NLP實驗室（導(dǎo)師是劉知遠教授）和加州大學(xué)圣地亞哥分校Rose-STL-Lab（導(dǎo)師是虞琦教授）進行科研實習(xí)。

他的研究興趣為機器學(xué)習(xí)（ML）和自然語言處理（NLP）。

Ziran Yang（楊子然）

楊子然是普林斯頓大學(xué)電子與計算機工程系的博士生，師從金馳教授。

此前，他在北京大學(xué)元培學(xué)院獲得學(xué)士學(xué)位，到時是朱毅鑫教授、朱松純教授。

Jui-Hui Chung（鐘瑞輝）

鐘瑞輝是普林斯頓大學(xué)應(yīng)用與計算數(shù)學(xué)項目的博士生，師從Jacob Shapiro教授。

他本科及碩士畢業(yè)于臺灣大學(xué)物理系，師從Ying-Jer Kao教授，期間主要從事計算物理研究。

他的研究方向是拓撲絕緣體的數(shù)學(xué)物理特性。近期在Chi Jin教授指導(dǎo)下，開展基于LLM的自動定理證明研究。

Haoyu Zhao

Haoyu Zhao是普林斯頓大學(xué)的博士生，師從Sanjeev Arora教授。

此前，他在清華大學(xué)計算機科學(xué)實驗班（姚班）獲得學(xué)士學(xué)位，導(dǎo)師是陳衛(wèi)教授。

他的研究興趣橫跨數(shù)學(xué)、算法與學(xué)習(xí)的交叉領(lǐng)域。

Lai Jiang

上海交通大學(xué)。

Yihan Geng

北京大學(xué)。

Hongzhou Lin

Hongzhou Lin是亞馬遜應(yīng)用研究科學(xué)家，隸屬于AGI基礎(chǔ)團隊。

此前，他在法國INRIA格勒諾布爾中心獲得了博士學(xué)位，師從Zaid Harchaoui和Julien Mairal教授。期間，他首創(chuàng)了一階優(yōu)化算法的通用加速框架，為后續(xù)應(yīng)用科學(xué)研究奠定了重要理論基礎(chǔ)。

隨后在MIT的Stefanie Jegelka教授指導(dǎo)下完成機器學(xué)習(xí)方向的博士后研究。

目前，他主要從事LLM開發(fā)工作，專注于數(shù)學(xué)推理與問題解決能力的研究，涵蓋非形式化與形式化（如LEAN）兩大方向。

Chi Jin（金馳）

金馳是普林斯頓大學(xué)電氣與計算機工程學(xué)系助理教授，計算機科學(xué)系聯(lián)合聘任教員。

此前，他在加州大學(xué)伯克利分校獲得計算機科學(xué)博士學(xué)位，在北京大學(xué)獲得物理學(xué)學(xué)士學(xué)位。

他的研究方向包括，大模型推理與智能體、博弈論與多智能體學(xué)習(xí)、強化學(xué)習(xí)、統(tǒng)計學(xué)習(xí)理論、優(yōu)化方法。

參考資料：

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