近日，由普林斯頓大學牽頭，聯合清華大學、北京大學、上海交通大學、斯坦福大學，以及英偉達、亞馬遜、Meta FAIR 等多家頂尖機構的研究者共同推出了新一代開源數學定理證明模型——Goedel-Prover-V2。

該項目的 32B 旗艦模型在多個自動數學定理證明的主要基準測試上均大幅超過之前的最先進開源模型 DeepSeek-Prover-V2-671B；而 8B 小尺寸模型在特定基準上，性能表現與 DeepSeek-Prover-V2-671B 持平，展示了其在效率和能力上的新突破。

• 項目主頁：http://blog.goedel-prover.com
• HuggingFace 模型下載：https://huggingface.co/Goedel-LM/Goedel-Prover-V2-32B

主要成果

MiniF2F 性能新高：其 32B 旗艦模型在 MiniF2F 測試中，Pass@32 （每道測試題目嘗試 32 次；pass 數越小，計算開銷越小）的正確率相較于之前的 SOTA 模型 DeepSeek-Prover-V2-671B 提升了 8.0%。

小而強：8B 參數模型的性能表現與之前 671B 參數的 SOTA 模型持平。

登頂 PutnamBench：在極具挑戰性的 PutnamBench （普特南數學競賽基準）上，該模型排名第一。

項目簡介

Goedel-Prover-V2 立足于形式化推理，即以精確、無歧義的形式語言（Formal Language）來進行數學推理，完整數學定理證明，整個推理和證明過程可被機器自動驗證。目前，最主流的形式化證明語言 Lean 已經被廣泛的數學家群體接受。

Goedel-Prover-V2 的開發流程基于標準的專家迭代（expert iteration）與強化學習，并引入了三項關鍵創新：

• 分層式數據合成 (Scaffolded data synthesis)：通過自動合成難度漸進遞增的證明任務來訓練模型，讓模型能夠循序漸進地處理更復雜的定理。
• 驗證器引導的自我修正 (Verifier-guided self-correction)：模型通過利用 Lean 編譯器的反饋，學習迭代地修正自身生成的證明，模擬人類自我修正的過程。
• 模型平均 (Model averaging)：融合不同訓練節點的模型權重，以提升模型的魯棒性與綜合性能。

基于這些方法，該項目的較小模型 Goedel-Prover-V2-8B 在 MiniF2F 測試集上（Pass@32）達到了 83.3% 的通過率，甚至超越此前模型參數量超過 80 倍的 SOTA 模型 DeepSeek-Prover-V2-671B 的性能。其旗艦模型 Goedel-Prover-V2-32B 更是將此項指標提升至 88.1% （標準模式）和 90.4% （自我修正模式），大幅超越了所有先前的 SOTA 模型。

在 PutnamBench 上，開啟自我修正模式的旗艦模型僅使用 Pass@64 就解決了 64 個問題，用遠遠更小的計算開銷超過了 DeepSeek-Prover-V2-671B 在 Pass@1024 下解決 47 個問題的記錄。

性能表現

基準測試結果

自我修正模式：模型先生成初始證明，再利用 Lean 編譯器的反饋進行兩輪自我修正。這一過程仍然保持了高效：總的輸出長度（包括初始證明和兩輪修正）僅僅從標準的 32K tokens 略微增加到 40K tokens。

圖 1: 在 MiniF2F、PutnamBench、以及新發布的 MathOlympiadBench （包含 360 道數學奧林匹克競賽級別題目）上的 Pass@32 性能對比。橫軸為不同模型表現，縱軸為模型性能（解決題目的百分比或者個數）

上圖展示了 Goedel-Prover-V2 在 MiniF2F、PutnamBench 和 MathOlympiadBench 三個基準測試中的性能。所有數據在 Pass@32 下測得：

• 在三個數據集中，32B 旗艦模型在標準模式和自我修正模式下的性能均顯著超過了之前的 SOTA 模型 DeepSeek-Prover-V2-671B 和 Kimina-Prover-72B。
• 在 MiniF2F 上，8B 模型的性能與模型尺寸大近 100 倍的 DeepSeek-Prover-V2-671B 相當。

PutnamBench 排行榜

下表為 PutnamBench 的最新排名。Goedel-Prover-V2-32B 在相對更少的計算開銷（pass 數）下取得了領先成績。

表 1: PutnamBench 排行榜。

推理時的計算擴展性

推理時的計算擴展性曲線顯示，在不同的推理采樣預算下，Goedel-Prover-V2-32B 模型的性能均穩定超過了之前的同類模型。

圖 2: 在不同采樣預算下，模型在 MiniF2F 測試集上的性能表現。橫軸為 pass 數（采樣預算），縱軸為解決題目的百分比

技術方法

Goedel-Prover-V2 的性能主要基于以下四種核心技術：

• 專家迭代與強化學習 (Expert Iteration & RL)：項目遵循標準的訓練流程：形式化問題、生成并驗證證明、利用新證明訓練下一代模型，并結合強化學習進行優化。
• 分層式數據合成 (Scafforded Data Synthesis)：該技術自動生成中等難度的問題，用以彌合已解決的簡單問題與尚未解決的復雜問題之間的鴻溝，從而實現更平滑的難度遞進，并為模型提供更密集且更具信息量的訓練信號。
• 驗證器引導的自我修正 (Verifier-Guided Self-Correction)：模型被訓練以使用 Lean 編譯器的反饋來迭代修正自身證明，這一能力被整合到監督微調和強化學習流程中。
• 模型平均 (Model Averaging)：為避免訓練后期模型多樣性下降，研究者將訓練好的模型與基礎模型進行權重平均，此方法有助于提升在需要更多采樣次數時的 Pass@K 性能。

模型與數據集下載

為了促進相關領域的研究，團隊已公開發布了 Goedel-Prover-V2 模型及全新的 MathOlympiadBench 基準。

模型下載

• Goedel-Prover-V2-32B:https://huggingface.co/Goedel-LM/Goedel-Prover-V2-32B
• Goedel-Prover-V2-8B:https://huggingface.co/Goedel-LM/Goedel-Prover-V2-8B

數據集下載

• MathOlympiadBench:https://huggingface.co/datasets/Goedel-LM/FoMOBench

MathOlympiadBench 是一個收錄了奧林匹克級別數學競賽問題形式化版本的數據集，來源包括 Compfiles 和 IMOSLLean4 等代碼庫。數據集共包含 360 個問題，覆蓋了 IMO （International Math Olympiad，國際數學奧林匹克競賽）、IMO 候選短名單及其他區域性競賽題。

研究團隊表示，發布此模型旨在支持開源社區的研究，包括為 IMO 等數學競賽做準備的相關項目。包含完整技術細節的論文將在未來幾周內發布。

項目骨干：

林勇（Yong Lin），普林斯頓大學博士后，與金馳、陳丹琦、Sanjeev Arora 教授合作，研究方向為大模型的形式化數學推理與后訓練。相關成果曾獲 NAACL 杰出論文獎，入選 2023 年蘋果 AI 學者。 

個人主頁：https://linyongver.github.io/Website/

唐山茖（Shange Tang），普林斯頓大學博士生，導師是金馳和范劍青教授。他的研究領域包括大模型的形式化數學推理、分布外泛化等。 

個人主頁：https://shangetang.github.io/

項目負責人：

金馳（Chi Jin），普林斯頓大學電子與計算機工程系教授。他的研究專注于機器學習的決策制定，致力于開發具備復雜決策與高級推理能力的智能體。其團隊在強化學習、博弈論及最優化等領域奠定了堅實的理論基礎。近期，他們正積極將研究拓展至大語言模型（LLM），重點提升其推理能力。金馳教授曾榮獲多項重要榮譽，如斯隆研究學者獎（Sloan Research Fellowship）、美國國家科學基金會 CAREER 獎（NSF CAREER Award）等。 

個人主頁：https://sites.google.com/view/cjin/home