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

延續DeepMind的命名傳統，這次叫：AlphaProof。

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

作者Tom Zahavy也趁此機會分享了一些開發過程中的細節：

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

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

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

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

把數學證明當游戲來玩

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

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

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

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

這個證明網絡不僅要理解當前的證明狀態，還要同時輸出兩個關鍵信息：

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

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

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

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

訓練AlphaProof面臨的最大挑戰是：哪來那么多數學題？

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

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

主強化學習循環是整個訓練的核心。系統會不斷嘗試證明或反證這些自動生成的命題，成功的證明會被用來更新神經網絡。

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

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

論文中的核心架構圖展示了AlphaProof的兩個學習循環是如何協同工作的。

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

測試時強化學習循環則展現了一種更加精細的適應機制。

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

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

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

IMO賽場上臨時突破

AlphaProof在2024年IMO上的表現堪稱驚艷，現在背后更多開發細節被公開。

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

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

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

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

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

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

數學AI的下一步在哪里

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

羅格斯大學的數學家Alex Kontorovich發現，AlphaProof特別擅長找出反例：

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

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

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

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

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

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

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

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

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

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

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