《自然》雜志11月12日發(fā)表了一項(xiàng)重要成果:英國(guó)深度思維正式推出其開(kāi)發(fā)的“數(shù)學(xué)做題家AI”AlphaProof,其成功證明了復(fù)雜的數(shù)學(xué)定理,并在2024年國(guó)際數(shù)學(xué)奧林匹克競(jìng)賽(IMO)中取得了相當(dāng)于銀牌的優(yōu)異成績(jī)。這項(xiàng)研究展示了AI在高難度數(shù)學(xué)推理領(lǐng)域的顯著進(jìn)步。

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

這一突破被認(rèn)為是AI研究領(lǐng)域的又一個(gè)里程碑。這是因?yàn)橛酶咚礁?jìng)賽題目測(cè)試AI系統(tǒng),已成為評(píng)估其邏輯推理、抽象思維和解決問(wèn)題能力的重要標(biāo)準(zhǔn)。這類題目不僅要求嚴(yán)密的演繹推理,還涉及創(chuàng)造性策略和跨領(lǐng)域知識(shí)整合,遠(yuǎn)超普通問(wèn)答或模式識(shí)別任務(wù)。因此,能否在IMO等權(quán)威競(jìng)賽中取得好成績(jī),被視為衡量AI是否具備“類人”深度推理能力的關(guān)鍵試金石。

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

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

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