近日，由普林斯頓大學(xué)牽頭，聯(lián)合清華大學(xué)、北京大學(xué)、上海交通大學(xué)、斯坦福大學(xué)，以及英偉達(dá)、亞馬遜、meta FAIR 等多家頂尖機(jī)構(gòu)的研究者共同推出了新一代開(kāi)源數(shù)學(xué)定理證明模型——Goedel-Prover-V2。

該項(xiàng)目的 32B 旗艦?zāi)Ｐ驮诙鄠€(gè)自動(dòng)數(shù)學(xué)定理證明的主要基準(zhǔn)測(cè)試上均大幅超過(guò)之前的最先進(jìn)開(kāi)源模型 DeepSeek-Prover-V2-671B；而 8B 小尺寸模型在特定基準(zhǔn)上，性能表現(xiàn)與 DeepSeek-Prover-V2-671B 持平，展示了其在效率和能力上的新突破。

項(xiàng)目主頁(yè)http://blog.goedel-prover.comHuggingFace 模型下載https://huggingface.co/Goedel-LM/Goedel-Prover-V2-32B

主要成果

MiniF2F性能新高：其 32B 旗艦?zāi)Ｐ驮?MiniF2F 測(cè)試中，Pass@32 （每道測(cè)試題目嘗試 32 次；pass 數(shù)越小，計(jì)算開(kāi)銷越?。┑恼_率相較于之前的 SOTA 模型 DeepSeek-Prover-V2-671B 提升了 8.0%。

小而強(qiáng)：8B 參數(shù)模型的性能表現(xiàn)與之前 671B 參數(shù)的 SOTA 模型持平。

登頂PutnamBench：在極具挑戰(zhàn)性的 PutnamBench （普特南數(shù)學(xué)競(jìng)賽基準(zhǔn)）上，該模型排名第一。

項(xiàng)目簡(jiǎn)介

Goedel-Prover-V2 立足于形式化推理，即以精確、無(wú)歧義的形式語(yǔ)言（Formal Language）來(lái)進(jìn)行數(shù)學(xué)推理，完整數(shù)學(xué)定理證明，整個(gè)推理和證明過(guò)程可被機(jī)器自動(dòng)驗(yàn)證。目前，最主流的形式化證明語(yǔ)言Lean已經(jīng)被廣泛的數(shù)學(xué)家群體接受。

Goedel-Prover-V2 的開(kāi)發(fā)流程基于標(biāo)準(zhǔn)的專家迭代（expert iteration）與強(qiáng)化學(xué)習(xí)，并引入了三項(xiàng)關(guān)鍵創(chuàng)新：

分層式數(shù)據(jù)合成(Scaffolded data synthesis)：通過(guò)自動(dòng)合成難度漸進(jìn)遞增的證明任務(wù)來(lái)訓(xùn)練模型，讓模型能夠循序漸進(jìn)地處理更復(fù)雜的定理。

驗(yàn)證器引導(dǎo)的自我修正(Verifier-guided self-correction)：模型通過(guò)利用 Lean 編譯器的反饋，學(xué)習(xí)迭代地修正自身生成的證明，模擬人類自我修正的過(guò)程。

模型平均 (Model averaging)：融合不同訓(xùn)練節(jié)點(diǎn)的模型權(quán)重，以提升模型的魯棒性與綜合性能。

基于這些方法，該項(xiàng)目的較小模型 Goedel-Prover-V2-8B 在 MiniF2F 測(cè)試集上（Pass@32）達(dá)到了83.3% 的通過(guò)率，甚至超越此前模型參數(shù)量超過(guò) 80 倍的 SOTA 模型 DeepSeek-Prover-V2-671B 的性能。其旗艦?zāi)Ｐ?Goedel-Prover-V2-32B 更是將此項(xiàng)指標(biāo)提升至 88.1%（標(biāo)準(zhǔn)模式）和90.4%（自我修正模式），大幅超越了所有先前的 SOTA 模型。

在 PutnamBench 上，開(kāi)啟自我修正模式的旗艦?zāi)Ｐ蛢H使用 Pass@64 就解決了 64 個(gè)問(wèn)題，用遠(yuǎn)遠(yuǎn)更小的計(jì)算開(kāi)銷超過(guò)了 DeepSeek-Prover-V2-671B 在 Pass@1024 下解決 47 個(gè)問(wèn)題的記錄。

性能表現(xiàn)

基準(zhǔn)測(cè)試結(jié)果

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

圖 1: 在 MiniF2F、PutnamBench、以及新發(fā)布的 MathOlympiadBench （包含 360 道數(shù)學(xué)奧林匹克競(jìng)賽級(jí)別題目）上的 Pass@32 性能對(duì)比。橫軸為不同模型表現(xiàn)，縱軸為模型性能（解決題目的百分比或者個(gè)數(shù)）

上圖展示了 Goedel-Prover-V2 在 MiniF2F、PutnamBench 和 MathOlympiadBench 三個(gè)基準(zhǔn)測(cè)試中的性能。所有數(shù)據(jù)在 Pass@32 下測(cè)得：

在三個(gè)數(shù)據(jù)集中，32B 旗艦?zāi)Ｐ驮跇?biāo)準(zhǔn)模式和自我修正模式下的性能均顯著超過(guò)了之前的 SOTA 模型 DeepSeek-Prover-V2-671B 和 Kimina-Prover-72B。

在 MiniF2F 上，8B 模型的性能與模型尺寸大近 100 倍的 DeepSeek-Prover-V2-671B 相當(dāng)。

PutnamBench 排行榜

下表為 PutnamBench 的最新排名。Goedel-Prover-V2-32B 在相對(duì)更少的計(jì)算開(kāi)銷（pass 數(shù)）下取得了領(lǐng)先成績(jī)。

表 1: PutnamBench 排行榜。

推理時(shí)的計(jì)算擴(kuò)展性

推理時(shí)的計(jì)算擴(kuò)展性曲線顯示，在不同的推理采樣預(yù)算下，Goedel-Prover-V2-32B 模型的性能均穩(wěn)定超過(guò)了之前的同類模型。

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

技術(shù)方法

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

專家迭代與強(qiáng)化學(xué)習(xí) (Expert Iteration & RL)：項(xiàng)目遵循標(biāo)準(zhǔn)的訓(xùn)練流程：形式化問(wèn)題、生成并驗(yàn)證證明、利用新證明訓(xùn)練下一代模型，并結(jié)合強(qiáng)化學(xué)習(xí)進(jìn)行優(yōu)化。

分層式數(shù)據(jù)合成 (Scafforded Data Synthesis)：該技術(shù)自動(dòng)生成中等難度的問(wèn)題，用以彌合已解決的簡(jiǎn)單問(wèn)題與尚未解決的復(fù)雜問(wèn)題之間的鴻溝，從而實(shí)現(xiàn)更平滑的難度遞進(jìn)，并為模型提供更密集且更具信息量的訓(xùn)練信號(hào)。

驗(yàn)證器引導(dǎo)的自我修正 (Verifier-Guided Self-Correction)：模型被訓(xùn)練以使用 Lean 編譯器的反饋來(lái)迭代修正自身證明，這一能力被整合到監(jiān)督微調(diào)和強(qiáng)化學(xué)習(xí)流程中。

模型平均 (Model Averaging)：為避免訓(xùn)練后期模型多樣性下降，研究者將訓(xùn)練好的模型與基礎(chǔ)模型進(jìn)行權(quán)重平均，此方法有助于提升在需要更多采樣次數(shù)時(shí)的 Pass@K 性能。

模型與數(shù)據(jù)集下載

為了促進(jìn)相關(guān)領(lǐng)域的研究，團(tuán)隊(duì)已公開(kāi)發(fā)布了 Goedel-Prover-V2 模型及全新的MathOlympiadBench基準(zhǔn)。

模型下載

Goedel-Prover-V2-32Bhttps://huggingface.co/Goedel-LM/Goedel-Prover-V2-32B

Goedel-Prover-V2-8Bhttps://huggingface.co/Goedel-LM/Goedel-Prover-V2-8B

數(shù)據(jù)集下載

MathOlympiadBenchhttps://huggingface.co/datasets/Goedel-LM/FoMOBench

MathOlympiadBench是一個(gè)收錄了奧林匹克級(jí)別數(shù)學(xué)競(jìng)賽問(wèn)題形式化版本的數(shù)據(jù)集，來(lái)源包括 Compfiles 和 IMOSLLean4 等代碼庫(kù)。數(shù)據(jù)集共包含 360 個(gè)問(wèn)題，覆蓋了 IMO （International Math Olympiad，國(guó)際數(shù)學(xué)奧林匹克競(jìng)賽）、IMO 候選短名單及其他區(qū)域性競(jìng)賽題。

研究團(tuán)隊(duì)表示，發(fā)布此模型旨在支持開(kāi)源社區(qū)的研究，包括為 IMO 等數(shù)學(xué)競(jìng)賽做準(zhǔn)備的相關(guān)項(xiàng)目。包含完整技術(shù)細(xì)節(jié)的論文將在未來(lái)幾周內(nèi)發(fā)布。

項(xiàng)目骨干：

林勇（Yong Lin），普林斯頓大學(xué)博士后，與金馳、陳丹琦、Sanjeev Arora 教授合作，研究方向?yàn)榇竽Ｐ偷男问交瘮?shù)學(xué)推理與后訓(xùn)練。相關(guān)成果曾獲 NAACL 杰出論文獎(jiǎng)，入選 2023 年蘋果 AI 學(xué)者。

個(gè)人主頁(yè)：

https://linyongver.github.io/Website/

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

個(gè)人主頁(yè)：

https://shangetang.github.io/

項(xiàng)目負(fù)責(zé)人：

金馳（Chi Jin），普林斯頓大學(xué)電子與計(jì)算機(jī)工程系教授。他的研究專注于機(jī)器學(xué)習(xí)的決策制定，致力于開(kāi)發(fā)具備復(fù)雜決策與高級(jí)推理能力的智能體。其團(tuán)隊(duì)在強(qiáng)化學(xué)習(xí)、博弈論及最優(yōu)化等領(lǐng)域奠定了堅(jiān)實(shí)的理論基礎(chǔ)。近期，他們正積極將研究拓展至大語(yǔ)言模型（LLM），重點(diǎn)提升其推理能力。金馳教授曾榮獲多項(xiàng)重要榮譽(yù)，如斯隆研究學(xué)者獎(jiǎng)（Sloan Research Fellowship）、美國(guó)國(guó)家科學(xué)基金會(huì) CAREER 獎(jiǎng)（NSF CAREER Award）等。

個(gè)人主頁(yè)：

https://sites.google.com/view/cjin/home