AI工具將如何改變數學領域

ChatGPT的橫空出世讓人們對聊天機器人的興趣如野火般蔓延，數學家們開始探索人工智慧（AI）如何幫助他們完成工作。英國《自然》雜誌網站在2月17日的報道中指出，機器學習等AI工具已經幫助數學家創建新的理論並解決棘手的問題，它們正以超越單純計算的方式改變數學領域。

“熱度”空前

加拿大蒙特利爾大學的數字理論家安德魯·格蘭維爾表示：“我們正在研究一個非常具體的問題：機器會改變數學嗎？”

不久前，在加州大學洛杉磯分校舉行的一個研討會探討了這個問題，該研討會旨在為數學家和電腦科學家之間架起橋梁。

2018年菲爾茲獎獲得者、普林斯頓高等研究所的阿克謝·文卡特什早在去年10月的一次研討會上，曾經進行過一場關於電腦將如何改變數學的對話。另外兩位獲獎者、巴黎法蘭西學院的蒂莫西·高爾斯和加州大學洛杉磯分校的陶哲軒也對這一領域表現出興趣。

英國帝國理工學院的數學家凱文·巴扎德表示：“菲爾茲獎獲得者和其他非常著名的大數學家對這一領域感興趣表明，這一領域的‘熱度’與過去不同。”

各展所長

數學家們目前關注的一個方面是：哪種自動工具最有用。

一種是“符號主義”人工智慧：程式員將邏輯或計算規則嵌入代碼中，微軟研究院的電腦科學家萊昂納多·德·莫拉説：“這是人們所説的‘老式AI’。”

另一種是基於人工神經網路的AI，在過去10年取得了極大的成功。在這種類型的AI中，電腦或多或少都是從頭開始，通過消化大量數據來學習，這被稱為機器學習，它是包括ChatGPT等聊天機器人在內的“大型語言模型”的基礎，也是可以在複雜遊戲中擊敗人類玩家或預測蛋白質如何折疊的系統。

德·莫拉所在的微軟研究院在2013年推出了電腦定理證明器Lean，幫助“符號”AI在數學領域取得了一些成就。

從原則上來説，Lean是一個“證明助手”，能幫助數學家完成證明過程：數學家可以把數學公式轉換成代碼，再輸入到Lean中，讓程式來驗證定理是否正確。2020年，德國著名數學家、菲爾茲獎得主皮特·舒爾茨遇到的難題被Lean證明了。幫助舒爾茨只是Lean這麼多年中的一項工作而已，這個數學證明器，如今已經得到許多數學家的支援。

谷歌公司的伊森·戴爾及其團隊則開發了一款名為Minerva的聊天機器人，專門解決數學問題。通過在預印本網站（arXiv）存儲庫中對數學論文進行培訓，Minerva學會了用一些應用程式預測單詞和短語的方式，逐步寫出問題的解決方案。

與Lean使用類似電腦代碼的方式進行交流不同，Minerva可以用英語會話回答問題並撰寫答案。

Minerva目前已經展示了自身的威力和可能的局限性。例如，它可以精確地將整數分解成質數。但一旦數字超過一定大小，它就會出錯。

戴爾表示，他們推出Minerva項目背後的另一隱藏動機是看機器學習方法能到什麼程度，一個幫助數學家的強大自動化工具最終有望將“符號主義”AI技術與神經網路技術結合起來。

有利有弊

AI可能會更好地産生正確的數學陳述和證明，但一些研究人員擔心，其中大多數陳述和證明會令人不感興趣或無法理解。

在去年10月的研討會上，高爾斯表示，可能有一些方法能教電腦一些與數學有關的客觀標準。他説：“為了更好地證明定理，電腦必須判斷什麼是有趣的和值得證明的。如果他們能做到這一點，某些數學家可能會失業。”

德國亞琛大學的電腦科學家埃裏卡·亞伯拉罕則持相反意見，她對數學家的未來更加樂觀。她説：“AI的智慧取決於我們編寫的程式，智慧不在電腦裏，智慧在程式員身上。”

美國聖塔菲研究所的電腦科學家和認知科學家梅勒妮·米切爾表示，AI目前存在一個主要缺點：無法從具體資訊中提取抽象概念，在克服這個“先天不足”之前，數學家的工作將是安全的，“雖然AI系統也許能夠證明定理，但要想從一開始就提出有趣的數學抽象，那就困難得多。”