在從圍棋到戰略棋類(lèi)游戲的所有領(lǐng)域戰勝人類(lèi)后，美國谷歌公司旗下的DeepMind表示，它即將在解決數學(xué)問(wèn)題方面擊敗全球最優(yōu)秀的學(xué)生。

7月25日，DeepMind宣布，其人工智能（AI）系統已經(jīng)解答了本月在英國巴斯舉行的2024年國際數學(xué)奧林匹克競賽（IMO）6個(gè)題目中的4個(gè)。AI給出了嚴謹、循序漸進(jìn)的證明，并由兩名頂級數學(xué)家打分，得分為28/42，這相當于銀牌的成績(jì)，僅比金牌差1分。

“這顯然是一個(gè)非常重大的進(jìn)步?！庇鴦虼髮W(xué)數學(xué)家Joseph Myers說(shuō)。他與菲爾茲獎獲得者Tim Gowers一起，幫助挑選了今年IMO的原始題目并審查了這些解題方案。

DeepMind和其他公司正在競相讓機器最終提供證明，以解決數學(xué)領(lǐng)域的實(shí)質(zhì)性研究問(wèn)題。該公司表示，IMO的題目已經(jīng)成為實(shí)現這一目標的基準，并被視為機器學(xué)習的“重大挑戰”。

“這是AI系統首次達到獎牌級別的表現?！盌eepMind負責AI科學(xué)的副總裁Pushmeet Kohli表示，“這是高級定理證明過(guò)程中的一座關(guān)鍵里程碑?！?/p>

今年1月，DeepMind的AI系統AlphaGeometry在解決一類(lèi)IMO問(wèn)題——歐幾里得幾何方面取得了獎牌級別的成績(jì)。這是第一個(gè)在整體測試中達到金牌水平的AI，包括代數、組合數學(xué)和數論。這些問(wèn)題通常被認為比幾何更具挑戰性，解決它們將有資格獲得500萬(wàn)美元獎金。

在最新研究中，研究人員使用AlphaGeometry2在20秒內解決了幾何問(wèn)題。DeepMind計算機科學(xué)家Thang Luong表示，該AI是他們創(chuàng )紀錄系統的改進(jìn)版本，速度更快。

對于其他類(lèi)型的問(wèn)題，該團隊開(kāi)發(fā)了一個(gè)名為AlphaProof的全新系統。新系統花了3天時(shí)間解決了競賽中的兩道代數題，外加一道數論題。不過(guò)，它無(wú)法解決組合數學(xué)領(lǐng)域的兩道題。

當試圖用語(yǔ)言模型回答數學(xué)問(wèn)題時(shí)，研究人員得到了喜憂(yōu)參半的結果。有時(shí)，這些模型給出了正確答案，但無(wú)法合理解釋其推理；有時(shí)，它們會(huì )胡說(shuō)八道。

據介紹，AlphaProof將語(yǔ)言模型與強化學(xué)習技術(shù)相結合，使用了DeepMind的AlphaZero系統，后者成功用于“狙擊”圍棋等游戲以及解決一些特定數學(xué)問(wèn)題。

在強化學(xué)習中，神經(jīng)網(wǎng)絡(luò )通過(guò)試錯進(jìn)行學(xué)習。當它的答案可以被客觀(guān)指標評估時(shí)，這種方法就很有效。為此，AlphaProof被訓練用一種名為L(cháng)ean的正式語(yǔ)言來(lái)閱讀和編寫(xiě)證明，Lean被用于數學(xué)家常用的同名“證明助手”軟件包。AlphaProof在Lean軟件包中運行并測試其輸出是否正確，這有助于填充代碼中的一些步驟。

訓練任何語(yǔ)言模型都需要大量數據，但Lean中幾乎沒(méi)有數學(xué)證明。DeepMind機器學(xué)習研究員Thomas Hubert表示，為了解決這個(gè)問(wèn)題，團隊設計了一個(gè)額外網(wǎng)絡(luò )，試圖將現有的100萬(wàn)個(gè)用自然語(yǔ)言編寫(xiě)的問(wèn)題轉化成Lean語(yǔ)言，但不包括人工編寫(xiě)的解題方案。

許多Lean的翻譯都是荒謬的，但足夠多的翻譯足以讓AlphaProof開(kāi)啟它的強化學(xué)習周期。Gowers說(shuō)，結果遠遠好于預期。在某些情況下，AlphaProof似乎能夠提供額外的創(chuàng )造力，在無(wú)限的可能性中做出正確的選擇。但Gowers補充說(shuō)，還需要進(jìn)一步分析才能確定。

Myers表示，這些技術(shù)能否完善到在數學(xué)領(lǐng)域進(jìn)行研究級別的工作，仍有待觀(guān)察?！八軘U展到其他類(lèi)型的數學(xué)問(wèn)題嗎？在那里可能沒(méi)有100萬(wàn)個(gè)問(wèn)題可以訓練?！?/p>

來(lái)源：《中國科學(xué)報》