AlphaProof 與 AlphaGeometry 2 解出 IMO 競賽 4 題：首次達銀牌水平

高中生奧數一直被當成機器推理的試金石。頂級人類選手在國際數學奧林匹克（IMO）賽場上苦練成千上萬個小時，而大語言模型哪怕能寫程式碼、做翻譯，碰上這類需要長鏈條嚴密邏輯的考題，常常幾步就露出馬腳，開始一本正經地胡說八道。

Google DeepMind 拿出兩套專打奧數的系統：AlphaProof 和升級版的 AlphaGeometry 2。它們聯手解出了 2024 年 IMO 六道大題中的四道，最終拿到 28 分，剛好壓在銀牌上限，距離今年 29 分的金牌門檻只差一分。

讓 AlphaZero 進軍形式化數學

今年 IMO 的題目先被人工翻譯成形式數學語言 Lean，再交由 AI 解題。判分過程找來了兩位權威人物：菲爾茲獎得主 Timothy Gowers 教授，以及 2024 年 IMO 選題委員會主席 Joseph Myers 博士。兩位評審完全按照賽規打分，給解出來的四道題都打了 7 分滿分。

整個過程中最搶眼的是新系統 AlphaProof。它把大語言模型和強化學習演算法 AlphaZero 綁在一起，專門在 Lean 環境裡自我博弈、尋找嚴格證明。它負責搞定兩道代數題和一道數論題，其中還包括本屆比賽裡最難的那道題，當時全場 609 名全球尖子生裡，只有 5 個人做出了這道題。

另一邊，專門攻克幾何的 AlphaGeometry 2 表現也很亮眼。它基於 Gemini 訓練，引入了比前代快 100 倍的符號引擎。在收到題目形式化表達後，它只花了 19 秒就解出了第 4 題。不過，剩下的兩道組合數學題，兩個系統都沒能做出來。

解題時間也是個有趣的對比。真人選手分成兩場，每場 4.5 小時；AI 解出一道題只要幾分鐘，但啃下其他難題最長花了整整三天。

解決幻覺的關鍵是 Lean

為什麼以前的大模型解不好數學？自然語言訓練的資料雖然海量，但模型容易在推理中間步驟編造邏輯，看似合理其實漏洞百出。

AlphaProof 的解法很聰明：它讓預訓練的 Gemini 模型把自然語言題目翻譯成 Lean 程式碼，建起一個龐大的形式化題庫。在 Lean 環境下，系統每走一步推導，編譯器都能瞬間驗證真偽，對就是對，錯就是錯，徹底杜絕了模型幻覺。

在比賽前幾週，AlphaProof 靠著證明和證偽數以百萬計的題目不斷強化自己。甚至在比賽進行中，它還在圍繞賽題自動生成變體自我訓練，直到搜出完整的證明鏈條。

為什麼重要

這是 AI 第一次在國際公認的頂級數學賽事中達到銀牌水準。這證明強化學習加形式驗證這條路，不僅能在圍棋這類固定規則的棋類裡通關，完全可以遷移到深奧的抽象數學領域。

對研究人員和數學家來說，這意味著未來的科研工具正在成型。你不需要擔心 AI 給出的證明步驟是在胡言亂語，因為 Lean 會幫你把關。數學家可以用它來暴力驗證繁瑣的子命題，或者探索那些原本需要耗費數月甚至數年人工推導的猜想。

但也要看到它的侷限。目前的系統依然高度依賴人工把人類語言“翻譯”成形式化程式碼，沒有人工這一步預處理，系統根本不知道題目在說什麼。而且兩道組合題剃了光頭、部分題目耗時三天，說明機器在缺乏明確直覺引導和巨大搜索空間的離散數學問題上，依然會被算力消耗拖垮。但無論如何，人類在頂尖純邏輯思維上的領地，又被機器切走了一大塊。