新智元報道

編輯：桃子 好困

【新智元導讀】迄今為止最強大的開源定理證明器登場！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是普林斯頓大學運籌學與金融工程系的博士生，導師是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/