AI真的可以做數學了嗎？來自帝國學院教授Kevin Buzzard在最新部落格文章中深刻探討了這個問題。甚至，他預測道，2025年AI能夠拿下IMO金牌級水準。 OpenAI o3發布後，多個高難度基準測試的SOTA被大幅刷新。就數學、程式碼、軟體工程等領域而言，更是完全粉碎了滿血版o1。

在這之中最引人注目的，便是在今年11月Epoch AI發布的數學基準Frontier Math上，準確率破紀錄地達到了25.2%。

那麼，這個結果到底意味著什麼呢？

聯手60多位數學家出題的陶哲軒，曾認為這項測驗能難住AI好多年

最近，帝國學院教授、數學家、IMO金牌得主Kevin Buzzard發表了一篇深度長文——AI現在能做數學了嗎？

文中，他探討了AI在數學研究中的潛力，特別是在處理複雜計算和驗證方面。不過，Buzzard認為在原創性證明、深刻理解數學概念方面，仍存在一些限制。

o3未來在數學方面的研究潛力究竟如何，或許我們能夠從這篇文章中獲得關鍵的一瞥。

o3是什麼？ FrontierMath又是什麼？

或許大多數人都認為，語言模型就是ChatGPT之類的東西：你可以向它問問題，它會寫一些句子給你答案。

語言模型在ChatGPT之前就有了，但總的來說，它們甚至無法寫出連貫的句子或段落。

之後還有很多其他模型。現在，它們仍在快速進步。

沒有人知道這種情況還會持續多久，但有很多人在這個遊戲中投入了大量資金，因此，如果打賭進展會很快放緩，那就太愚蠢了。

Epoch AI在11月宣布， 其精心挑選了「數百」個數學難題， 組成了保密的FrontierMath資料集。

論文連結：https://arxiv.org/abs/2411.04872

之所以要進行“保密”，是有原因的。

大語言模型的訓練要依賴大型的知識資料庫，因此一旦你將資料集公開，這些語言模型就會在上面進行訓練。

如果你向這樣的模型提出來自資料集中的問題，它們可能會直接複述出已經看到的答案。

這個資料集有多難？

那麼，FrontierMath資料集中的問題是什麼樣的呢？

我們知道的是，這些問題不是「證明這個定理」問題，而是「找出這個數字」問題。更準確地說，“問題必須具有清晰且可計算的答案，並且能夠被自動驗證。”

對於資料集中公開的5個範例問題，透過隨機猜測的方式幾乎上不可能成功。而且對於專業數學家來說也不簡單。

Buzzard稱，自己可以理解這5個問題的題意，並且能較為輕鬆地完成第三題──他以前見過這個技巧。

簡單來說就是，函數將自然數n映射到α^n，當且僅當α-1的p進值為正值時，函數在n上是p進連續的。

而且，他也完全知道如何解決第五個問題——這是一個涉及曲線Weil猜想的標準技巧，但沒有去算出確切的13位數答案。

對於第一個和第二個問題，Buzzard承認自己並不會做；至於第四個問題，如果花很多力氣去研究的話可能會有進展，不過他最終沒有嘗試，只是看了看答案。

Buzzard懷疑道，即便是非常聰明的數學本科生，可能連其中的一個問題都無法完成。

例如第一個問題，就需要是解析數論領域的博士生才有可能。

FrontierMath論文中引用了一些數學家對這些問題難度的評價。就連菲爾茲獎得主陶哲軒表示：「這些問題極具挑戰性，只有領域專家才能解決」。

確實，Buzzard稱自己能解決的兩個範例問題都在專業領域，例如算術；而對那些不在專業範圍內的問題，一個都沒解決。

不過，同是菲爾茲獎得主的Borcherds也在論文中提到，機器所產生數值答案「並不完全等同於提出了原創性的證明」。

那麼，為什麼要製作這樣一個資料集呢？

問題在於，對「數百」個「證明這個定理」問題的答案進行評分成本非常高。至少在2024年，人們還不會信任機器在這種複雜程度下進行評分，因此必須花錢聘請人類專家來完成。

相較之下，檢查一個清單中的數百個數字是否與另一個清單中的相對應，電腦可以在一秒鐘內完成。

正如Borcherds所指出的，數學研究人員的大部分時間都是在嘗試提出證明或構思想法，而不是處理數字。

不過，由於在數學領域，AI迫切需要高難度的資料集，而創建這樣一個資料集是非常困難的，或者說是非常昂貴的。因此，FrontierMath資料集仍然非常有價值。

在最近的一篇論文中，Frieder等人深入討論了數學領域AI資料集的不足之處。

論文連結：https://arxiv.org/pdf/2412.15184

此外，Science上也有一篇關於FrontierMath數據集的文章，其中引用了Buzzard的話：“如果有一個系統能夠在這個數據集上取得滿分，那麼數學家的時代就結束了。”

沒想到，就在論文發出的一個多月之後，OpenAI突然宣布o3在這個資料集上取得了破紀錄的25.2%準確率。

整個AI數學圈，都為之震驚，包括Buzzard本人也是。

發生了什麼事？

在數學領域，Buzzard對「AI」能力的認知是「本科生或預科生」的程度。

o3在解決為優秀高中生設計的「奧林匹克式」問題方面，表現得非常出色。

毫無懸念的是，AI系統在一年之內就能通過本科數學考試。

因為，在設計本科數學考試時，通常需要確保不至於有50%的學生都不及格，因此會加入一些標準化問題（和學生們已經見過的非常相似），從而幫助那些對課程有基本理解的學生能通過考試。在這些問題上，機器很容易取得高分。

但要從這一水平跨越到高級本科或早期博士階段，並提出創新性想法，而不僅僅是重複利用標準化的思路，將需要一個相當大的飛躍。

畢竟在普特南競賽（美加知名大學生數學競賽）中， o1 pro只對「B4」這題給出了還不錯的解答，其他大多數答案最多只能得一兩分（滿分10分） 。

上下滑動查看

因此，Buzzard原本預計這個資料集在接下來的幾年內仍然是難以攻破的。

但還是激動早了。

Epoch AI的Elliot Glazer在Reddit發文聲稱資料集中實際上有25%的問題是「IMO/本科生風格的問題」。

這個說法有點令人困惑，因為很難將這樣的形容詞，對應到公開發布的5個問題中的任何一個。

即使是最簡單的一個，也涉及了Weil曲線猜想（或是透過暴力計算論證——勉強可行但會非常痛苦，因為它需要在有限域上分解10^12個三多次項式）。

那麼問題來了，這個資料集中問題的實際程度到底是什麼？或者換句話說，這五個公開問題是否真的有代表性？我們無從得知。

考慮到這一新的信息，即25%的問題是本科水平，Buzzard稱自己對o3取得的成績也就不那麼驚訝了。

不過，他表示，還是很期待AI能夠在資料集上達到50%的準確率。因為在「博士資格考試」上的表現（也就是Elliot Glazer所描述的接下來50%的問題），正是Buzzard希望從這些系統中看到的。

證明這個定理！

然而，正如Borcherds指出的那樣，即使我們最終得到了一台在「找到這個數字」方面超越人類的機器， 它在許多數學研究領域的適用性也將十分有限，因為這些領域的核心問題通常是如何「證明這個定理」。

在Buzzard看來，2024年最成功的案例是DeepMind的AlphaProof——它解決了2024年國際數學奧林匹克（IMO）六道題中的四道。

在這些問題中，既有“證明這個定理”， 也有“找到一個數字並證明它的正確性”。對於其中的三題，機器的輸出是完全形式化的Lean證明。

互動式定理證明器Lean擁有一個完善的數學庫mathlib，其中就包含有能夠解決IMO以及其他問題所需的眾多技術。

最終，DeepMind系統的解答經過人工檢查後被驗證為「滿分」答案。

不過，這相當於讓我們又回到了高中——儘管題目極難，但解題只需使用高中程度的技術。

Buzzard認為，我們將會在2025年看到IMO金牌等級的機器。

但同時，這也迫使我們必須重新面對先前提到的「評分難題」。

誰給機器打分數？

可以設想，在2025年7月的國際數學奧林匹克大賽（IMO）上，除了數百名世界上最聰明的中學生之外，還會有機器參賽。但希望數量不要太多。

這些系統將分為兩種類型：

以電腦證明檢視器（如Lean、Rocq、Isabelle等）的語言提交答案的系統

以人類的語言提交答案的大語言模型

這兩種提交方式之間最大的差別在於：

對於已正確翻譯為電腦證明檢查器語言的題目陳述，評審只需檢查證明能否通過編譯，基本上就可以確定這是不是一個「滿分」答案了。

對於大語言模型，評審將面臨類似普特南競賽解答的情況——計算機會寫出一些看起來很有說服力的內容，但人類需要仔細閱讀並評分，而且並不能保證這會是一個「滿分」答案。

Borcherds提醒AI社群「證明這個定理！」是數學家真正希望看到的，這是非常正確的。

目前在邏輯推理方面，大語言模型的準確度至少比人類專家低一個數量級。

我擔心，在一兩年之內會不可避免地出現語言模型「證明」黎曼猜想的浪潮。這些模糊或不準確的「證明」可能會夾雜10頁正確的數學內容中，而人類必須耗費大量的精力才能把它們找出來。

另一方面，定理證明器的準確性至少高一個數量級：每當看到Lean拒絕接受數學文獻中的某個人類論證時，錯誤的總是人類。

事實上，數學家希望看到的不僅僅是“證明這個定理！”，而是希望看到“正確地證明這個定理，並以人類能夠理解的方式解釋其成立原因”。

對於語言模型方法，我非常擔心「正確性」；而對於定理證明器的方法，我則擔心「是否能夠以人類能夠理解的方式呈現」。

目前進展非常迅速，但我們在這一領域仍然有大量工作要做。

至於何時才能「跨越本科生水平這道坎」？沒有人知道。

來源：新智元