·越來(lái)越多的數(shù)學(xué)研究者關(guān)注人工智能對(duì)該領(lǐng)域的影響，在各種討論會(huì)上辯論，采用不同的AI工具嘗試解答數(shù)學(xué)問(wèn)題。
·數(shù)學(xué)是機(jī)器學(xué)習(xí)能做什么或不能做什么的試金石。推理是數(shù)學(xué)過(guò)程的精髓，也是機(jī)器學(xué)習(xí)中尚未解決的關(guān)鍵問(wèn)題。神經(jīng)網(wǎng)絡(luò)以某種方式直觀地辨別出了數(shù)學(xué)真理，但其邏輯“原因”卻遠(yuǎn)非那么明顯。
(相關(guān)資料圖)
加州理工學(xué)院和麻省理工學(xué)院研究者發(fā)布用大語(yǔ)言模型證明數(shù)學(xué)定理的論文。
最近一段時(shí)間，人工智能似乎在數(shù)學(xué)領(lǐng)域取得了進(jìn)展，盡管一開(kāi)始大語(yǔ)言模型被看作并不是特別適合數(shù)學(xué)推理。
上周，英偉達(dá)數(shù)學(xué)家Jim Fan轉(zhuǎn)發(fā)了加州理工學(xué)院和麻省理工學(xué)院研究者用ChatGPT證明數(shù)學(xué)定理的論文，稱(chēng)數(shù)學(xué)的AI Copilot（副駕駛）時(shí)代已經(jīng)到來(lái)，未來(lái)人工智能將能夠發(fā)現(xiàn)數(shù)學(xué)定理。這篇論文構(gòu)建了一個(gè)基于大語(yǔ)言模型的定理證明器，為解決大語(yǔ)言模型幻覺(jué)方面的缺陷開(kāi)辟了一條新途徑。
幾天前，數(shù)學(xué)家、菲爾茲獎(jiǎng)得主陶哲軒表示，他最近在解決一個(gè)數(shù)學(xué)難題時(shí)“使用了GPT-4”，“它給我提供了最終的解題思路，接下來(lái)我只需要繼續(xù)計(jì)算就行?！睘榱私o更多研究者參考，他曬出了自己和GPT-4的聊天記錄。
如今，越來(lái)越多的數(shù)學(xué)研究者關(guān)注人工智能對(duì)該領(lǐng)域的影響，他們?cè)诟鞣N討論會(huì)上辯論，采用不同的AI工具嘗試解答數(shù)學(xué)問(wèn)題。根據(jù)《紐約時(shí)報(bào)》最近對(duì)一些數(shù)學(xué)家的采訪，他們正在努力應(yīng)對(duì)人工智能這一最新變革力量。數(shù)千年來(lái)，數(shù)學(xué)家們已經(jīng)適應(yīng)了邏輯和推理方面的最新進(jìn)展，他們?yōu)槿斯ぶ悄茏龊脺?zhǔn)備了嗎？
數(shù)學(xué)家和計(jì)算機(jī)科學(xué)家一起開(kāi)會(huì)
兩千多年來(lái)，數(shù)學(xué)家歐幾里得的文本一直是數(shù)學(xué)論證和推理的典范?？▋?nèi)基梅隆大學(xué)邏輯學(xué)家杰里米·阿維加德（Jeremy Avigad）在接受采訪時(shí)說(shuō)：“眾所周知，歐幾里得以近乎詩(shī)意的‘定義（definitions）’開(kāi)始。”?“然后，他在此基礎(chǔ)上建立了當(dāng)時(shí)的數(shù)學(xué)，使用基本概念、定義和先驗(yàn)定理，以每一個(gè)后續(xù)步驟‘清楚地遵循’之前的步驟來(lái)證明事物?！卑⒕S加德說(shuō)，有人抱怨歐幾里得的一些“明顯”步驟并不明顯，但該系統(tǒng)仍然有效。
但到了20世紀(jì)，數(shù)學(xué)家不再愿意將數(shù)學(xué)建立在這種直觀的幾何基礎(chǔ)上。相反，他們開(kāi)發(fā)了正式的系統(tǒng)——精確的符號(hào)表示、機(jī)械規(guī)則。最終，這種形式化使得數(shù)學(xué)能夠轉(zhuǎn)化為計(jì)算機(jī)代碼。1976年，四色定理（該定理指出四種顏色足以填充地圖，因此沒(méi)有兩個(gè)相鄰區(qū)域具有相同的顏色）成為第一個(gè)借助計(jì)算強(qiáng)力證明的主要定理。
現(xiàn)在，人工智能來(lái)了。2019年，曾供職于谷歌、現(xiàn)供職于灣區(qū)一家初創(chuàng)企業(yè)的計(jì)算機(jī)科學(xué)家克里斯蒂安·塞格迪（Christian Szegedy）預(yù)測(cè)，計(jì)算機(jī)系統(tǒng)將在10年內(nèi)趕上或超過(guò)人類(lèi)最優(yōu)秀數(shù)學(xué)家解決問(wèn)題的能力。去年他將目標(biāo)年份修改為2026年。
普林斯頓高等研究院數(shù)學(xué)家、2018年菲爾茲獎(jiǎng)獲得者阿克謝·文卡特什（Akshay Venkatesh）目前對(duì)使用人工智能不感興趣，但他熱衷于談?wù)摗?“我希望我的學(xué)生意識(shí)到他們所處的領(lǐng)域?qū)?huì)發(fā)生很大的變化。”他在去年的一次采訪中說(shuō)。最近他又補(bǔ)充說(shuō)：“我并不反對(duì)深思熟慮和刻意使用技術(shù)來(lái)支持我們?nèi)祟?lèi)的理解。但我堅(jiān)信，留心我們使用它的方式至關(guān)重要。”
今年2月，阿維加德參加了在加州大學(xué)洛杉磯分校純數(shù)學(xué)與應(yīng)用數(shù)學(xué)研究所舉辦的“機(jī)器輔助證明”研討會(huì)。這次聚會(huì)吸引了數(shù)學(xué)家和計(jì)算機(jī)科學(xué)家這一不尋常的組合。該研討會(huì)的主要組織者是陶哲軒，他曾在一篇博客中稱(chēng)，2026年AI將與搜索和符號(hào)數(shù)學(xué)工具相結(jié)合，成為數(shù)學(xué)研究中值得信賴(lài)的合著者。陶指出，直到最近幾年，數(shù)學(xué)家們才開(kāi)始擔(dān)心人工智能的潛在威脅，無(wú)論是對(duì)數(shù)學(xué)美學(xué)還是對(duì)他們自己，圈子成員現(xiàn)在正在提出這些問(wèn)題并探索“打破禁忌”。
幫助解決數(shù)學(xué)問(wèn)題的小工具們
如今，在飲食、睡眠、鍛煉方面，優(yōu)化人們生活的小工具十分普遍，威斯康星大學(xué)麥迪遜分校數(shù)學(xué)家喬丹·埃倫伯格（Jordan Ellenberg）在研討會(huì)休息期間接受采訪說(shuō)：“我們喜歡給自己增加一些東西，以便更容易把事情做好?！比斯ぶ悄苄」ぞ呖赡軐?duì)數(shù)學(xué)有同樣的作用。
其中一種數(shù)學(xué)小工具被稱(chēng)為證明助手或交互式定理證明器。數(shù)學(xué)家一步步將證明轉(zhuǎn)化為代碼，然后軟件程序檢查推理是否正確。驗(yàn)證在一個(gè)庫(kù)中積累，成為其他人可以查閱的動(dòng)態(tài)參考。阿維加德說(shuō)，這種“形式化”為當(dāng)今的數(shù)學(xué)奠定了基礎(chǔ)，“就像歐幾里得試圖編纂和整理數(shù)學(xué)、為他那個(gè)時(shí)代的數(shù)學(xué)奠定了基礎(chǔ)一樣?！?/p>
最近，開(kāi)源證明輔助系統(tǒng)Lean備受關(guān)注。Lean由計(jì)算機(jī)科學(xué)家萊昂納多·德·莫拉（Leonardo de Moura）開(kāi)發(fā)，當(dāng)時(shí)他在微軟，現(xiàn)在是亞馬遜的計(jì)算機(jī)科學(xué)家。Lean使用自動(dòng)推理，由所謂的“老式人工智能（GOFAI）”提供支持，即受邏輯啟發(fā)的符號(hào)人工智能。到目前為止，Lean社區(qū)已經(jīng)驗(yàn)證了一個(gè)翻轉(zhuǎn)球體的定理和一個(gè)有助于統(tǒng)一數(shù)學(xué)領(lǐng)域的關(guān)鍵定理等。
但證明助手也有缺點(diǎn)：它經(jīng)常抱怨不理解數(shù)學(xué)家輸入的定義、公理或推理步驟，因此它被戲稱(chēng)為“證明抱怨者”。所有這些抱怨都會(huì)讓研究變得很麻煩，但福特漢姆大學(xué)（Fordham University）的數(shù)學(xué)家希瑟·麥克白（Heather Macbeth）表示，提供逐行反饋的功能也使該系統(tǒng)對(duì)教學(xué)很有用。
今年春天，麥克白設(shè)計(jì)了一門(mén)“雙語(yǔ)”課程：她把黑板上提出的每一個(gè)問(wèn)題都翻譯成講義中的Lean代碼，學(xué)生們用Lean和普通語(yǔ)言提交作業(yè)答案。?“這給了它們信心?！丙溈税渍f(shuō)，因?yàn)樗鼈兪盏搅岁P(guān)于證明何時(shí)完成以及整個(gè)過(guò)程中的每一步是對(duì)還是錯(cuò)的即時(shí)反饋。
自從參加洛杉磯研討會(huì)以來(lái)，約翰·霍普金斯大學(xué)的數(shù)學(xué)家艾米麗·里爾（Emily Riehl）使用實(shí)驗(yàn)性證明輔助程序來(lái)形式化她之前與合著者發(fā)表的證明。在驗(yàn)證結(jié)束時(shí)，她說(shuō)：“我真的非常深入地理解了這個(gè)證明，比我以前理解的要深入得多。”
約翰·霍普金斯大學(xué)的數(shù)學(xué)家艾米麗·里爾一直在使用一個(gè)實(shí)驗(yàn)性證明助理程序。
卡內(nèi)基梅隆大學(xué)計(jì)算機(jī)科學(xué)家、亞馬遜學(xué)者馬利恩·海勒（Marijn Heule）使用另一種自動(dòng)推理工具，被他稱(chēng)為“暴力推理”，或者更專(zhuān)業(yè)地說(shuō)是可滿(mǎn)足性問(wèn)題求解器。他說(shuō)，只要用精心設(shè)計(jì)的代碼來(lái)說(shuō)明你想要找到哪個(gè)“奇異物體”，超級(jí)計(jì)算機(jī)網(wǎng)絡(luò)就會(huì)在搜索空間中進(jìn)行“翻攪”，并確定該實(shí)體是否存在。
還有一組工具使用機(jī)器學(xué)習(xí)，可以合成大量數(shù)據(jù)并檢測(cè)模式，但不擅長(zhǎng)邏輯、逐步推理。谷歌的DeepMind就設(shè)計(jì)了機(jī)器學(xué)習(xí)算法來(lái)解決蛋白質(zhì)折疊和國(guó)際象棋獲勝等問(wèn)題，在2021年《自然》雜志的一篇論文中，一個(gè)團(tuán)隊(duì)將他們的成果描述為“通過(guò)人工智能指導(dǎo)人類(lèi)直覺(jué)來(lái)推進(jìn)數(shù)學(xué)發(fā)展”。
前谷歌計(jì)算機(jī)科學(xué)家、現(xiàn)在在灣區(qū)創(chuàng)業(yè)的宇懷·“托尼”·吳（Yuhuai?“Tony”?Wu）概述了一個(gè)更宏偉的機(jī)器學(xué)習(xí)目標(biāo)。在谷歌，吳探索了支持聊天機(jī)器人的大型語(yǔ)言模型如何幫助數(shù)學(xué)。該團(tuán)隊(duì)使用的模型經(jīng)過(guò)互聯(lián)網(wǎng)數(shù)據(jù)訓(xùn)練，然后利用數(shù)學(xué)和科學(xué)論文的在線(xiàn)存檔等大型數(shù)據(jù)集進(jìn)行微調(diào)。吳在研討會(huì)上說(shuō)，當(dāng)以日常語(yǔ)言來(lái)要求解決數(shù)學(xué)問(wèn)題時(shí)，這個(gè)名為Minerva的專(zhuān)門(mén)聊天機(jī)器人“非常擅長(zhǎng)模仿人類(lèi)”。該模型在高中數(shù)學(xué)考試中獲得的成績(jī)優(yōu)于16歲學(xué)生的平均成績(jī)。吳說(shuō)，他設(shè)想最終會(huì)有一位“自動(dòng)化數(shù)學(xué)家”，具有“自行解決數(shù)學(xué)定理的能力”。
計(jì)算機(jī)科學(xué)家宇懷·“托尼”·吳設(shè)想了一位“自動(dòng)化數(shù)學(xué)家”——具有“自行解決數(shù)學(xué)定理能力”的通用研究助理。
數(shù)學(xué)是試金石
對(duì)于這些顛覆式的創(chuàng)新，數(shù)學(xué)家們做出了不同程度的關(guān)注。
哥倫比亞大學(xué)的邁克爾·哈里斯（Michael Harris）表達(dá)了疑慮，他對(duì)研究數(shù)學(xué)與國(guó)防工業(yè)之間潛在的目標(biāo)和價(jià)值觀沖突感到困擾。在最近的一份時(shí)事通訊中，他指出由美國(guó)國(guó)家科學(xué)院組織的一個(gè)研討班——“AI協(xié)助數(shù)學(xué)推理”中，一名演講者是博思艾倫咨詢(xún)公司（Booz Allen Hamilton）的代表，該公司是情報(bào)機(jī)構(gòu)和軍方的承包商。哈里斯希望，能夠有更多關(guān)于人工智能影響數(shù)學(xué)研究的討論。
DeepMind的合作者、悉尼大學(xué)的喬迪·威廉姆森（Geordie Williamson）在美國(guó)國(guó)家科學(xué)院的那場(chǎng)聚會(huì)上發(fā)表了講話(huà)，鼓勵(lì)數(shù)學(xué)家和計(jì)算機(jī)科學(xué)家更多地參與此類(lèi)對(duì)話(huà)。在洛杉磯的研討會(huì)上，他以改編自喬治·奧威爾1945年文章《你和原子彈》的一句話(huà)開(kāi)始了自己的演講。威廉姆森說(shuō)：“考慮到我們所有人在未來(lái)五年內(nèi)都可能受到深刻影響，深度學(xué)習(xí)并沒(méi)有引起像預(yù)期那么多的討論?！彼J(rèn)為，數(shù)學(xué)是機(jī)器學(xué)習(xí)能做什么或不能做什么的試金石。推理是數(shù)學(xué)過(guò)程的精髓，也是機(jī)器學(xué)習(xí)中尚未解決的關(guān)鍵問(wèn)題。
威廉姆森在接受采訪時(shí)表示，在他與DeepMind合作的早期，該團(tuán)隊(duì)發(fā)現(xiàn)了一個(gè)簡(jiǎn)單的神經(jīng)網(wǎng)絡(luò)，可以預(yù)測(cè)他非常關(guān)心的數(shù)學(xué)量，而且它的預(yù)測(cè)“準(zhǔn)確得可笑”。威廉姆森努力想要理解其中的原因，但是無(wú)法理解，DeepMind的其他人也都做不到，而這個(gè)原因?qū)⒊蔀橐粋€(gè)定理的基礎(chǔ)。就像歐幾里得一樣，神經(jīng)網(wǎng)絡(luò)以某種方式直觀地辨別出了數(shù)學(xué)真理，但其邏輯“原因”卻遠(yuǎn)非那么明顯。
在洛杉磯的研討會(huì)上，一個(gè)突出的主題是如何將直覺(jué)和邏輯結(jié)合起來(lái)。但威廉姆森觀察到，人們很少有動(dòng)力去理解機(jī)器學(xué)習(xí)的黑箱。他說(shuō)：“這是科技界的黑客文化，如果它在大部分時(shí)間都有效，那就太好了?！钡@種情況讓數(shù)學(xué)家們感到不滿(mǎn)意。
他補(bǔ)充說(shuō)，試圖理解神經(jīng)網(wǎng)絡(luò)內(nèi)部發(fā)生的事情會(huì)引發(fā)“令人著迷的數(shù)學(xué)問(wèn)題”，而尋找答案為數(shù)學(xué)家“為世界做出有意義的貢獻(xiàn)”提供了機(jī)會(huì)。
（原標(biāo)題：研究者用ChatGPT證明數(shù)學(xué)定理，3年內(nèi)AI會(huì)趕超數(shù)學(xué)家？）
標(biāo)簽：
