夢晨 發(fā)自 凹非寺
量子位 | 公眾號 QbitAI

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

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

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

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

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

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

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

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

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

AlphaProof的核心思路其實(shí)很直接：把數(shù)學(xué)證明過程變成一個(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需要通過選擇合適的策略（tactics）來推進(jìn)證明。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Hinton在今年6月份的訪談中指出，AI未來在數(shù)學(xué)方面很可能會比人類強(qiáng)得多：由于它能夠在封閉的數(shù)學(xué)系統(tǒng)中即時(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