去年 7 月，Google DeepMind 宣布其 AI 系統在國際數學奧林匹克競賽（International Mathematical Olympiad, IMO）中取得銀牌成績，這是 AI 首次在這項賽事中達到獎牌水平。當時團隊承諾會公布技術細節，如今，這一承諾得以兌現：11 月 12 日，完整論文發表在《自然》（Nature）雜志上，AlphaProof 系統的技術細節得以全面公開。

圖丨相關論文（Nature）

作為匯集了全球最擅長數學的一批青少年的比賽，IMO 的試卷涵蓋六道極具挑戰性的題目，覆蓋代數、組合數學、數論和幾何等領域。這些題目的難度往往讓人望而生畏，在 2024 年的比賽中，滿分 42 分的試卷上，只有不到百分之一的參賽者能夠獲得滿分。許多數學界的菲爾茲獎得主都曾是 IMO 的參賽者，這足以說明這項賽事在數學界的分量。而近年來，IMO 也逐漸成為衡量人工智能系統高級數學推理能力的標桿性挑戰。

在 2024 年的 IMO 中，AlphaProof 與專門處理幾何問題的 AlphaGeometry 2 系統聯手，完成了六道題目中的四道，獲得 28 分。這個成績相當于當年 609 名參賽者中排名前列的銀牌獲得者的水平。此外，AlphaProof 還成功解決了被認為是當年最難的第六題，這道題目只有五名人類參賽者完全解答出來。這是人工智能系統首次在 IMO 中達到獎牌級別的表現，標志著機器數學推理能力的一個重要里程碑。

（Google）

AlphaProof 的核心優勢在于它將形式化數學語言與強化學習深度結合。傳統的大語言模型雖然能夠生成看似合理的數學推理步驟，但它們存在一個致命弱點——會產生“幻覺”，即生成錯誤但看起來可信的內容。而數學證明需要的是絕對的嚴謹性，容不得半點瑕疵。為了解決這個問題，研究團隊選擇了 Lean 這種形式化語言作為系統的工作環境。

Lean 是一種交互式定理證明助手，它能夠自動驗證數學證明的正確性。在 Lean 中，每一步推理都必須符合嚴格的邏輯規則，任何錯誤都會立即被系統檢測出來。這種特性使得 AI 生成的證明可以被自動驗證，不需要人工檢查，也不會出現幻覺問題。問題在于，Lean 這樣的形式化系統雖然嚴謹，卻面臨著訓練數據稀缺的困境，Lean 的標準數學庫 mathlib 只包含約二十萬個定理，遠遠無法滿足大規模機器學習的需求。

圖丨AlphaProof 核心推理組件（Nature）

研究團隊想出了一個辦法。他們首先對 Gemini 語言模型進行微調，使其能夠將自然語言的數學問題自動轉化為 Lean 能夠理解的形式化語言。這個過程被稱為“自動形式化”。通過這種方法，他們從一百萬個自然語言數學命題中生成了八千萬個不同的 Lean 形式化語句。這個龐大的合成數據集為后續的強化學習訓練提供了充足的素材。

AlphaProof 的架構借鑒了 AlphaZero 的設計思路。系統的核心是一個擁有三十億參數的編碼器-解碼器變換器網絡，它能夠理解 Lean 中的證明狀態，并生成兩種輸出：一個策略網絡，用于建議下一步應該采取的證明策略；一個價值函數，用于評估當前證明路徑的前景。這兩個輸出共同指導一個專門設計的樹搜索算法，在浩瀚的可能證明空間中尋找正確的路徑。

圖丨AlphaProof 的學習與適應過程（Nature）

在樹搜索的設計上，研究團隊引入了一個名為“乘積節點”（product node）的概念。在 Lean 中，證明一個定理往往需要將目標分解為多個獨立的子目標——比如使用數學歸納法時，需要分別證明基礎情況和遞推步驟。“乘積節點”要求其所有子節點都必須被證明，這讓搜索算法能夠有效追蹤哪些子目標已經完成，并將計算資源集中在最困難的分支上。這種設計大大提高了搜索的效率。

但 AlphaProof 最具創新性的技術，或許是它的“測試時強化學習”（Test-Time RL, TTRL）。對于特別重要或困難的問題，系統會在推理時投入大量計算資源進行深度學習。具體來說，它會利用語言模型生成目標定理的眾多變體。這些變體難度各異，形成了一個自然的學習課程。通過解決這些較容易的變體，系統能夠逐步積累經驗和洞察，最終攻克原始的復雜問題。這種方法在解決 2024 年 IMO 第六題時發揮了關鍵作用。

在訓練過程中，AlphaProof 會仔細追蹤每個形式化問題的進展，一旦證明某個形式化語句是錯誤的，就不再浪費資源嘗試證明它；而當找到一個成功的證明后，系統還會再次嘗試，看能否發現更短、更優雅的證明。訓練初期，系統從小規模搜索開始，避免在過難的問題上浪費計算；隨著訓練深入，逐步增加搜索的規模和深度。這種漸進式的訓練策略讓系統既能快速找到簡單證明，又不會被困在難題上無謂消耗資源。

在實戰中，AlphaProof 呈現出與人類選手非常不同的特點。在官方比賽中，學生們有兩個 4.5 小時的答題時段。而 AlphaProof 解決某些問題只需幾分鐘，但處理其他問題卻可能需要長達三天時間。這種時間差異引起了一些討論。對此，研究團隊表示，重點不在于比拼速度，而在于驗證 AI 是否能達到奧賽水平的推理能力。隨著技術進步，這個時間差距會逐漸縮小。

菲爾茲獎得主、IMO 金牌得主 Timothy Gowers 教授在評估 AlphaProof 的解答后說：“作為數學家，我認為這很令人印象深刻，是一個顯著的進步。”劍橋大學 AI 與數學專家 Katie Collins 認為，自動化形式化過程的突破對數學界很有意義：“如果研究成果能夠用這種證明系統來表述，我們對發表結果的正確性會更有信心，也能促進更多合作。”

值得一提的是，就在今年的 IMO 競賽中，DeepMind 推出了全新的系統 Gemini Deep Think，實現了端到端的自然語言推理，在 4.5 小時的限制時間內獲得了 35 分的金牌成績。這個系統不再需要形式化語言的中介，直接用自然語言理解問題并生成可讀的證明。這表明，從銀牌到金牌，從形式化語言到自然語言，AI 數學推理能力正在快速演進。AlphaProof 開創的形式化驗證路徑和新系統的自然語言能力，或許會在未來某個時刻匯聚融合，帶來更加強大和通用的數學 AI 工具。

論文作者之一 Julian Schrittwieser 在博客中提到了一些細節。他特別提到 Test-Time RL 的可擴展性，直言：“限制我們的只是能用上多少 TPU 算力。”這種在推理時投入大量計算資源來獲得更好結果的方式，可能為 AI 系統開辟新的優化方向。更重要的是，AlphaProof 表明強化學習與搜索的組合對大語言模型同樣有效，這為構建更通用、可驗證的 AI 系統提供了思路。

不過，目前所有 IMO 題目都需要人工翻譯成形式語言才能讓 AlphaProof 理解。雖然團隊也試驗了基于 Gemini 的自然語言推理系統，但要實現真正自主的數學 AI，還需要解決從自然語言到形式語言的自動轉換問題。另外，AlphaProof 在代數和數論上表現不錯，但在組合數學上相對較弱，團隊正在研究原因。

參考資料：

1.https://www.nature.com/articles/s41586-025-09833-y

2.https://www.julian.ac/blog/2025/11/13/alphaproof-paper/

3.https://www.nature.com/articles/d41586-025-03585-5

運營/排版：何晨龍