科技日報北京11月12日電 （記者張夢然）《自然》雜志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”http://m.sq15.cn/show-11-28118-0.html
聲明：本網站為非營利性網站，本網頁內容由互聯網博主自發貢獻，不代表本站觀點，本站不承擔任何法律責任。天上不會到餡餅，請大家謹防詐騙！若有侵權等問題請及時與本網聯系，我們將在第一時間刪除處理。
上一篇： 立冬投票TOP1出爐！您最關心的“冬季代謝提升技巧”干貨來了
下一篇： 美國國際博士生人數目前保持穩定