《自然》雜志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推理的局限，也為探索復雜數學猜想提供了新工具，更為未來人機協作攻克前沿科學難題開辟了現實路徑。其影響將輻射至理論計算機科學、自動定理證明乃至基礎數學研究等領域。
責任編輯：陸迪
