o3拿下25%高分震驚數學教授，2025 IMO金牌或被AI收入囊中

AI真的可以做數學了嗎？來自帝國理工學院教授Kevin Buzzard在最新博文中深刻探討了這個問題。甚至，他預測道，2025年AI能夠拿下IMO金牌級水平。

OpenAI o3發佈後，多個高難度基準測試的SOTA被大幅刷新。

就數學、代碼、軟件工程等領域而言，更是完全粉碎了滿血版o1。

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

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

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

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

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

01 o3是什麼？FrontierMath又是什麼？

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

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

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

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

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

之所以要進行「保密」，是有原因的。

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

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

02 這個數據集有多難？

那麼，FrontierMath數據集中的問題是什麼樣的呢？

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

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

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

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

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

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

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

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

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

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

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

那麼，為什麼要製作這樣一個數據集呢？

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

相比之下，檢查一個列表中的數百個數字是否與另一個列表中的相對應，計算機可以在一秒鍾內完成。

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

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

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

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

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

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

03 發生了什麼？

在數學領域，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希望從這些系統中看到的。

04 證明這個定理！

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

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

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

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

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

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

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

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

05 誰給機器打分？

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

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

以計算機證明檢查器（如Lean、Rocq、Isabelle等）的語言提交答案的系統

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

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

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

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

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

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

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

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

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

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

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

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

參考資料： 

https://xenaproject.wordpress.com/2024/12/22/can-ai-do-maths-yet-thoughts-from-a-mathematician/ 

本文來自微信公眾號「新智元」，作者：新智元，36氪經授權發佈。