IMO中的問題涵蓋了多個數(shù)學(xué)領(lǐng)域,。但大多數(shù)IMO問題都是用英語編寫的,，需要翻譯成AI能理解和驗證的編程語言，才能讓AI進(jìn)行機(jī)器學(xué)習(xí),。圖片來源：《自然》網(wǎng)站【今日視點】繼擊敗人類圍棋大師和戰(zhàn)略棋盤游戲頂尖高手之后,，谷歌“深度思維”公司人工智能（AI）系統(tǒng)在英國巴斯舉行的2024年國際數(shù)學(xué)奧林匹克競賽（IMO）上,，僅以1分之差與金牌失之交臂，獲得了銀牌,。這是AI選手首次登上IMO領(lǐng)獎臺,。英國《自然》雜志網(wǎng)站在7月27日的報道中指出，“深度思維”正與其他公司競相解決數(shù)學(xué)領(lǐng)域的疑難問題,。近年來,，IMO被廣泛認(rèn)為是對機(jī)器學(xué)習(xí)的一個挑戰(zhàn)，也是衡量AI系統(tǒng)高級數(shù)學(xué)推理能力的理想基準(zhǔn),。AI系統(tǒng)在今年IMO中的精彩表現(xiàn),，標(biāo)志著其即將再下一城：在解決數(shù)學(xué)難題方面擊敗世界頂尖學(xué)生,。首登領(lǐng)獎臺“深度思維”公司訓(xùn)練了一個專門用于解答數(shù)學(xué)奧賽考題的AI系統(tǒng)，成功解答了6道競賽題中的4道,，獲得28分（滿分42分）,，達(dá)到本次比賽銀牌獲得者的水平。該系統(tǒng)包括解答數(shù)學(xué)推理問題的模型AlphaProof和解答幾何問題的模型AlphaGeometry的升級版AlphaGeometry 2,。其中,，AlphaGeometry 2解決了一個幾何問題，而AlphaProof則解答了兩個代數(shù)問題和一個數(shù)論問題,。今年1月份,，AlphaGeometry在解決歐幾里得幾何問題上，就已表現(xiàn)出獎牌級選手的水平,。在今年的IMO比賽前,，AlphaGeometry 2已經(jīng)能夠解決過去25年里83%的IMO幾何問題，而其“前身”僅能解決53%,?！吧疃人季S”公司AI科學(xué)副總裁普什米特·科利指出，這是AI系統(tǒng)首次達(dá)到獲IMO獎牌級別的性能。IMO主席格雷戈爾·多利納爾也表示,，AI最終將能比人類更好地解決大多數(shù)數(shù)學(xué)問題,，其進(jìn)步速度令人驚嘆。幾乎同一時間,，軟件公司Numina的科學(xué)家使用語言模型，贏得了AI數(shù)學(xué)奧林匹克獎（AIMO）的首個“進(jìn)步獎”,。但Numina團(tuán)隊在獲獎后表示,，要解決更難的數(shù)學(xué)問題，僅靠語言模型可能還不夠,。與自己對抗AlphaProof是一個自學(xué)習(xí)系統(tǒng),，其核心創(chuàng)新在于結(jié)合預(yù)訓(xùn)練語言模型與AlphaZero強(qiáng)化學(xué)習(xí)算法的策略。強(qiáng)化學(xué)習(xí)是機(jī)器學(xué)習(xí)領(lǐng)域一種重要的學(xué)習(xí)范式,，系統(tǒng)可通過多次嘗試找到自己的解題方法。這種方法需要用AI能理解和驗證的語言編寫大量問題,，而大多數(shù)IMO問題都是用英語編寫的。為解決這個問題,，“深度思維”團(tuán)隊托馬斯·赫伯特及其同事使用谷歌的大語言模型Gemini，將這些問題翻譯成一種名為Lean的編程語言,，以供AI進(jìn)行學(xué)習(xí)。AlphaProof使用經(jīng)過微調(diào)的Gemini模型,，自動將數(shù)學(xué)問題轉(zhuǎn)換為Lean語言,，從而創(chuàng)建了一個涵蓋不同難度級別的大型問題庫。在強(qiáng)化學(xué)習(xí)階段,，系統(tǒng)每驗證一個證明,，就用它來強(qiáng)化AlphaProof的語言模型，提高其解決后續(xù)更具挑戰(zhàn)性問題的能力,。赫伯特表示,，在挑戰(zhàn)圍棋游戲時，他們也采用了類似的方法：AI通過與自己對抗,，來學(xué)習(xí)如何更好地玩游戲,。結(jié)果顯示，在某些情況下,，AlphaProof能夠在無限多的可能性中邁出正確的一步,，展現(xiàn)出“靈光一閃”的能力,。仍有改進(jìn)空間盡管AlphaProof的表現(xiàn)令人印象深刻，但其速度相對較慢,，解決3個問題耗費了3天時間，而人類參賽者僅需4個半小時,。此外,，它也未能回答兩個與組合數(shù)學(xué)有關(guān)的問題。英國數(shù)學(xué)家約瑟夫·邁爾斯審查了AI在本次IMO比賽中給出的答案,。他指出,，AlphaProof采取的這些技術(shù)能否予以完善還有待觀察。英國倫敦數(shù)學(xué)科學(xué)研究所何楊輝稱,，AlphaProof這樣的系統(tǒng)對于幫助數(shù)學(xué)家證明問題很有用,，但它無法幫助研究人員確定需要解決和研究的問題?！吧疃人季S”團(tuán)隊表示,，他們正繼續(xù)探索多種用于推進(jìn)數(shù)學(xué)推理的AI方法。未來,，數(shù)學(xué)研究者將與AI合作驗證假說,，嘗試新方法來解決長期未解決的數(shù)學(xué)難題。他們也希望AlphaProof能夠通過減少錯誤響應(yīng),，幫助改進(jìn)谷歌的大型語言模型,。（記者 劉 霞）來源：科技日報