陶哲軒牛津對談羅博深：解密DeepMind如何讓AI拿到IMO銀牌

新智元報道

編輯：編輯部

【新智元導讀】陶哲軒一場新鮮出爐的演講，爲我們帶來了一場乾貨滿滿的思想盛宴。

7月17日，「牛津數學公開講座」系列研討會邀請到了陶哲軒進行演講，主題是關於AI在科學和數學領域的潛力。

演講結束後，陶哲軒還和CMU數學教授、IMO美國隊前教練羅博深進行了對談。

人工智能是「猜測機器」

「通俗來講，人工智能基本上就是一臺猜測機器。」

陶哲軒的這次演講建立在一個基調之上，那就是「AI會改變科學和數學，這是一項令人驚歎的技術」，但「AI並不是魔法」。

LLM是一個讓我們輸入（比如一個文本查詢請求或其他請求），繼而產生輸出（文本、圖像或數字）的軟件。

這種做法在數學上其實很平常。

實際上，LLM的本質就是在解一個巨大的方程組！通過反覆幾百次的權重調整，LLM最終找到了每個單詞後面的下一個單詞是什麼。

對於人類來說，這個過程相當複雜，但在數學上，這是一個非常無聊的過程。有趣的是如何找到這些權重的方法。

說到這裡，陶哲軒又打了一個比方，AI就像是「飛機的發明」。

噴氣式發動機剛剛出現時，汽車、火車和船隻已經是相當成熟的交通工具了，因此這種新引擎看起來僅僅是個玩具，幾乎無法完成任何實際工作。

但隨着時間的推移，它會變得越來越強大，終有一天讓人類的旅行速度達到當時最快陸地交通工具的10倍。

但你不能僅僅因爲看到了引擎，就直接期待未來的成果，這中間還有許多工作。

爲了造出有實際用途的飛機，我們需要設計新的安全協議、新的儀表設備，找到新的方法，以便更好地理解物理定律——飛機仍然遵循物理定律。

是的，AI就是這樣。它不是魔法，而是與規模有關。AI就像我們日常生活中已經使用的許多軟件一樣。

但是有一個關鍵的區別，那就是我們現在傾向於使用的軟件往往相當無聊，缺乏創意。你輸入什麼，每次都會得到相同的輸出。

在瀏覽器中輸入一個網址，就會直接跳轉到相應的網頁。而且軟件常常很挑剔，如果你稍微犯了個小錯誤，輸入了錯誤的網址，那麼你可能會被帶到其他的地方。但是這一切都非常可預測。

Karpathy也曾表達類似觀點，過去的搜索引擎沒有幻覺，但也沒有創造力：LLM is 100% dreaming

但人工智能不同，特別是去年流行起來的那些大語言模型，它們更有創意。

用相同的查詢問LLM兩次，你可能會得到不同的答案，而且無法保證答案是正確的。

看起來更加離譜且難以理解的是，大模型有時能成功解決非常複雜的數學證明題，比如——

但大多數情況下，它們很難答對「9.9和9.11哪個大」這種問題，簡單的算術題也經常算不準。

這正是陶哲軒將其比喻爲「猜測機器」原因——它猜測出一個接近於它曾看到的其他問題的正確答案，而不是經過它的獨立思考。

這是一種與我們習慣的技術不同的新技術。

我們習慣的技術是那種「在我們眼皮子底下犯錯」的，它們會製造出一些不怎麼樣的輸出，讓我們易於察覺。

但由於AI的本質，這些權重被特意選擇，以便讓答案儘可能接近正確答案。所以即使它們錯了，看起來也會非常具有說服力。

那麼問題來了，我們該如何使用這項新技術呢？

陶哲軒承認，在醫療、財務決策等領域，AI的安全性真的還沒有達到標準。儘管有許多潛在的好處，我們依舊需要抱持謹慎的態度。

這就像我們花了幾十年時間，才讓飛行器達到一個對普通公衆來說真的很安全的狀態。

英雄所見略同，LeCun在談到AI的安全性問題時，也喜歡將其與飛行器做比

但AI正在一些領域取得應用，比如陶哲軒此次演講時的背景幻燈片就是自動生成的，有一種濃濃的「AI味兒」。

看起來的確很像MidJourney或DALL-E的默認風格

但陶哲軒笑談道，「其實也還好，它只需要看起來足夠令人信服即可。背景圖片並不是我演講的核心內容」。

詳解AI潛力

「消防水管」加速科學發展

「科學就像能產生一定量飲用水的水龍頭，而突然之間，我們有了AI這個大消防水管」。

陶哲軒又做出了一個精彩的類比。

他認爲，雖然AI的缺陷在醫療、財務決策這類領域顯得相當危險，但在某些領域是可以接受的，特別是科學領域，因爲科學就是關於驗證，尤其是獨立驗證的過程。

如果有一種設置，可以將AI不可預測但功能強大的輸出與獨立驗證相結合，以過濾掉垃圾，只保留有用的東西。那麼我們將會看到大量潛在應用的涌現。

AI這個「大消防水管」，可以輸出10倍甚至100倍的液體，但輸出的並不是可飲用的水。

但如果我們擁有一個過濾裝置以後呢？它可以幫助我們過濾掉那些雜質，我們就可以得到乾淨的水（科學）了。

這就是陶哲軒看待科學的方式——以數學的方式來看待它。

在許多科學領域，尋找解決問題的「候選答案」成爲了瓶頸。

比如在藥物設計領域，我們想爲某種疾病找到一種藥物。爲此，我們必須要合成它。

首先可能需要從自然界中找到一種藥物，或者對藥物進行改良。然後，必須要合成、試驗，第一階段試驗，第二階段試驗……

這是一個長達數年的試驗過程，而且非常昂貴。因此，只有最大的製藥公司才能負擔得起全程研發直至最終獲得批准。

許多測試的藥物實際上並不奏效，它們在研發過程中的某個階段不得不被放棄。有時候你會幸運一點，雖然它們沒有治癒你想要治療的問題，但它們對其他某些問題有益。

但即便如此，這還是一個非常不確定，有很多試錯的過程。

如果有一種方法可以減少試驗候選對象，那麼一定是利用人工智能。

現在科學家真的在用AI來模擬蛋白質。並且很快，如果有足夠的數據，就可以開始根據現有臨牀試驗的數據模擬藥物功能，爲各種疾病找到有潛力的候選藥物。

在這個過程中，我們仍然需要遵循科學驗證的標準。但不必篩選100個候選者，或許只需10個，你就能找到那一個有效的方法。

陶哲軒還談到了材料科學領域。

室溫超導體是否存在，這個問題已經困擾了我們數十年。人們嘗試了不同的材料，雖然偶爾有所突破，但通常都以失敗告終。

但是，AI有潛力跳過昂貴的合成過程，如果科學家能將候選者數量大幅減少，以大比例縮小範圍，那將是革命性的改變。

實際上，這些科學問題中的設計部分不僅正在被人工智能自動化，甚至合成過程本身也是如此。

人們還在開發由AI驅動的實驗室，以更加自動化的方式進行危險性的化學品的合成。

因此，減少昂貴測試候選對象，這是AI加速科學發展的一個應用領域。

另一個領域是模型加速。

在現代社會，我們必須對各種事物進行建模。

大氣、交通、經濟……幾乎每一件事，每一個複雜的系統，我們希望爲宇宙建模。

但是，建模常常需要我們做的是，必須要運行物理定律。

如果我們想預測地球未來20年的氣候狀況，我們會收集大量數據，並運用已知的物理定律，爲了提高準確性，我們需要將時間劃分得非常細小，還需要把地球劃分成非常細小的網格。

這需要使用超級計算機，而且需要數月的時間來完成。

如果想預測氣候，比如假設二氧化碳濃度保持在這個水平，20年後會發生什麼，則需要花費數月時間才能得到一個相對準確的答案。

但是，原則上，人工智能可以大大縮短這個過程。如果有大量通過超級計算機獲得的模擬數據，就可以用於AI訓練，找出基於未見過的輸入數據預測結果的最佳擬合方案。

氣候模擬領域的人們已經能夠在幾小時內恢復傳統超級計算機模擬的準確性，而不是幾個月。

陶哲軒強調說，這種加速真的是非常、非常地顯著。

從20年到3周：革命即將到來

作爲一名數學家，我對人工智能可能如何改變數學感到非常興奮。

提升AI數學推理能力可能會是一個非常廣闊的領域，提升許多應用場景中的可用性。

目前我們已經看到了一些用例，但還是遠遠不夠。雖然革命尚未發生，但我認爲它即將到來。

將AI應用於學和數據學科有一些缺點，就像上面的乘法題一樣，它可能給出錯誤的結果。

但這也不是世界末日，我們有很多方法進行獨立驗證，例如Lean這類的輔助證明軟件，從而不必完全信任AI。

輔助證明軟件類似於一種計算機編程語言，但輸出並不是可執行程序，而是用於驗證某個陳述是否正確。與AI不同，這類軟件可以100%按照程序設定運行。

目前，數學家們編寫一箇中等規模問題的證明大概需要幾個月的時間，將其形式化所需的時間還要更久，至少是前者的10倍，還需要團隊合作才能完成。

但得益於輔助證明軟件，這個進程正在加快。

下圖列出了數學領域的一些知名成果。上個世紀，定理從成功證明到形式化往往需要幾十年時間，比如四色定理和開普勒猜想。

到了2020年提出的液體張量實驗，僅用了18個月就完成了形式化。

去年11月，我和一些合作者證明了一個關於交換代數的猜想。當時我們立即決定，這是一個很好的測試案例，可以用來觀察計算機的形式化技術是如何工作的。

最終，我們組建了一個大約20人的大團隊，用三週的時間完成了形式化。

雖然依舊沒有那麼方便，但這個過程的難度在降低，每個定理都會在不久的將來被形式化。

目前，速度的提升大部分還是來自傳統方法，比如更好的語言和軟件庫。

GitHub這樣的平臺能讓更多的數學家在一起協同工作，不僅僅止步於5個人或者一兩個小組，而是組織起更大的、20～50人蔘與的項目，這在以前是很難做到的。

而且，就像Copilot的代碼自動補全一樣，AI可以自動填補證明中的小步驟。

隨着時間的推移，我認爲AI不僅能自動完成單行證明，還能完成雙行證明，最終在編寫證明語句方面超越人類的速度。

甚至，未來數學家編寫證明時，可能是向AI口述。只需像對學生那樣，向AI解釋證明的過程，讓AI嘗試對我們解釋的每一個步驟進行形式化驗證，再進行迭代改進。

這會比傳統方式的數學研究更快，而且可以確保不會出錯。所以我認爲人工智能與數學將會產生巨大的協同效應。

與羅博深的爐邊對談

關於DeepMind的IMO銀牌

對談中，羅博深問到了前段時間IMO競賽的重大消息——DeepMind研發的AlphaProof和AlphaGeometry 2模型取得了相當於銀牌的成績。

在對談中，他承認這個結果是自己沒有預料到的。原本預計的時間線是未來3～4年，但沒想到今年就能見證了AI解決IMO級別的數學問題。

這是非常好的工作，也很令人興奮，又有點trick的成分在裡面，但似乎進步往往來自cheap tricks。

IMO中的幾何問題一般是確定可解的，但問題是，如果讓AI直接寫下全部的，比如20個語句，並執行標準算法，會有指數級的運行時間增長。

但是，如果你能做出一個有創意的構建，比如加上一個中點，然後根據這個新座標重新排列現有信息，就可以大幅降低問題的複雜度。

DeepMind所做的事情就是讓AI找到了這個捷徑，再應用更標準的自動化工具，所以實際上只有很小一部分涉及到了AI，而且很有策略性。

但這種通用流程是可以擴展的。在複雜的數學問題，最困難的就是要找出關鍵的中間步驟。

比如，要證A⭢B，如果你能找到合適的中間點C，將問題轉變爲證明A⭢C且C⭢B成立，讓兩個子問題都是原問題難度的一半，這就是一個重大的進步。

也許AI在未來會很擅長這項工作，但我們沒有這方面的數據。DeepMind之所以成功，背後的秘密是他們生成了大量幾何問題進行測試。

參考資料：

https://www.youtube.com/watch?v=_sTDSO74D8Q

https://www.maths.ox.ac.uk/node/68242