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