2024年7月25日 DeepMind在解決數(shù)學(xué)問題方面達(dá)到里程碑——人工智能的下一個重大挑戰(zhàn) AlphaProof在今年的數(shù)學(xué)奧林匹克(Mathematical Olympiad)問題上展示了自己的實力——在用人工智能創(chuàng)建實質(zhì)性證明的競賽中邁出了一步。 大衛(wèi)·卡斯特爾韋奇主題為“2016年第五十七屆國際數(shù)學(xué)奧林匹克”的郵票小型張?zhí)貙?國際數(shù)學(xué)奧林匹克中的問題來自幾個數(shù)學(xué)領(lǐng)域。鳴謝:David Wong/南華早報via Getty 谷歌DeepMind在從圍棋游戲到戰(zhàn)略棋盤游戲的所有領(lǐng)域都擊敗了人類，現(xiàn)在它表示，它即將在解決數(shù)學(xué)問題方面擊敗世界頂級學(xué)生。 這家總部位于倫敦的機(jī)器學(xué)習(xí)公司于7月25日宣布，其人工智能(AI)系統(tǒng)已經(jīng)解決了本月在英國巴斯舉行的2024年國際數(shù)學(xué)奧林匹克(IMO)上向?qū)W校學(xué)生提出的六個問題中的四個。人工智能產(chǎn)生了嚴(yán)格的、一步一步的證明，由兩名頂級數(shù)學(xué)家標(biāo)記，并獲得了28/42的分?jǐn)?shù)——離金牌范圍僅差一分。 “這顯然是一個非常重大的進(jìn)步，”英國劍橋的數(shù)學(xué)家約瑟夫·邁爾斯說，他與菲爾茲獎獲得者蒂姆·高爾斯一起審查了這些解決方案，并幫助選擇了今年IMO的原始問題。 DeepMind和其他公司正在進(jìn)行一場競賽，最終讓機(jī)器給出證明，解決數(shù)學(xué)中的實質(zhì)性研究問題。該公司表示，在國際數(shù)學(xué)家大會(IMO)上設(shè)置的問題——世界上最重要的年輕數(shù)學(xué)家競賽——已經(jīng)成為實現(xiàn)這一目標(biāo)的進(jìn)展基準(zhǔn)，并被視為機(jī)器學(xué)習(xí)的“重大挑戰(zhàn)”。 “這是第一次任何人工智能系統(tǒng)能夠?qū)崿F(xiàn)獎牌級別的性能”，DeepMind負(fù)責(zé)科學(xué)的人工智能副總裁Pushmeet Kohli在向記者發(fā)布的一份簡報中說?！斑@是構(gòu)建高級定理證明器的旅程中的一個關(guān)鍵里程碑，”Kohli說。 分支 就在幾個月前的一月份，DeepMind系統(tǒng)AlphaGeometry在解決一種類型的IMO問題(歐幾里德幾何中的問題)時，已經(jīng)達(dá)到了獎?wù)芦@得者級別的性能。第一個在整體測試中表現(xiàn)出金牌水平的人工智能——包括代數(shù)、組合學(xué)和數(shù)論等通常被認(rèn)為比幾何更具挑戰(zhàn)性的問題——將有資格獲得500萬美元的獎勵，稱為人工智能數(shù)學(xué)奧林匹克(AIMO)獎。(該獎項有嚴(yán)格的標(biāo)準(zhǔn)，如開源代碼和有限的計算能力，這意味著DeepMind目前的努力不符合條件。) 在他們最近的努力中，研究人員使用AlphaGeometry2在20秒內(nèi)解決了幾何問題；DeepMind計算機(jī)科學(xué)家Thang Luong表示，人工智能是他們創(chuàng)紀(jì)錄系統(tǒng)的改進(jìn)和更快版本。 對于其他類型的問題，該團(tuán)隊開發(fā)了一個全新的系統(tǒng)，名為AlphaProof。AlphaProof解決了競賽的兩個代數(shù)問題，外加一個數(shù)論問題，花了三天時間。(實際IMO的參與者有兩次會議，每次4.5小時。)它無法解決數(shù)學(xué)的另一個領(lǐng)域組合學(xué)中的兩個問題。一名羅馬尼亞選手在第63屆國際數(shù)學(xué)奧林匹克競賽中獲得金牌的特寫鏡頭。 數(shù)學(xué)奧林匹克是世界上學(xué)齡數(shù)學(xué)天才的首要競賽。信用:MoiraM/Alamy當(dāng)試圖用語言模型回答數(shù)學(xué)問題時，研究人員獲得了喜憂參半的結(jié)果——這種類型的系統(tǒng)為ChatGPT等聊天機(jī)器人提供了動力。有時，模型給出了正確的答案，但不能合理地解釋他們的推理，有時他們吐出廢話。 就在上周，來自軟件公司Numina和HuggingFace的一組研究人員使用一種語言模型贏得了AIMO中級“進(jìn)步獎”，該獎基于IMO問題的簡化版本。這些公司將他們的整個系統(tǒng)開源，供其他研究人員下載。但是獲獎?wù)吒嬖V《自然》雜志，要解決更難的問題，單靠語言模型可能還不夠。 a級求解器 AlphaProof將語言模型與強(qiáng)化學(xué)習(xí)技術(shù)相結(jié)合，使用該公司已成功用于攻擊圍棋等游戲以及一些特定數(shù)學(xué)問題的“AlphaZero”引擎。在強(qiáng)化學(xué)習(xí)中，神經(jīng)網(wǎng)絡(luò)通過反復(fù)試驗來學(xué)習(xí)。當(dāng)它的答案可以用一些客觀的度量標(biāo)準(zhǔn)來評估時，這種方法很有效。出于這個目的，AlphaProof被訓(xùn)練用一種叫做Lean的正式語言讀寫證明，這種語言被用在數(shù)學(xué)家流行的同名軟件包“證明助手”中。為此，AlphaProof通過在精益包中運(yùn)行它們來測試其輸出是否正確，這有助于填充代碼中的一些步驟。 訓(xùn)練任何語言模型都需要大量的數(shù)據(jù)，但是在精益中幾乎沒有可用的數(shù)學(xué)證明。DeepMind機(jī)器學(xué)習(xí)研究人員托馬斯·休伯特(Thomas Hubert)說，為了克服這個問題，該團(tuán)隊設(shè)計了一個額外的網(wǎng)絡(luò)，試圖將現(xiàn)有的用自然語言寫的100萬個問題的記錄翻譯成精益，但不包括人類寫的解決方案，他是AlphaProof的開發(fā)負(fù)責(zé)人之一。“我們的方法是，我們能學(xué)會證明嗎，即使我們最初沒有訓(xùn)練人類書寫的證明？”(該公司對圍棋采取了類似的方法，其人工智能通過與自己對弈來學(xué)習(xí)下棋，而不是像人類那樣。) 魔法鑰匙 許多精益翻譯都是無意義的，但足夠好了，足以讓AlphaProof開始它的強(qiáng)化學(xué)習(xí)周期。高爾斯在新聞發(fā)布會上說，結(jié)果比預(yù)期好得多。“IMO中的許多問題都有這種神奇的特性。巴黎法蘭西學(xué)院的高爾斯說:“這個問題起初看起來很難，直到你找到一把神奇的鑰匙來解開它。 在某些情況下，AlphaProof似乎能夠提供額外的創(chuàng)造性飛躍，在無限大的可能性范圍內(nèi)提供正確的一步。高爾斯補(bǔ)充說，但是還需要進(jìn)一步的分析來確定答案是否沒有看起來那么令人驚訝。在DeepMind的AlphaGo機(jī)器人在2016年擊敗世界頂級人類圍棋選手的著名比賽中采取了令人驚訝的“37步棋”之后，類似的辯論隨之而來——這是人工智能的分水嶺。 邁爾斯在新聞發(fā)布會上說，這些技術(shù)是否能完善到在數(shù)學(xué)領(lǐng)域做研究水平的工作還有待觀察?！八苎由斓狡渌N類的數(shù)學(xué)嗎？在這些數(shù)學(xué)中，可能沒有一百萬個問題需要訓(xùn)練?！? DeepMind計算機(jī)科學(xué)家大衛(wèi)·西爾弗(David Silver)說，“我們現(xiàn)在可以證明，他們不是公開的研究問題，而是至少對世界上最優(yōu)秀的年輕數(shù)學(xué)家來說非常具有挑戰(zhàn)性的問題，”他在2010年代中期是開發(fā)AlphaGo的主要研究人員。doi::https:///10.1038/d41586-024-02441-2