新智元報道
編輯：編輯部 JHY【新智元導(dǎo)讀】AI真的可以做數(shù)學了嗎？來自帝國理工學院教授Kevin Buzzard在最新博文中深刻探討了這個問題。甚至，他預(yù)測道，2025年AI能夠拿下IMO金牌級水平。OpenAI o3發(fā)布后，多個高難度基準測試的SOTA被大幅刷新。
就數(shù)學、代碼、軟件工程等領(lǐng)域而言，更是完全粉碎了滿血版o1。
在這之中最引人矚目的，便是在今年11月Epoch AI發(fā)布的數(shù)學基準Frontier Math上，準確率破紀錄地達到了25.2%。
那么，這個結(jié)果到底意味著什么呢？
聯(lián)手60多位數(shù)學家出題的陶哲軒，曾認為這項測試能夠難住AI好多年
最近，帝國理工學院教授、數(shù)學家、IMO金牌得主Kevin Buzzard發(fā)表了一篇深度長文AI現(xiàn)在能做數(shù)學了嗎？
文中，他探討了AI在數(shù)學研究中的潛力，特別是在處理復(fù)雜計算和驗證方面。不過，Buzzard認為在原創(chuàng)性證明、深刻理解數(shù)學概念方面，依舊存在一些局限。
o3未來在數(shù)學方面的研究潛力究竟如何，或許我們能夠從這篇文章中獲得關(guān)鍵的一瞥。
o3是什么？FrontierMath又是什么？
可能大多數(shù)人都認為，語言模型就是ChatGPT之類的東西：你可以向它提出問題，它會寫一些句子給你答案。
語言模型在ChatGPT之前就有了，但總的來說，它們甚至無法寫出連貫的句子或段落。
之后還有很多其他模型�，F(xiàn)在，它們?nèi)栽诳焖龠M步。
沒有人知道這種情況還會持續(xù)多久，但有很多人在這個游戲中投入了大量資金，因此，如果打賭進展會很快放緩，那就太傻了。
論文鏈接：https://arxiv.org/abs/2411.04872
之所以要進行「保密」，是有原因的。
大語言模型的訓(xùn)練要依賴于大型的知識數(shù)據(jù)庫，因此一旦你將數(shù)據(jù)集公開，這些語言模型就會在上面進行訓(xùn)練。
如果你向這樣的模型提出來自數(shù)據(jù)集中的問題，它們可能會直接復(fù)述出已經(jīng)看到的答案。
這個數(shù)據(jù)集有多難？
那么，F(xiàn)rontierMath數(shù)據(jù)集中的問題是什么樣的呢？
我們知道的是，這些問題不是「證明這個定理」問題，而是「找到這個數(shù)字」問題。更準確地說，「問題必須具有清晰且可計算的答案，并且能夠被自動驗證�！�
對于數(shù)據(jù)集中公開的5個示例問題，通過隨機猜測的方式幾乎上不可能成功。而且對于專業(yè)數(shù)學家來說也不簡單。
Buzzard稱，自己可以理解這5個問題的題意，并能較為輕松地完成第三道題他以前見過這個技巧。
簡單來說就是，函數(shù)將自然數(shù)n映射到α^n，當且僅當α-1的p進值為正時，該函數(shù)在n上是p進連續(xù)的。
而且，他也完全知道如何解決第五個問題這是一個涉及曲線Weil猜想的標準技巧，但沒有去算出確切的13位數(shù)答案。
對于第一個和第二個問題，Buzzard承認自己并不會做；至于第四個問題，如果花很多力氣去研究的話可能會有進展，不過他最終沒有嘗試，只是看了看答案。
Buzzard懷疑道，即便是非常聰明的數(shù)學本科生，可能連其中的一個問題都無法完成。
比如第一個問題，就需要是解析數(shù)論領(lǐng)域的博士生才有可能。
FrontierMath論文中引用了一些數(shù)學家對這些問題難度的評價。就連菲爾茲獎得主陶哲軒表示：「這些問題極具挑戰(zhàn)性，只有領(lǐng)域?qū)＜也拍芙鉀Q」。
確實，Buzzard稱自己能解決的兩個示例問題都在專業(yè)領(lǐng)域，比如算術(shù)；而對那些不在專業(yè)范圍內(nèi)的問題，一個都沒解決。
不過，同是菲爾茲獎得主的Borcherds也在論文中提到，機器所生成數(shù)值答案「并不完全等同于提出了原創(chuàng)性的證明」。
那么，為什么要制作這樣一個數(shù)據(jù)集呢？
問題在于，對「數(shù)百」個「證明這個定理」問題的答案進行評分成本非常高。至少在2024年，人們還不會信任機器在這種復(fù)雜程度下進行評分，因此必須花錢聘請人類專家來完成。
相比之下，檢查一個列表中的數(shù)百個數(shù)字是否與另一個列表中的相對應(yīng)，計算機可以在一秒鐘內(nèi)完成。
正如Borcherds所指出的，數(shù)學研究人員的大部分時間都是在嘗試提出證明或構(gòu)思想法，而不是處理數(shù)字。
不過，由于在數(shù)學領(lǐng)域，AI迫切需要高難度的數(shù)據(jù)集，而創(chuàng)建這樣一個數(shù)據(jù)集是非常困難的，或者說是非常昂貴的。因此，F(xiàn)rontierMath數(shù)據(jù)集仍然非常有價值。
在最近的一篇論文中，F(xiàn)rieder等人深入討論了數(shù)學領(lǐng)域AI數(shù)據(jù)集的不足之處。
論文鏈接：https://arxiv.org/pdf/2412.15184
此外，Science上也有一篇關(guān)于FrontierMath數(shù)據(jù)集的文章，其中引用了Buzzard的話：「如果有一個系統(tǒng)能夠在這個數(shù)據(jù)集上取得滿分，那數(shù)學家的時代就結(jié)束了�！�
沒想到，就在論文發(fā)出的一個多月之后，OpenAI突然宣布o3在這個數(shù)據(jù)集上取得了破紀錄的25.2%準確率。
整個AI數(shù)學圈，都為之震驚，包括Buzzard本人也是。
發(fā)生了什么？
在數(shù)學領(lǐng)域，Buzzard對「AI」能力的認知是「本科生或預(yù)科生」的水平。
o3在解決為優(yōu)秀高中生設(shè)計的「奧林匹克式」問題方面，表現(xiàn)得非常出色。
毫無懸念的是，AI系統(tǒng)在一年之內(nèi)就能通過本科數(shù)學考試。
因為，在設(shè)計本科數(shù)學考試時，通常需要確保不至于有50%的學生都不及格，因此會加入一些標準化問題（和學生們已經(jīng)見過的非常相似），從而幫助那些對課程有基本理解的學生能通過考試。在這些問題上，機器很容易取得高分。
但要從這一水平跨越到高級本科或早期博士階段，并提出創(chuàng)新性想法，而不僅僅是重復(fù)利用標準化的思路，將需要一個相當大的飛躍。
上下滑動查看
因此，Buzzard原本預(yù)計這個數(shù)據(jù)集在接下來的幾年內(nèi)仍然是難以攻破的。
但還是激動早了。
Epoch AI的Elliot Glazer在Reddit發(fā)帖聲稱數(shù)據(jù)集中實際上有25%的問題是「IMO/本科生風格的問題」。
這個說法有點令人困惑，因為很難將這樣的形容詞，對應(yīng)到公開發(fā)布的5個問題中的任何一個。
即使是最簡單的一個，也涉及到了Weil曲線猜想（或是通過暴力計算論證勉強可行但會非常痛苦，因為它需要在有限域上分解10^12個三多次項式）。
那么問題來了，這個數(shù)據(jù)集中問題的實際水平到底是什么？或者換句話說，這五個公開問題是否真的具有代表性？我們無從得知。
考慮到這一新的信息，即25%的問題是本科水平，Buzzard稱自己對o3取得的成績也就不那么驚訝了。
不過，他表示，還是很期待AI能夠在數(shù)據(jù)集上達到50%的準確率。因為在「博士資格考試」上的表現(xiàn)（也就是Elliot Glazer所描述的接下來50%的問題），正是Buzzard希望從這些系統(tǒng)中看到的。
證明這個定理！
然而，正如Borcherds指出的那樣，即使我們最終得到了一臺在「找到這個數(shù)字」方面超越人類的機器， 它在許多數(shù)學研究領(lǐng)域的適用性也將十分有限，因為這些領(lǐng)域的核心問題通常是如何「證明這個定理」。
在Buzzard看來，2024年最成功的案例是DeepMind的AlphaProof它解決了2024年國際數(shù)學奧林匹克（IMO）六道題中的四道。
在這些問題中，既有「證明這個定理」, 也有「找到一個數(shù)字并證明它的正確性」。對于其中的三道題，機器的輸出是完全形式化的Lean證明。
交互式定理證明器Lean擁有一個完善的數(shù)學庫mathlib，其中就包含有能夠解決IMO以及其他問題所需的眾多技術(shù)。
最終，DeepMind系統(tǒng)的解答經(jīng)過人工檢查后被驗證為「滿分」答案。
不過，這相當于讓我們又回到了高中盡管題目極難，但解題只需使用高中水平的技術(shù)。
Buzzard認為，我們將會在2025年看到IMO金牌水平的機器。
但同時，這也迫使我們不得不重新面對之前提到的「評分難題」。
誰給機器打分？
可以設(shè)想，在2025年7月的國際數(shù)學奧林匹克大賽（IMO）上，除了數(shù)百名世界上最聰明的中學生之外，還會有機器參賽。但希望數(shù)量不會太多。
這些系統(tǒng)將分為兩種類型：
以計算機證明檢查器（如Lean、Rocq、Isabelle等）的語言提交答案的系統(tǒng)
以人類的語言提交答案的大語言模型
這兩種提交方式之間最大的區(qū)別在于：
對于已被正確翻譯為計算機證明檢查器語言的題目陳述，評審只需檢查證明能否通過編譯，基本上就可以確定這是不是一個「滿分」答案了。
對于大語言模型，評審將面臨類似普特南競賽解答的情況計算機會寫出一些看起來很有說服力的內(nèi)容，但人類需要仔細閱讀并評分，而且并不能保證這會是一個「滿分」答案。
Borcherds提醒AI社區(qū)「證明這個定理！」是數(shù)學家真正希望看到的，這是非常正確的。
目前在邏輯推理方面，大語言模型的準確度至少比人類專家低一個數(shù)量級。
我擔心，在一兩年之內(nèi)會不可避免地出現(xiàn)語言模型「證明」黎曼猜想的浪潮。這些模糊或不準確的「證明」可能會夾雜10頁正確的數(shù)學內(nèi)容中，而人類不得不耗費大量的精力才能把它們找出來。
另一方面，定理證明器的準確性至少高一個數(shù)量級：每當看到Lean拒絕接受數(shù)學文獻中的某個人類論證時，錯誤的總是人類。
事實上，數(shù)學家希望看到的不僅僅是「證明這個定理！」，而是希望看到「正確地證明這個定理，并以人類能夠理解的方式解釋其成立原因」。
對于語言模型方法，我非常擔心「正確性」；而對于定理證明器的方法，我則擔心「是否能夠以人類能夠理解的方式呈現(xiàn)」。
目前進展非常迅速，但我們在這一領(lǐng)域仍然有大量工作要做。
至于何時才能「跨越本科生水平這道坎」？沒有人知道。
參考資料：https://xenaproject.wordpress.com/2024/12/22/can-ai-do-maths-yet-thoughts-from-a-mathematician/
