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