谷歌DeepMind在國際數學奧林匹克競賽（IMO）中再獲突破，其研發的AlphaProof模型成功斬獲金牌。這一成果以完整論文形式發表于《自然》期刊，首次詳細披露了該系統的技術架構與訓練方法。值得注意的是，曾實現“無師自通”下棋的AlphaZero相關技術，在此次研究中被多次借鑒與改進。

項目核心團隊規模精簡，長期保持約十名成員，僅在IMO賽事臨近時擴充人手。突破性進展源于團隊成員、IMO金牌得主米克洛什·霍瓦特提出的創新方法：通過生成數學問題的多樣化變體，構建智能體的訓練環境。這些變體涵蓋簡化版本、推廣形式及結構類似的問題，使系統能在更廣泛的場景中積累解題經驗。

AlphaProof將數學證明轉化為強化學習任務，基于Lean定理證明器搭建訓練環境。每個數學命題被視為獨立關卡，系統需選擇策略推進證明進程。成功策略將生成新子目標，直至所有目標完成即證明成功。其核心采用30億參數的編碼器-解碼器Transformer模型，該模型需同時輸出策略建議與剩余步驟預估，優化計算資源分配效率。

搜索算法層面，系統在AlphaZero樹搜索基礎上引入AND-OR樹結構，可分解證明中的多重獨立條件為子問題逐個攻克。漸進采樣機制則允許在關鍵路徑探索更多策略。訓練數據構建分為三階段：首先用3000億token的代碼與數學文本預訓練模型；隨后通過Mathlib庫的30萬個人工證明微調；最終利用基于Gemini 1.5 Pro開發的翻譯系統，將約100萬道自然語言數學題轉化為8000萬道形式化問題，數據規模遠超現有集合。

主訓練階段消耗約8萬TPU日計算資源，系統通過持續嘗試證明或反證自動生成命題，成功案例用于更新神經網絡。即便形式化結果存在誤差，只要命題有效，系統仍能從中學習。測試階段采用雙循環機制：主循環處理大規模自動生成問題；測試時強化學習循環針對特定難題生成約40萬個變體，啟動獨立訓練進程積累解題洞察。

在2024年IMO賽事中，AlphaProof展現強大實力，成功解決代數與數論領域三道題目，其中包括僅5名選手完全攻克的最高難度試題P6。面對難題時，系統通過生成特殊變體（如限定有理數范圍、強化條件假設）進行專項訓練，每題需2-3日計算時間。團隊透露，賽事期間部分證明系統僅能確保銅牌成績，直至后臺運行的測試時強化學習完成三道完整證明，才最終鎖定金牌。

目前DeepMind已向科研界開放AlphaProof使用權限，多位數學家分享了試用體驗。羅格斯大學學者發現系統擅長發現反例，助力修正理論假設；伊利諾伊大學團隊用其驗證棘手引理，一分鐘內完成證明或找出定義漏洞；倫敦帝國理工學院測試費馬大定理證明時則遇到挑戰，顯示系統在處理全新數學概念時仍存在局限。

研究團隊指出，系統對Lean定理證明器的依賴構成雙重影響：活躍的社區支持推動其在成熟數學子領域表現優異，但證明器的持續演進也帶來環境不穩定性。數據局限性同樣突出，盡管變體生成技術取得進展，但創建真正原創的數學問題仍需突破。該成果為AI數學研究提供了新范式，其技術路徑印證了專家關于AI在封閉系統中超越人類潛力的預測。

論文全文鏈接：https://www.nature.com/articles/s41586-025-09833-y
相關技術討論：https://www.nature.com/articles/d41586-025-03585-5