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

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

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

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

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

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

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