戴維·卡斯特維奇Davide Castelvecchi)在《自然》期刊發表的<人工智能將如何改變數學?聊天機器人的興起凸顯了討論>(How will AI change mathematics? Rise of chatbots highlights discussion)指出,「機器學習工具已經幫助數學家製定新理論和解決棘手問題。但他們將進一步撼動這個領域。」(Machine learning tools already help mathematicians to formulate new theories and solve tough problems. But they’re set to shake up the field even more.)
文 /巴枯寧 綜合報導
隨著對聊天機器人的興趣像野火一樣蔓延,數學家開始探索人工智能 (AI) 如何幫助他們完成工作。研究人員表示,無論是協助驗證人工編寫的作品還是提出解決難題的新方法,自動化都開始以超越單純計算的方式改變該領域。
DeepMind AI 發明了更快的算法來解決棘手的數學難題
「我們正在研究一個非常具體的問題:機器會改變數學嗎?」 加拿大蒙特利爾大學的數論學家 Andrew Granville 說。加州大學洛杉磯分校 (UCLA) 的一個研討會探討了這個問題,旨在在數學家和計算機科學家之間架起橋樑。該活動的組織者之一、賓夕法尼亞州匹茲堡卡內基梅隆大學的計算機科學家 Marijn Heule 說:「大多數數學家完全沒有意識到這些機會。」
Akshay Venkatesh 是新澤西州普林斯頓高等研究院的 2018 年著名菲爾茲獎獲得者,他在 10 月的一次研討會上發起了一場關於計算機將如何改變數學的對話,以紀念他。該獎章的另外兩位獲得者,巴黎法蘭西學院的 Timothy Gowers 和加州大學洛杉磯分校的 Terence Tao,也在辯論中發揮了主導作用。
數學家凱文·巴扎德 (Kevin Buzzard) 表示在倫敦帝國理工學院:「事實上,我們現在有像菲爾茲獎得主和其他非常著名的大數學家對這個領域感興趣,這表明它以一種前所未有的方式變得‘熱門’。」
部分討論涉及哪種自動化工具最有用。人工智能有兩種主要類型。在「符號」人工智能中,程序員將邏輯或計算規則嵌入到他們的代碼中。「這就是人們所說的『優秀的老式人工智能』」位於華盛頓州雷德蒙德的微軟研究院的計算機科學家 Leonardo de Moura 說。
另一種方法在過去十年左右取得了極大的成功,它基於人工神經網絡。在這種類型的 AI 中,計算機或多或少地從一張白紙開始,通過消化大量數據來學習模式。這就是所謂的機器學習,它是「大型語言模型」(包括 ChatGPT 等聊天機器人)以及可以在復雜遊戲中擊敗人類玩家或預測蛋白質折疊方式的系統的基礎。符號人工智能本質上是嚴謹的,而神經網絡只能進行統計猜測,而且它們的操作往往很神秘。
De Moura 通過創建一個名為 Lean 的系統幫助符號 AI 取得了一些早期的數學成功。這種交互式軟件工具迫使研究人員寫出問題的每個邏輯步驟,直到最基本的細節,並確保數學是正確的。兩年前,一組數學家成功地將一個重要但難以理解的證明——一個如此復雜以致於它的作者也不確定——轉化為精益,從而證實它是正確的。
研究人員表示,這個過程幫助他們理解了證明,甚至找到了簡化證明的方法。「我認為這比檢查正確性更令人興奮,」De Moura 說。「即使在我們最瘋狂的夢想中,我們也沒有想到這一點。」
除了讓單獨的工作變得更容易之外,這種「證明助手」還可以通過消除De Moura 所說的「信任瓶頸」來改變數學家的合作方式。「當我們合作時,我可能不相信你在做什麼。但是證明助理會向您的合作者表明他們可以信任您的工作部分。」
另一個極端是聊天機器人式的、基於神經網絡的大型語言模型。在加利福尼亞州山景城的谷歌,前物理學家 Ethan Dyer 和他的團隊開發了一個名為 Minerva 的聊天機器人,它專門解決數學問題。從本質上講,Minerva 是消息應用程序自動完成功能的一個非常複雜的版本:通過對 arXiv 存儲庫中的數學論文進行訓練,它學會了以某些應用程序可以預測的相同方式寫下問題的逐步解決方案單詞和短語。與使用類似於計算機代碼的東西進行交流的 Lean 不同,Minerva 以對話式英語接受問題並寫下答案。「自動解決其中一些問題是一項成就,」De Moura 說。
人工智能數學奇才為人類創造了棘手的新問題來解決。Minerva 展示了這種方法的力量和可能的局限性。例如,它可以準確地將整數分解為質數——不能將整數平均分成更小的數。但是一旦數字超過一定大小,它就會開始出錯,這表明它還沒有「理解」一般程序。
不過,Minerva 的神經網絡似乎能夠獲得一些通用技術,而不僅僅是統計模式,谷歌團隊正試圖了解它是如何做到這一點的。「最終,我們想要一個您可以集思廣益的模型,」Dyer 說。他說,對於需要從專業文獻中提取信息的非數學家來說,它也可能有用。進一步的擴展將通過學習教科書和連接專用數學軟件來擴展 Minerva 的技能。
Dyer 說,Minerva 項目背後的動機是想看看機器學習方法能走多遠;幫助數學家的強大自動化工具最終可能會將符號 AI 技術與神經網絡相結合。
從長遠來看,程序會繼續作為配角,還是能夠獨立進行數學研究?AI 可能會更好地生成正確的數學陳述和證明,但一些研究人員擔心其中的大部分將變得無趣或無法理解。在 10 月的研討會上,Gowers 表示,可能有一些方法可以教計算機一些客觀的數學相關性標準,例如一個小陳述是否可以體現許多特殊情況,甚至可以在不同的數學子領域之間架起一座橋樑。「為了擅長證明定理,計算機將不得不判斷什麼是有趣的和值得證明的,」他說。如果他們能做到這一點,那麼人類在該領域的未來看起來就不確定了。
德國亞琛工業大學的計算機科學家 Erika Abraham 對數學家的未來更加樂觀。「人工智能係統的智能程度取決於我們對其進行編程的程度,」她說,智能不在計算機中;智慧在於程序員或培訓師。
新墨西哥州聖達菲研究所的計算機科學家和認知科學家 Melanie Mitchell 表示,在 AI 的一個主要缺點——無法從具體信息中提取抽象概念——得到解決之前,數學家的工作將是安全的。「雖然人工智能係統可能能夠證明定理,但首先要提出有趣的數學摘要來產生定理要困難得多。
本文僅代表作者立場,不代表本平台立場
Facebook Comments 文章留言