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