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

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

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

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

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

AlphaProof團隊規(guī)模并不大。大部分時間里只有大約10個人，臨近IMO比賽時才有更多人加入。

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

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

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

把數(shù)學證明當游戲來玩

AlphaProof的核心思路其實很直接：把數(shù)學證明過程變成一個可以反復訓練的游戲。

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

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

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

這個證明網(wǎng)絡不僅要理解當前的證明狀態(tài)，還要同時輸出兩個關鍵信息：

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

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

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

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

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

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

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

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

即使自動形式化的結果不完全準確，只要它是一個有效的形式命題，AlphaProof都能從嘗試證明它的過程中學到東西。

整個主訓練階段消耗了約8萬TPU天的計算資源。

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

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

測試時強化學習循環(huán)則展現(xiàn)了一種更加精細的適應機制。

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

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

系統(tǒng)會啟動一個獨立的AlphaZero式學習過程，專門在這些變體上訓練，逐步積累解決原問題所需的洞察。這個機制可以并行處理多個目標問題，每個問題都有自己的變體課程和專屬的學習進程。

IMO賽場上臨時突破

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

AlphaProof的方法，正是這一預言的預演。

論文地址：
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