人工智能領域迎來重大突破——Google DeepMind開發(fā)的AlphaProof模型成為首個在國際數(shù)學奧林匹克競賽（IMO）中達到銀牌水平的AI系統(tǒng)，相關(guān)研究成果登上權(quán)威科學期刊《自然》。這一成果被學界視為AI在復雜推理領域邁出的關(guān)鍵一步，標志著自動化系統(tǒng)已具備攻克傳統(tǒng)難題的潛力。

研究團隊通過將數(shù)學定理證明轉(zhuǎn)化為強化學習任務，構(gòu)建了獨特的訓練框架。模型首先在包含3000億token的數(shù)學與代碼語料庫中進行預訓練，掌握符號邏輯與基礎數(shù)學表達結(jié)構(gòu)。隨后，利用約30萬條Lean證明器數(shù)據(jù)開展監(jiān)督微調(diào)，使其理解形式化語法。為解決訓練數(shù)據(jù)不足的問題，研究團隊開發(fā)了基于Gemini模型的自動形式化系統(tǒng)，生成涵蓋代數(shù)、數(shù)論等領域的8000萬個形式化問題，為強化學習提供核心素材。

AlphaProof的核心創(chuàng)新在于"測試時強化學習"（TTRL）機制。當遇到新問題時，系統(tǒng)會生成數(shù)千個結(jié)構(gòu)相似的變體進行短期自我訓練，再將優(yōu)化后的策略應用于原題求解。這種"臨場學習"方式使模型在多項基準測試中的解題率提升10%-15%。主訓練階段累計消耗約8萬TPU天計算資源，通過不斷嘗試證明、驗證結(jié)果、更新策略的循環(huán)，逐步掌握復雜推理模式。

在2024年IMO模擬測試中，AlphaProof獨立證明了三道非幾何難題，包括全場最難題目P6。配合負責幾何題的AlphaGeometry 2系統(tǒng)，兩者合計獲得28分（滿分42分），達到人類參賽者的銀牌水平。這是AI首次在國際數(shù)學奧林匹克競賽中達到獎牌標準，相比此前僅能解決中學水平題目的系統(tǒng)，展現(xiàn)了基于經(jīng)驗學習的形式化系統(tǒng)在復雜推理領域的突破。

伊利諾伊大學厄巴納-香檳分校助理教授Talia Ringer在同期發(fā)表的觀點文章中指出，AlphaProof是她使用過的首款真正實用的AI工具。其證明質(zhì)量高度可靠，每步推理都能通過證明輔助工具獲得即時反饋，避免了自然語言模型常見的模糊與錯誤。盡管存在計算成本高、推理速度慢等局限，但這一成果為"可驗證的機器推理"提供了可行路徑。

研究團隊強調(diào)，AlphaProof的核心價值在于將強化學習與形式化邏輯系統(tǒng)結(jié)合，實現(xiàn)了可驗證的高水平數(shù)學推理。與自然語言模型不同，其每步邏輯均通過Lean驗證器審查，為AI在科學推理中的應用奠定基礎。未來工作將聚焦優(yōu)化模型效率、降低算力需求，并探索形式化學習在數(shù)學及其他科學領域的應用，同時開發(fā)交互式工具促進人機協(xié)作。

論文鏈接：https://www.nature.com/articles/s41586-025-09833-y
新聞與觀點文章鏈接：https://www.nature.com/articles/d41586-025-03585-5