陶哲軒最新演講：AI將如何改變數學這一“最保守學科”

來源：學術頭條

整理：王躍然 王江玨

【編者按】日前，菲爾茨獎得主、華裔數學家、加州大學洛杉磯分校教授陶哲軒在牛津數學公開講座中，探討了人工智能（AI）將如何改變數學這個“最保守的學科”。

他指出，數學有著驚人的連續性——200 年前的教科書今天仍可使用，黑板與粉筆依然是標配，論文合著者數量長期徘徊在每篇 2.5 人，遠低于其他科學的“大合作”模式。但這種延續數個世紀的研究范式，正在被新技術打破。

核心觀點如下：

• 形式化驗證使正確運用機器學習和 AI 來解決問題成為可能。

• 當前 AI 本質是“猜測機器”，必須與驗證器結合，AI 負責批量生成候選答案，驗證器負責剔除錯誤。

• AI應處理“中等難度長尾問題”，而非替代數學家攻堅。 最有效的應用方向不是讓AI挑戰人類最擅長的創造性難題，而是讓它完成第一遍篩選，再把真正困難的留給人類專家。

• 數學研究正在從“個案研究”轉向“大規模調查”。AI 的使命不是縮小數學的蛋糕，而是把它做大。

學術頭條在不改變原文大意的情況下，做了簡單的編譯。演講內容如下：

我將談談我所在的數學領域在 AI 時代是如何發生變革，以及這種變革可能對其他學科產生的影響。但當前我們身處一個充滿變革和不確定性的時代，這是我們不太習慣的。就數學領域而言，我們或許是所有學科中最保守的，因為幾個世紀以來，我們的研究方法幾乎未曾改變。

左側展示的是一本 200 年前由柯西教授撰寫的教科書，其中介紹了我們現在稱之為柯西積分公式的內容。雖然在當前的分辨率下難以辨認，但是它的內容幾乎和如今研究生使用的教材一模一樣。除了它是法語而不是英語，且沒有采用現代計算機排版語言排版之外，它如今完全可以使用。數學的這種連續性正是其強大的一大優勢。我們使用 200 年前、甚至 2000 年前的成果。比如我在工作中經常用到勾股定理。這確實很棒，但這確實意味著我們往往不像其他學科那樣熱衷于追逐潮流。

右邊這本咖啡桌畫冊是由攝影師杰西卡·溫創作的。她對數學家使用的黑板非常著迷。我們幾乎是唯一一個仍然保留黑板和粉筆的學科了。其他人都開始用 PPT、白板等現代工具了。但是，我的辦公室里還是有六塊黑板。我超愛它們，絕對舍不得丟棄。話說回來，她給數學家們的黑板拍了照片，制作了一本精美的小型藝術畫冊。

我們與其他科學領域的區別還在于，數學研究往往缺乏合作。這里有一些科學指標可以參考：多年來，我們論文的合著者平均數從每篇 1.5 人逐漸上升到數學領域的 2.5 人。但看看其他學科，它們正在蓬勃發展——那些大型合作研究項目層出不窮，數學家們卻遠遠落后。

現在，這并不是因為我們不善交際，或者不僅僅是因為不善交際。這里確實存在一些系統性問題。

傳統數學項目歷來都有很高的準入門檻。通常需要數學博士才能理解研究課題。我們要求證明必須在每個細節上都做到百分之百正確。所以，如果你嘗試通過眾包獲取證明，當 100 個貢獻中有一份出錯時，整個證明就會被推翻。而我們現有的工作流程，比如用粉筆在黑板上一起討論解決問題，無法擴展到與 100 人通過互聯網進行協作。

其他科學領域正在蓬勃發展，我們難道就落后了嗎？

其實情況正在開始改變，這要歸功于新技術的推動，包括 AI （雖然我認為 AI 只是其中一部分）。我們正逐步掌握如何開展大規模研究項目。要知道，直到最近，數學研究還停留在“案例分析”階段——先攻克一個難題，花幾個月時間完成報告，然后轉向下一個課題。但現在我們開始采用“調查研究”模式，能夠同時處理數百甚至數千個問題。

我們或許無法解決所有問題，但我們可以收集有關這些難題群體的各種有趣數據。我們正開始突破數學博士群體的局限，擴大參與范圍。“公民科學”正在其他學科領域蓬勃發展，而數學領域的“公民數學”才剛剛起步。

雖然目前還處于萌芽階段，但我們正逐步摸索如何正確運用機器學習和 AI 來解決問題。雖然我們發現許多錯誤的 AI 應用方式，但這些工具的實用價值正逐漸顯現。其中有個關鍵要素讓這一切成為可能——形式化驗證。

形式化驗證是一種特殊的計算機語言，簡單來說，它能自動處理數學論證并驗證其正確性。這種技術能大幅減少干擾因素，有效過濾掉那些曾阻礙新型工作流程發展的“糟粕”。

舉個例子，我今天只能在演講中分享一個半案例。

第一個案例是去年我在加州大學洛杉磯分校啟動的“方程理論項目”，這個項目是我與 50 位合作者共同完成的。其中大部分伙伴都是通過這個項目結識的，之前我都沒見過面。而且他們中的大多數并不是專業數學家。很多計算機科學家、學生、研究生、本科生，甚至一些高中生都參與了這個開放的協作項目。

這個代數研究項目的具體內容我暫時不便透露，但是我們通過程序生成了 2200 萬個代數問題。比如典型問題就是：交換律是否蘊含結合律？如果有一個運算，使得 a*b 等于 b*a，你能推斷出 a*b*c 等于 a*b*c 嗎？結果表明答案是否定的。

但是我們生成了 2200 萬個這類問題。任何一個具體的問題，也許一個代數專業的研究生可以花一個小時就能判斷對錯。但問題數量高達 2200 萬個，我可沒有 2200 萬研究生。有人會說：“讓我們眾包吧”，“開放平臺讓公眾參與”。但要處理 2200 萬道代數題，這根本沒人能搞定。我也沒時間處理。

所以這類項目在過去根本無法實現。比如之前文獻里提到的同類項目，最多也就研究過 20 道題。但這次涉及 2200 萬道題，完全不是一個量級。

不過我們居然在三個月內完成了這個項目。對于每個命題，我們都有對應的證明或反證，來證明它是真是假。

為此我們不得不發明一些新的工作流程：

• 我們在 GitHub 上搭建了大型儲存庫，所有證明都必須用標準化語言“形式化”，這樣才能實現自動化驗證。我們使用了 Lean 這個證明輔助語言。

• 我們搭建了活躍的討論區，這里既有人工生成的證明：有人會從 2200 萬條推論中隨機選取一條進行驗證并發布，其他人則會嘗試復刻這些成果。

• 研究人員會運行計算機程序，嘗試解決全部 2200 萬個問題，他們的程序每次最多能處理 10 萬個問題。

• 團隊成員會反復調整，將人類證明轉換為計算機證明，或將計算機證明轉換為人類證明。這種反復調整的過程我們算是即興摸索出來的，但效果確實非常顯著。

我認為這個項目成功有幾個關鍵因素：

1.高度模塊化設計

系統本身就被拆解成 2200 萬個相關問題，研究人員可以針對其中的某個子集展開專項攻關。或者說，有些人會專門撰寫人類可讀的證明文件，而另一些人則會專門將這些證明轉化成計算機可讀的證明。你不必事無巨細地了解項目每個環節，完全可以專注于某個特定領域。這就像現代軟件開發項目中的分工協作模式。

2.明確的評估標準

另一個關鍵優勢在于我們制定了明確的評估標準。當項目設定目標并建立評分體系（比如損失函數）后，就能開始優化改進，這種機制為項目推進開辟了全新思路。

在項目進行到第 16 天時，系統顯示存在 2200 萬條關聯數據。但實際上，我們早在第 16 天就解決了除 888 條之外的所有問題。隨后團隊會從這些數據中篩選出部分子集進行專項研究。這種機制讓項目實現了自主分散化運作——參與者自發開展研究，若發現有效方案，就會為數據庫新增解決方案，使剩余問題數量持續減少。整個團隊就這樣不斷推動項目進展。

有些想法讓這個數字大幅下降，有些則不太成功，不過我們不需要像傳統項目那樣協調配合——你知道的，大家各司其職。雖然我們進行了任務分配，但參與者們也自發地展開了許多獨立活動，這過程其實挺有意思的。

3.形式化驗證打破信任壁壘

最后我提到的秘訣是形式化驗證，關鍵在于它能打破信任壁壘。

以前在數學領域，如果你想和其他人合作，要么你必須檢查他們提交的每一行內容，要么你必須相信他們擁有足夠好的聲譽，相信他們的工作質量足夠高，值得被納入你的論文中。但是我們收到了來自各種各樣的人的投稿，這些人我們從未見過。但是所有貢獻都必須經過這種形式化驗證，所以我們可以接受匿名或不受信任的貢獻。

而且，這種驗證方式確實能帶來極其精確的討論。比如有人嘗試驗證某個證明（比如人工驗證），然后將其轉換為Lean 代碼。假設這個證明包含九個步驟，其中八個步驟都能正常運行，但最后一個步驟存在形式化問題。這時可以與原作者進行深入討論，針對這個需要特別說明的微步驟進行澄清。這種討論雖然不需要 BLE 工具，但通常需要耗費大量時間來規范符號體系和通用術語。

有時候人們可能不太明白，如果不能具體說明某個步驟，為什么你會卡在這個環節。但這些編程語言支持極其精確的技術討論，甚至能細化到原子級層面。而且你不需要完全理解整個項目就能推進工作。

雖然我們確實使用了一些相對復雜的 AI 技術，特別是那些被稱為自動定理證明器的工具，但事實上，像 GitHub 這樣的基礎協作平臺，以及 Zulip 平臺上的討論組這類基礎協作工具，反而非常實用且不可或缺。

我有時間再講半個案例。這個項目是與 Google DeepMind 合作進行的，雖然已經進入開發階段，但論文還在審批流程中，所以具體成果暫時不便透露。不過可以大致說明谷歌在該領域的前期工作：

目前大型語言模型正變得越來越強大，能夠解決奧林匹克競賽級別的難題，有時甚至能解答相當復雜的數學問題。但它們仍會出錯，而且這些錯誤往往非常基礎。就連最新款的模型，當你問它簡單算術題時，有時答對有時答錯。比如有個題目它把 7*4+8*8 算錯了，結果被指出錯誤后道歉，最后居然也答對了。

所有數學家都試過用這種系統，最終發現它的不可靠性實在是個大問題。不過要是能把這種不穩定輸出和驗證器結合起來——也就是能實際檢測輸出是否正確的工具——那至少在理論上還是能派上用場的。有時候你可以讓它進入循環運行：讓語言模型生成數學計算結果，然后進行測試。如果運行正常就很好；如果出問題，就將錯誤信息反饋給模型，讓它嘗試修正。

確實有很多人嘗試過各種方法來實現這個功能，效果參差不齊。我一直在與 DeepMind 合作開發他們最新推出的 Alpha Evolve 工具。除此之外還有其他方案，比如底層的通用算法。不過這個方案目前看來效果還算不錯。

它已經能夠解決某些類型的數學問題了。幾個月前我們發表了一篇初步論文，其中我們成功地改進了諸如打包問題的各種界限。例如，如果你有 11 個六邊形，能同時容納這 11 個六邊形的最小六邊形是什么？之前也有關于最佳包裝的記錄。通過讓大語言模型嘗試各種隨機的東西，獲得反饋，不斷改進代碼，他們最終獲得了數值上的提升。

這些本身只是一些測試用例，是有限維優化問題，只是我們所關心的所有數學問題中很小的一部分。不過，我們最近在研究無限維優化問題方面也取得了一些進展。很遺憾，我現在還不能透露更多信息。敬請期待，幾周后我們會發表一篇論文。

總而言之，這些工具正在逐步改變我們的職業領域。它們已經在多個方面發揮著重要作用：

• 輔助次要任務：事實上，我和許多同事日常工作中都會用到 AI 來輔助完成次要任務。比如編寫計算機代碼現在變得輕松多了，進行文獻綜述也變得更加高效。

• 發現新模式：雖然我們還無法系統化地應用，但已有零星案例表明，將數據集輸入 AI 后，確實能獲得新的數學猜想和發現規律。

• 充當“萬能翻譯器”：AI 還能幫助科學家跨越專業壁壘——雖然我們的術語體系與同行存在差異，但借助 AI 技術，溝通效率已顯著提升。

目前已有諸多 AI 應用展現出良好效果，但要開發更先進的應用場景，我們仍需通過嚴格的驗證機制來規范其使用。說白了，我們只能在信任 AI 輸出結果的前提下使用它，或者至少能進一步驗證這些結果。但風險實在太高了。

雖然 AI 能為數學家提供一定幫助，但我覺得它們最有效的應用場景還是需要融入更廣泛的科研協作體系。只有通過團隊協作，才能填補 AI 在數學研究中存在的空白。

最直觀的用法就是讓 AI 來替代數學家最擅長的領域——用創新方法攻克那些棘手難題。但實際上，AI 還有一個正交的、更有前景的應用方向：處理那些中等難度的問題。比如這 2200 萬道代數題，我們沒有足夠的人力來解決，但可以讓 AI 先進行初步探索，找出所有容易解決的問題，然后再把任何難題交給人類專家。

在專家小組討論中，大家也提到了這種范式。總體來說，我認為 AI 不應該是為了和人類競爭現有工作量，而是要擴大這個領域，創造更多經濟上可行的新任務。

雖然存在許多前景廣闊的應用場景，但其應用具有高度情境依賴性。這并非即插即用的解決方案，我們必須掌握其使用方法及適用時機。

謝謝大家。

閱讀最新前沿科技趨勢報告，請訪問歐米伽研究所的“未來知識庫”

https://wx.zsxq.com/group/454854145828

未來知識庫是“ 歐米伽 未來研究所”建立的在線知識庫平臺，收藏的資料范圍包括人工智能、腦科學、互聯網、超級智能，數智大腦、能源、軍事、經濟、人類風險等等領域的前沿進展與未來趨勢。目前擁有超過8000篇重要資料。每周更新不少于100篇世界范圍最新研究資料。 歡迎掃描二維碼或訪問https://wx.zsxq.com/group/454854145828進入。