《自然》雜志12日發(fā)表了一項重要成果：英國深度思維正式推出其開發(fā)的“數(shù)學做題家AI”AlphaProof，其成功證明了復雜的數(shù)學定理，并在2024年國際數(shù)學奧林匹克競賽（IMO）中取得了相當于銀牌的優(yōu)異成績。這項研究展示了AI在高難度數(shù)學推理領域的顯著進步。

深度思維2004年曾透露其混合AI系統(tǒng)在同年的IMO競賽中表現(xiàn)優(yōu)異，僅差1分就能摘得金牌。而今正式發(fā)布論文推出并詳解該AI系統(tǒng)。

這一突破被認為是AI研究領域的又一個里程碑。這是因為用高水平競賽題目測試AI系統(tǒng)，已成為評估其邏輯推理、抽象思維和解決問題能力的重要標準。這類題目不僅要求嚴密的演繹推理，還涉及創(chuàng)造性策略和跨領域知識整合，遠超普通問答或模式識別任務。因此，能否在IMO等權威競賽中取得好成績，被視為衡量AI是否具備“類人”深度推理能力的關鍵試金石。

目前，許多大型語言模型雖然具備強大的生成能力，卻難以驗證其推理是否正確，因為它們通?；诜钦降淖匀徽Z言進行訓練和輸出，缺乏嚴格的邏輯結構。為應對這一挑戰(zhàn)，深度思維團隊將強化學習引入一個名為Lean的正式數(shù)學證明環(huán)境，在該系統(tǒng)中，所有推理步驟都必須符合形式化邏輯規(guī)則，從而能夠被自動驗證。

AlphaProof是專為證明數(shù)學命題而設計的系統(tǒng)。團隊首先對約8000萬個數(shù)學命題進行了自動形式化處理，隨后利用強化學習讓AlphaProof在這些命題中探索有效的證明路徑。結果顯示，該系統(tǒng)不僅超越了此前最先進的AI模型在歷史IMO題目上的表現(xiàn)，還在今年的競賽中聯(lián)合另一款專攻幾何的AI系統(tǒng)AlphaGeometry，共同解決了6道題中的4道，達到銀牌水平。

盡管AlphaProof在競賽級數(shù)學推理方面展現(xiàn)出驚人能力，但團隊坦承其目前仍存在局限，例如在處理某些非標準或高度抽象的數(shù)學問題時表現(xiàn)不足。他們指出，未來的研究應聚焦于拓展系統(tǒng)的通用性和適應性。一旦這些障礙被克服，AlphaProof有望成為協(xié)助數(shù)學家攻克復雜數(shù)學難題的有力工具，推動形式化證明與AI的深度融合。

【總編輯圈點】

數(shù)學家長期以來依賴計算工具輔助解決復雜問題和構建嚴謹證明，而AI有望加速這一過程?，F(xiàn)在，AI在形式化推理領域邁出了關鍵一步，不同于依賴模糊語言模型的通用AI，最新成果在嚴格邏輯框架中運行，其每一步推理均可驗證，極大提升了結果的可靠性。此舉不僅突破了AI推理的局限，也為探索復雜數(shù)學猜想提供了新工具，更為未來人機協(xié)作攻克前沿科學難題開辟了現(xiàn)實路徑。其影響將輻射至理論計算機科學、自動定理證明乃至基礎數(shù)學研究等領域。