Nature公開(kāi)谷歌IMO金牌模型技術(shù)細(xì)節(jié)！核心團(tuán)隊(duì)僅10人，一年給AI編出8000萬(wàn)道數(shù)學(xué)題訓(xùn)練

夢(mèng)晨 2025-11-13 15:55:51 來(lái)源：量子位

夢(mèng)晨 發(fā)自 凹非寺
量子位 | 公眾號(hào) QbitAI

谷歌DeepMind的IMO金牌模型，完整技術(shù)全公開(kāi)了！

延續(xù)DeepMind的命名傳統(tǒng)，這次叫：AlphaProof。

依然是Nature刊發(fā)的形式，放出了AlphaProof的完整論文，首次詳細(xì)公開(kāi)了其背后的技術(shù)架構(gòu)和訓(xùn)練方法。值得一提的是，無(wú)師自通的下棋AlphaZero，也在這次論文里被多次提及。

作者Tom Zahavy也趁此機(jī)會(huì)分享了一些開(kāi)發(fā)過(guò)程中的細(xì)節(jié)：

AlphaProof團(tuán)隊(duì)規(guī)模并不大。大部分時(shí)間里只有大約10個(gè)人，臨近IMO比賽時(shí)才有更多人加入。

真正帶來(lái)突破的核心團(tuán)隊(duì)成員是IMO金牌得主Miklós Horváth。

他想出一個(gè)方法可以創(chuàng)建AI正在處理的問(wèn)題的各種變體，并將它們作為初始狀態(tài)，讓智能體在這些變體上進(jìn)行訓(xùn)練。

在整整一年里，這只團(tuán)隊(duì)還探索了各種研究思路，雖然很多都失敗了，但成功的那些都被整合到了AlphaProof系統(tǒng)里，現(xiàn)在全面公開(kāi)。

把數(shù)學(xué)證明當(dāng)游戲來(lái)玩

AlphaProof的核心思路其實(shí)很直接：把數(shù)學(xué)證明過(guò)程變成一個(gè)可以反復(fù)訓(xùn)練的游戲。

系統(tǒng)基于Lean定理證明器構(gòu)建了一個(gè)強(qiáng)化學(xué)習(xí)環(huán)境。在這個(gè)環(huán)境中，每個(gè)數(shù)學(xué)命題就是一個(gè)新的游戲關(guān)卡，AI需要通過(guò)選擇合適的策略（tactics）來(lái)推進(jìn)證明。

如果某個(gè)策略成功了，就會(huì)得到新的子目標(biāo)；如果所有目標(biāo)都完成了，就意味著證明完成。

論文揭示，AlphaProof使用了一個(gè)30億參數(shù)的編碼器-解碼器transformer模型作為”大腦”。

這個(gè)證明網(wǎng)絡(luò)不僅要理解當(dāng)前的證明狀態(tài)，還要同時(shí)輸出兩個(gè)關(guān)鍵信息：

一是建議接下來(lái)嘗試哪些策略，二是估計(jì)完成證明還需要多少步。

這種設(shè)計(jì)讓系統(tǒng)能夠更智能地分配計(jì)算資源，優(yōu)先探索最有希望的證明路徑。

搜索算法方面，AlphaProof采用了受AlphaZero啟發(fā)的樹(shù)搜索，但做了關(guān)鍵改進(jìn)。

比如引入了AND-OR樹(shù)結(jié)構(gòu)來(lái)處理證明中的多個(gè)獨(dú)立子目標(biāo)，當(dāng)一個(gè)證明需要同時(shí)滿(mǎn)足多個(gè)條件時(shí)，系統(tǒng)會(huì)把它們分解成獨(dú)立的子問(wèn)題分別攻克。另外還加入了漸進(jìn)采樣機(jī)制，讓系統(tǒng)在關(guān)鍵路徑上能夠探索更多樣的證明策略。

訓(xùn)練AlphaProof面臨的最大挑戰(zhàn)是：哪來(lái)那么多數(shù)學(xué)題？

他們首先用約3000億個(gè)token的代碼和數(shù)學(xué)文本對(duì)模型進(jìn)行預(yù)訓(xùn)練，讓它理解基本的邏輯結(jié)構(gòu)和數(shù)學(xué)語(yǔ)言。接著用Mathlib庫(kù)中約30萬(wàn)個(gè)人工編寫(xiě)的證明進(jìn)行微調(diào)，讓模型學(xué)會(huì)Lean的語(yǔ)法和證明技巧。

真正的突破來(lái)自于自動(dòng)形式化過(guò)程。團(tuán)隊(duì)基于Gemini 1.5 Pro開(kāi)發(fā)了一個(gè)專(zhuān)門(mén)的翻譯系統(tǒng)，能夠把自然語(yǔ)言的數(shù)學(xué)問(wèn)題轉(zhuǎn)換成Lean可以理解的形式語(yǔ)言。通過(guò)反復(fù)迭代和改進(jìn)，這個(gè)系統(tǒng)最終從約100萬(wàn)道自然語(yǔ)言數(shù)學(xué)題生成了約8000萬(wàn)道形式化問(wèn)題，遠(yuǎn)超所有現(xiàn)有數(shù)據(jù)集。

主強(qiáng)化學(xué)習(xí)循環(huán)是整個(gè)訓(xùn)練的核心。系統(tǒng)會(huì)不斷嘗試證明或反證這些自動(dòng)生成的命題，成功的證明會(huì)被用來(lái)更新神經(jīng)網(wǎng)絡(luò)。

即使自動(dòng)形式化的結(jié)果不完全準(zhǔn)確，只要它是一個(gè)有效的形式命題，AlphaProof都能從嘗試證明它的過(guò)程中學(xué)到東西。

整個(gè)主訓(xùn)練階段消耗了約8萬(wàn)TPU天的計(jì)算資源。

論文中的核心架構(gòu)圖展示了AlphaProof的兩個(gè)學(xué)習(xí)循環(huán)是如何協(xié)同工作的。

在主強(qiáng)化學(xué)習(xí)循環(huán)中，約100萬(wàn)道非正式數(shù)學(xué)問(wèn)題首先經(jīng)過(guò)形式化系統(tǒng)的處理，被翻譯成大約8000萬(wàn)道Lean能夠理解的形式化問(wèn)題。證明網(wǎng)絡(luò)配合樹(shù)搜索算法在Lean環(huán)境中不斷嘗試，無(wú)論是成功找到證明、找到反證，還是超時(shí)失敗，每一次嘗試都會(huì)產(chǎn)生經(jīng)驗(yàn)數(shù)據(jù)反饋給學(xué)習(xí)系統(tǒng)。

測(cè)試時(shí)強(qiáng)化學(xué)習(xí)循環(huán)則展現(xiàn)了一種更加精細(xì)的適應(yīng)機(jī)制。

當(dāng)面對(duì)一道特別困難的目標(biāo)問(wèn)題時(shí)，變體生成器會(huì)圍繞這道題產(chǎn)生大約40萬(wàn)個(gè)相關(guān)變體，相當(dāng)于為一道題專(zhuān)門(mén)創(chuàng)建了一個(gè)小型數(shù)據(jù)集。

這些變體包含了各種數(shù)學(xué)直覺(jué)：簡(jiǎn)化特殊情況、推廣到更一般的形式、探索類(lèi)似的結(jié)構(gòu)等。

系統(tǒng)會(huì)啟動(dòng)一個(gè)獨(dú)立的AlphaZero式學(xué)習(xí)過(guò)程，專(zhuān)門(mén)在這些變體上訓(xùn)練，逐步積累解決原問(wèn)題所需的洞察。這個(gè)機(jī)制可以并行處理多個(gè)目標(biāo)問(wèn)題，每個(gè)問(wèn)題都有自己的變體課程和專(zhuān)屬的學(xué)習(xí)進(jìn)程。

IMO賽場(chǎng)上臨時(shí)突破

AlphaProof在2024年IMO上的表現(xiàn)堪稱(chēng)驚艷，現(xiàn)在背后更多開(kāi)發(fā)細(xì)節(jié)被公開(kāi)。

面對(duì)IMO級(jí)別的難題，僅靠增加搜索時(shí)間往往不夠。這時(shí)候，前面介紹的測(cè)試時(shí)強(qiáng)化學(xué)習(xí)（TTRL）就派上了用場(chǎng)，也就是生成大量相關(guān)的變體問(wèn)題（比如簡(jiǎn)化版、推廣版、類(lèi)比版等），然后專(zhuān)門(mén)訓(xùn)練一個(gè)”專(zhuān)家”模型來(lái)攻克這道題。

以2024年IMO的第一題為例，這道題要求找出所有滿(mǎn)足特定整除性質(zhì)的實(shí)數(shù)α。AlphaProof生成的變體包括：只考慮有理數(shù)的情況、假設(shè)α滿(mǎn)足更強(qiáng)的性質(zhì)、證明α必須接近某個(gè)整數(shù)等等。通過(guò)在這些變體上訓(xùn)練，系統(tǒng)逐漸掌握了解決原問(wèn)題的關(guān)鍵。

在實(shí)際比賽中，AlphaProof成功解決了代數(shù)和數(shù)論的三道題（P1、P2、P6），其中P6是整個(gè)比賽最難的題目，609名參賽選手中只有5人完全解出。

每道題的TTRL過(guò)程需要2-3天的計(jì)算時(shí)間，雖然遠(yuǎn)超人類(lèi)選手的9小時(shí)限制，但考慮到此前最先進(jìn)的AI系統(tǒng)連最簡(jiǎn)單的IMO題都很難解決，這個(gè)成就已經(jīng)相當(dāng)了不起。

Tom Zahavy在回憶中提到，比賽期間他們通過(guò)部分證明系統(tǒng)就已經(jīng)確定的成績(jī)只能拿到銅牌水平，但TTRL還在后臺(tái)運(yùn)行。

三天后，當(dāng)三個(gè)完整證明陸續(xù)出現(xiàn)時(shí)，才終于確定能拿到金牌，團(tuán)隊(duì)興奮地敲鑼打鼓慶祝。

數(shù)學(xué)AI的下一步在哪里

AlphaProof奪金后，谷歌DeepMind已經(jīng)向科學(xué)界開(kāi)放AlphaProof的能力，研究人員可以通過(guò)申請(qǐng)獲得使用權(quán)限，多位數(shù)學(xué)家在Nature上分享了他們?cè)囉肁lphaProof的體驗(yàn)。

羅格斯大學(xué)的數(shù)學(xué)家Alex Kontorovich發(fā)現(xiàn)，AlphaProof特別擅長(zhǎng)找出反例：

每次它指出我的陳述有問(wèn)題時(shí)，我都能很快找出遺漏了什么假設(shè)，調(diào)整陳述后再次嘗試。這種來(lái)回迭代對(duì)于得到正確的形式化陳述至關(guān)重要。

伊利諾伊大學(xué)的Talia Ringer教授讓她的兩個(gè)博士生各提供了一個(gè)他們覺(jué)得棘手的引理。AlphaProof在一分鐘內(nèi)證明了其中一個(gè)，而另一個(gè)則被反證了，原來(lái)是定義中有個(gè)漏洞。

她評(píng)價(jià)“AlphaProof傾向于找反證的特性可能是它最令人驚訝的有用功能”。

當(dāng)然，數(shù)學(xué)家們也測(cè)試出了AlphaProof也有局限性。

倫敦帝國(guó)理工學(xué)院的Kevin Buzzard在嘗試用它翻譯費(fèi)馬大定理的證明時(shí)遇到了困難。他發(fā)現(xiàn)當(dāng)證明中充滿(mǎn)了“定制化的定義”時(shí)，AlphaProof就不太管用了。

這也印證了AlphaProof團(tuán)隊(duì)在論文中的發(fā)現(xiàn)：系統(tǒng)在處理Mathlib中已有概念時(shí)表現(xiàn)出色，但面對(duì)全新定義時(shí)就會(huì)遇到瓶頸。

Tom Zahavy也分享了自己對(duì)于AI在數(shù)學(xué)界應(yīng)用的思考：

AlphaProof面臨的一大挑戰(zhàn)在于它對(duì)Lean定理證明器的依賴(lài)。Lean雖然功能強(qiáng)大且擁有活躍的社區(qū)，但其持續(xù)演進(jìn)為AlphaProof創(chuàng)造了一個(gè)不穩(wěn)定的環(huán)境。這意味著在Lean的高級(jí)策略更為成熟的數(shù)學(xué)子領(lǐng)域，AlphaProof的性能往往更佳。

另一個(gè)關(guān)鍵問(wèn)題是“數(shù)據(jù)有限性 ”。獨(dú)特的數(shù)學(xué)題和數(shù)量是有限的。為了使強(qiáng)化學(xué)習(xí)智能體真正具備通用性，它需要能夠生成自己的問(wèn)題。雖然目前在創(chuàng)建IMO級(jí)別的問(wèn)題變體方面取得了一些成功，但這個(gè)方向還需要進(jìn)一步拓展。

Hinton在今年6月份的訪談中指出，AI未來(lái)在數(shù)學(xué)方面很可能會(huì)比人類(lèi)強(qiáng)得多：由于它能夠在封閉的數(shù)學(xué)系統(tǒng)中即時(shí)共享知識(shí)并生成自己的訓(xùn)練數(shù)據(jù)。

AlphaProof的方法，正是這一預(yù)言的預(yù)演。

論文地址：
https://www.nature.com/articles/s41586-025-09833-y

參考鏈接：
[1]https://www.tomzahavy.com/post/how-we-achieved-an-imo-medal-one-year-before-everyone-else
[2]https://www.nature.com/articles/d41586-025-03585-5