《自然》雜志12日發表了一項重要成果:英國深度思維正式推出其開發的“數學做題家AI”AlphaProof,其成功證明了復雜的數學定理,并在2024年國際數學奧林匹克競賽(IMO)中取得了相當于銀牌的優異成績。這項研究展示了AI在高難度數學推理領域的顯著進步。
深度思維2004年曾透露其混合AI系統在同年的IMO競賽中表現優異,僅差1分就能摘得金牌。而今正式發布論文推出并詳解該AI系統。
這一突破被認為是AI研究領域的又一個里程碑。這是因為用高水平競賽題目測試AI系統,已成為評估其邏輯推理、抽象思維和解決問題能力的重要標準。這類題目不僅要求嚴密的演繹推理,還涉及創造性策略和跨領域知識整合,遠超普通問答或模式識別任務。因此,能否在IMO等權威競賽中取得好成績,被視為衡量AI是否具備“類人”深度推理能力的關鍵試金石。
目前,許多大型語言模型雖然具備強大的生成能力,卻難以驗證其推理是否正確,因為它們通常基于非正式的自然語言進行訓練和輸出,缺乏嚴格的邏輯結構。為應對這一挑戰,深度思維團隊將強化學習引入一個名為Lean的正式數學證明環境,在該系統中,所有推理步驟都必須符合形式化邏輯規則,從而能夠被自動驗證。
AlphaProof是專為證明數學命題而設計的系統。團隊首先對約8000萬個數學命題進行了自動形式化處理,隨后利用強化學習讓AlphaProof在這些命題中探索有效的證明路徑。結果顯示,該系統不僅超越了此前最先進的AI模型在歷史IMO題目上的表現,還在今年的競賽中聯合另一款專攻幾何的AI系統AlphaGeometry,共同解決了6道題中的4道,達到銀牌水平。
盡管AlphaProof在競賽級數學推理方面展現出驚人能力,但團隊坦承其目前仍存在局限,例如在處理某些非標準或高度抽象的數學問題時表現不足。他們指出,未來的研究應聚焦于拓展系統的通用性和適應性。一旦這些障礙被克服,AlphaProof有望成為協助數學家攻克復雜數學難題的有力工具,推動形式化證明與AI的深度融合。
【總編輯圈點】
數學家長期以來依賴計算工具輔助解決復雜問題和構建嚴謹證明,而AI有望加速這一過程。現在,AI在形式化推理領域邁出了關鍵一步,不同于依賴模糊語言模型的通用AI,最新成果在嚴格邏輯框架中運行,其每一步推理均可驗證,極大提升了結果的可靠性。此舉不僅突破了AI推理的局限,也為探索復雜數學猜想提供了新工具,更為未來人機協作攻克前沿科學難題開辟了現實路徑。其影響將輻射至理論計算機科學、自動定理證明乃至基礎數學研究等領域。
責任編輯:陸迪