在從圍棋到戰(zhàn)略棋類游戲的所有領(lǐng)域戰(zhàn)勝人類后，美國谷歌公司旗下的DeepMind表示，它即將在解決數(shù)學(xué)問題方面擊敗全球最優(yōu)秀的學(xué)生。
7月25日，DeepMind宣布，其人工智能（AI）系統(tǒng)已經(jīng)解答了本月在英國巴斯舉行的2024年國際數(shù)學(xué)奧林匹克競賽（IMO）6個題目中的4個。AI給出了嚴謹、循序漸進的證明，并由兩名頂級數(shù)學(xué)家打分，得分為28/42，這相當(dāng)于銀牌的成績，僅比金牌差1分。
“這顯然是一個非常重大的進步?！庇鴦虼髮W(xué)數(shù)學(xué)家Joseph Myers說。他與菲爾茲獎獲得者Tim Gowers一起，幫助挑選了今年IMO的原始題目并審查了這些解題方案。
DeepMind和其他公司正在競相讓機器最終提供證明，以解決數(shù)學(xué)領(lǐng)域的實質(zhì)性研究問題。該公司表示，IMO的題目已經(jīng)成為實現(xiàn)這一目標(biāo)的基準，并被視為機器學(xué)習(xí)的“重大挑戰(zhàn)”。
“這是AI系統(tǒng)首次達到獎牌級別的表現(xiàn)。”DeepMind負責(zé)AI科學(xué)的副總裁Pushmeet Kohli表示，“這是高級定理證明過程中的一座關(guān)鍵里程碑。”
今年1月，DeepMind的AI系統(tǒng)AlphaGeometry在解決一類IMO問題——歐幾里得幾何方面取得了獎牌級別的成績。這是第一個在整體測試中達到金牌水平的AI，包括代數(shù)、組合數(shù)學(xué)和數(shù)論。這些問題通常被認為比幾何更具挑戰(zhàn)性，解決它們將有資格獲得500萬美元獎金。
在最新研究中，研究人員使用AlphaGeometry2在20秒內(nèi)解決了幾何問題。DeepMind計算機科學(xué)家Thang Luong表示，該AI是他們創(chuàng)紀錄系統(tǒng)的改進版本，速度更快。
對于其他類型的問題，該團隊開發(fā)了一個名為AlphaProof的全新系統(tǒng)。新系統(tǒng)花了3天時間解決了競賽中的兩道代數(shù)題，外加一道數(shù)論題。不過，它無法解決組合數(shù)學(xué)領(lǐng)域的兩道題。
當(dāng)試圖用語言模型回答數(shù)學(xué)問題時，研究人員得到了喜憂參半的結(jié)果。有時，這些模型給出了正確答案，但無法合理解釋其推理；有時，它們會胡說八道。
據(jù)介紹，AlphaProof將語言模型與強化學(xué)習(xí)技術(shù)相結(jié)合，使用了DeepMind的AlphaZero系統(tǒng)，后者成功用于“狙擊”圍棋等游戲以及解決一些特定數(shù)學(xué)問題。
在強化學(xué)習(xí)中，神經(jīng)網(wǎng)絡(luò)通過試錯進行學(xué)習(xí)。當(dāng)它的答案可以被客觀指標(biāo)評估時，這種方法就很有效。為此，AlphaProof被訓(xùn)練用一種名為Lean的正式語言來閱讀和編寫證明，Lean被用于數(shù)學(xué)家常用的同名“證明助手”軟件包。AlphaProof在Lean軟件包中運行并測試其輸出是否正確，這有助于填充代碼中的一些步驟。
訓(xùn)練任何語言模型都需要大量數(shù)據(jù)，但Lean中幾乎沒有數(shù)學(xué)證明。DeepMind機器學(xué)習(xí)研究員Thomas Hubert表示，為了解決這個問題，團隊設(shè)計了一個額外網(wǎng)絡(luò)，試圖將現(xiàn)有的100萬個用自然語言編寫的問題轉(zhuǎn)化成Lean語言，但不包括人工編寫的解題方案。
許多Lean的翻譯都是荒謬的，但足夠多的翻譯足以讓AlphaProof開啟它的強化學(xué)習(xí)周期。Gowers說，結(jié)果遠遠好于預(yù)期。在某些情況下，AlphaProof似乎能夠提供額外的創(chuàng)造力，在無限的可能性中做出正確的選擇。但Gowers補充說，還需要進一步分析才能確定。
Myers表示，這些技術(shù)能否完善到在數(shù)學(xué)領(lǐng)域進行研究級別的工作，仍有待觀察。“它能擴展到其他類型的數(shù)學(xué)問題嗎？在那里可能沒有100萬個問題可以訓(xùn)練?！?/p>
來源：《中國科學(xué)報》
