Google DeepMind AlphaProof 登上《自然》期刊：AI 首度達到國際數學奧林匹克銀牌水準
Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning — Google DeepMind AlphaProof published in Nature
Google DeepMind 的重磅論文《以強化學習進行奧林匹克等級的形式化數學推理》（Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning）已正式刊登於頂尖科學期刊 《自然》（Nature），詳細記錄了 AI 系統 AlphaProof 如何首度在國際數學奧林匹克（IMO）競賽中達到銀牌水準的完整技術路徑。
歷史性成就：2024 IMO 六題答對四題
在 IMO 2024 的競賽中，AlphaProof 與 AlphaGeometry 2 組合解出了六道題目中的四題，累計得分 28 分（滿分 42 分），位於銀牌得主區間，距金牌門檻僅差 1 分。
最令人矚目的是，AlphaProof 成功解出了 P6——本屆 IMO 最難的一道題，全體 609 名參賽者中僅有 5 人拿到滿分 7 分。
形式化語言：零幻覺的數學 AI
AlphaProof 與一般大型語言模型（LLM）的根本差異在於：它的輸出是形式化語言（Lean 定理證明器語法），而非自然語言。
這意味著每一步推導均可由電腦自動驗證，不可能產生看似正確實則有誤的「幻覺」解答。對比 GPT-5.4 等模型在數學競賽中偶有隱藏邏輯錯誤的問題，AlphaProof 的正確率達到 100%。
技術核心：強化學習 × 自動形式化
AlphaProof 融合了三項關鍵技術：
- 自動形式化（Auto-formalization）：將 8,000 萬道自然語言數學題轉換為 Lean 語言，建立龐大訓練語料庫
- AlphaZero RL 框架：借鑑 AlphaZero 在棋類遊戲自我對弈的學習機制，讓模型通過反覆嘗試與驗證習得數學推理技能
- 測試時強化學習（TTRL）：在面對競賽題目時，系統自動生成數百萬道簡化版變體問題，逐步逼近解答
意義與局限
論文通訊作者強調，AlphaProof 目前的限制之一是解題所需的計算時間遠超人類選手（比賽是限時完成的）。此外，系統依賴預先形式化的輸入，尚無法端對端地從原始數學題文字直接輸出完整 Lean 證明。
儘管如此，這項研究被數學界視為里程碑：它首度用同行審查的方式確立了 AI 系統能夠在競賽等級的數學推理上媲美頂尖人類選手，為 AI 輔助數學研究、自動定理證明乃至科學發現打開了新的想像空間。