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