·越來越多的數學研究者關注人工智能對該領域的影響，在各種討論會上辯論，采用不同的AI工具嘗試解答數學問題。

·數學是機器學習能做什么或不能做什么的試金石。推理是數學過程的精髓，也是機器學習中尚未解決的關鍵問題。神經網絡以某種方式直觀地辨別出了數學真理，但其邏輯“原因”卻遠非那么明顯。

(相關資料圖)

加州理工學院和麻省理工學院研究者發(fā)布用大語言模型證明數學定理的論文。

最近一段時間，人工智能似乎在數學領域取得了進展，盡管一開始大語言模型被看作并不是特別適合數學推理。

上周，英偉達數學家Jim Fan轉發(fā)了加州理工學院和麻省理工學院研究者用ChatGPT證明數學定理的論文，稱數學的AI Copilot（副駕駛）時代已經到來，未來人工智能將能夠發(fā)現數學定理。這篇論文構建了一個基于大語言模型的定理證明器，為解決大語言模型幻覺方面的缺陷開辟了一條新途徑。

幾天前，數學家、菲爾茲獎得主陶哲軒表示，他最近在解決一個數學難題時“使用了GPT-4”，“它給我提供了最終的解題思路，接下來我只需要繼續(xù)計算就行?！睘榱私o更多研究者參考，他曬出了自己和GPT-4的聊天記錄。

如今，越來越多的數學研究者關注人工智能對該領域的影響，他們在各種討論會上辯論，采用不同的AI工具嘗試解答數學問題。根據《紐約時報》最近對一些數學家的采訪，他們正在努力應對人工智能這一最新變革力量。數千年來，數學家們已經適應了邏輯和推理方面的最新進展，他們?yōu)槿斯ぶ悄茏龊脺蕚淞藛幔?/p>

數學家和計算機科學家一起開會

兩千多年來，數學家歐幾里得的文本一直是數學論證和推理的典范。卡內基梅隆大學邏輯學家杰里米·阿維加德（Jeremy Avigad）在接受采訪時說：“眾所周知，歐幾里得以近乎詩意的‘定義（definitions）’開始?！?“然后，他在此基礎上建立了當時的數學，使用基本概念、定義和先驗定理，以每一個后續(xù)步驟‘清楚地遵循’之前的步驟來證明事物?！卑⒕S加德說，有人抱怨歐幾里得的一些“明顯”步驟并不明顯，但該系統(tǒng)仍然有效。

但到了20世紀，數學家不再愿意將數學建立在這種直觀的幾何基礎上。相反，他們開發(fā)了正式的系統(tǒng)——精確的符號表示、機械規(guī)則。最終，這種形式化使得數學能夠轉化為計算機代碼。1976年，四色定理（該定理指出四種顏色足以填充地圖，因此沒有兩個相鄰區(qū)域具有相同的顏色）成為第一個借助計算強力證明的主要定理。

現在，人工智能來了。2019年，曾供職于谷歌、現供職于灣區(qū)一家初創(chuàng)企業(yè)的計算機科學家克里斯蒂安·塞格迪（Christian Szegedy）預測，計算機系統(tǒng)將在10年內趕上或超過人類最優(yōu)秀數學家解決問題的能力。去年他將目標年份修改為2026年。

普林斯頓高等研究院數學家、2018年菲爾茲獎獲得者阿克謝·文卡特什（Akshay Venkatesh）目前對使用人工智能不感興趣，但他熱衷于談論。?“我希望我的學生意識到他們所處的領域將會發(fā)生很大的變化?！彼谌ツ甑囊淮尾稍L中說。最近他又補充說：“我并不反對深思熟慮和刻意使用技術來支持我們人類的理解。但我堅信，留心我們使用它的方式至關重要?！?/p>

今年2月，阿維加德參加了在加州大學洛杉磯分校純數學與應用數學研究所舉辦的“機器輔助證明”研討會。這次聚會吸引了數學家和計算機科學家這一不尋常的組合。該研討會的主要組織者是陶哲軒，他曾在一篇博客中稱，2026年AI將與搜索和符號數學工具相結合，成為數學研究中值得信賴的合著者。陶指出，直到最近幾年，數學家們才開始擔心人工智能的潛在威脅，無論是對數學美學還是對他們自己，圈子成員現在正在提出這些問題并探索“打破禁忌”。

幫助解決數學問題的小工具們

如今，在飲食、睡眠、鍛煉方面，優(yōu)化人們生活的小工具十分普遍，威斯康星大學麥迪遜分校數學家喬丹·埃倫伯格（Jordan Ellenberg）在研討會休息期間接受采訪說：“我們喜歡給自己增加一些東西，以便更容易把事情做好?！比斯ぶ悄苄」ぞ呖赡軐祵W有同樣的作用。

其中一種數學小工具被稱為證明助手或交互式定理證明器。數學家一步步將證明轉化為代碼，然后軟件程序檢查推理是否正確。驗證在一個庫中積累，成為其他人可以查閱的動態(tài)參考。阿維加德說，這種“形式化”為當今的數學奠定了基礎，“就像歐幾里得試圖編纂和整理數學、為他那個時代的數學奠定了基礎一樣?！?/p>

最近，開源證明輔助系統(tǒng)Lean備受關注。Lean由計算機科學家萊昂納多·德·莫拉（Leonardo de Moura）開發(fā)，當時他在微軟，現在是亞馬遜的計算機科學家。Lean使用自動推理，由所謂的“老式人工智能（GOFAI）”提供支持，即受邏輯啟發(fā)的符號人工智能。到目前為止，Lean社區(qū)已經驗證了一個翻轉球體的定理和一個有助于統(tǒng)一數學領域的關鍵定理等。

但證明助手也有缺點：它經常抱怨不理解數學家輸入的定義、公理或推理步驟，因此它被戲稱為“證明抱怨者”。所有這些抱怨都會讓研究變得很麻煩，但福特漢姆大學（Fordham University）的數學家希瑟·麥克白（Heather Macbeth）表示，提供逐行反饋的功能也使該系統(tǒng)對教學很有用。

今年春天，麥克白設計了一門“雙語”課程：她把黑板上提出的每一個問題都翻譯成講義中的Lean代碼，學生們用Lean和普通語言提交作業(yè)答案。?“這給了它們信心。”麥克白說，因為它們收到了關于證明何時完成以及整個過程中的每一步是對還是錯的即時反饋。

自從參加洛杉磯研討會以來，約翰·霍普金斯大學的數學家艾米麗·里爾（Emily Riehl）使用實驗性證明輔助程序來形式化她之前與合著者發(fā)表的證明。在驗證結束時，她說：“我真的非常深入地理解了這個證明，比我以前理解的要深入得多?！?/p>

約翰·霍普金斯大學的數學家艾米麗·里爾一直在使用一個實驗性證明助理程序。

卡內基梅隆大學計算機科學家、亞馬遜學者馬利恩·海勒（Marijn Heule）使用另一種自動推理工具，被他稱為“暴力推理”，或者更專業(yè)地說是可滿足性問題求解器。他說，只要用精心設計的代碼來說明你想要找到哪個“奇異物體”，超級計算機網絡就會在搜索空間中進行“翻攪”，并確定該實體是否存在。

還有一組工具使用機器學習，可以合成大量數據并檢測模式，但不擅長邏輯、逐步推理。谷歌的DeepMind就設計了機器學習算法來解決蛋白質折疊和國際象棋獲勝等問題，在2021年《自然》雜志的一篇論文中，一個團隊將他們的成果描述為“通過人工智能指導人類直覺來推進數學發(fā)展”。

前谷歌計算機科學家、現在在灣區(qū)創(chuàng)業(yè)的宇懷·“托尼”·吳（Yuhuai?“Tony”?Wu）概述了一個更宏偉的機器學習目標。在谷歌，吳探索了支持聊天機器人的大型語言模型如何幫助數學。該團隊使用的模型經過互聯網數據訓練，然后利用數學和科學論文的在線存檔等大型數據集進行微調。吳在研討會上說，當以日常語言來要求解決數學問題時，這個名為Minerva的專門聊天機器人“非常擅長模仿人類”。該模型在高中數學考試中獲得的成績優(yōu)于16歲學生的平均成績。吳說，他設想最終會有一位“自動化數學家”，具有“自行解決數學定理的能力”。

計算機科學家宇懷·“托尼”·吳設想了一位“自動化數學家”——具有“自行解決數學定理能力”的通用研究助理。

數學是試金石

對于這些顛覆式的創(chuàng)新，數學家們做出了不同程度的關注。

哥倫比亞大學的邁克爾·哈里斯（Michael Harris）表達了疑慮，他對研究數學與國防工業(yè)之間潛在的目標和價值觀沖突感到困擾。在最近的一份時事通訊中，他指出由美國國家科學院組織的一個研討班——“AI協(xié)助數學推理”中，一名演講者是博思艾倫咨詢公司（Booz Allen Hamilton）的代表，該公司是情報機構和軍方的承包商。哈里斯希望，能夠有更多關于人工智能影響數學研究的討論。

DeepMind的合作者、悉尼大學的喬迪·威廉姆森（Geordie Williamson）在美國國家科學院的那場聚會上發(fā)表了講話，鼓勵數學家和計算機科學家更多地參與此類對話。在洛杉磯的研討會上，他以改編自喬治·奧威爾1945年文章《你和原子彈》的一句話開始了自己的演講。威廉姆森說：“考慮到我們所有人在未來五年內都可能受到深刻影響，深度學習并沒有引起像預期那么多的討論。”他認為，數學是機器學習能做什么或不能做什么的試金石。推理是數學過程的精髓，也是機器學習中尚未解決的關鍵問題。

威廉姆森在接受采訪時表示，在他與DeepMind合作的早期，該團隊發(fā)現了一個簡單的神經網絡，可以預測他非常關心的數學量，而且它的預測“準確得可笑”。威廉姆森努力想要理解其中的原因，但是無法理解，DeepMind的其他人也都做不到，而這個原因將成為一個定理的基礎。就像歐幾里得一樣，神經網絡以某種方式直觀地辨別出了數學真理，但其邏輯“原因”卻遠非那么明顯。

在洛杉磯的研討會上，一個突出的主題是如何將直覺和邏輯結合起來。但威廉姆森觀察到，人們很少有動力去理解機器學習的黑箱。他說：“這是科技界的黑客文化，如果它在大部分時間都有效，那就太好了?！钡@種情況讓數學家們感到不滿意。

他補充說，試圖理解神經網絡內部發(fā)生的事情會引發(fā)“令人著迷的數學問題”，而尋找答案為數學家“為世界做出有意義的貢獻”提供了機會。

（原標題：研究者用ChatGPT證明數學定理，3年內AI會趕超數學家？）

標簽：