頂尖學者研究兩年 AI僅花5天超車
文／編譯張佑生
今年稍早某日，美國卡內基美隆（Carnegie Mellon）大學數學博士生哈里哈蘭（Sidharth Hariharan）收到一封電子郵件後，立刻衝進指導教授辦公室，眼眶泛紅，幾乎說不出話來。
寄信的人不是普通學者，而是2022年菲爾茲獎得主、瑞士洛桑聯邦理工學院數學教授維亞佐夫斯卡（Maryna Viazovska）。消息只有一個：他們被搶先了。
更準確地說，他們被AI搶先，也可說是攔胡了。
過去兩年多來，哈里哈蘭和維亞佐夫斯卡帶領一支6人團隊，投入一項艱鉅工程，希望把維亞佐夫斯卡最著名的一篇數學證明，拆解成電腦可以逐步驗證的形式化版本（formalization）。這是一項耗時漫長、極度講究細節的工作，往往需要研究人員逐行檢查每一個推論步驟。
然而，就在他們即將完成之際，一家AI新創公司的系統只花了5天便完成同樣任務：八維球體堆積定理的形式化驗證工作。
「你會開始懷疑，自己這兩年的人生是不是都白費了。」哈里哈蘭回憶。這句話，道出如今許多年輕研究者心中的焦慮。
被AI完成的，不是普通數學作業。它涉及數學界著名的「球體堆積問題」（Sphere Packing Problem）。
在三維空間裡，這個問題其實很容易理解。想像水果攤上一顆顆柳丁堆疊在一起，怎樣排列才能塞進最多顆水果？數學家數百年前就提出答案，但要嚴格證明這個答案正確卻困難得多，直到1998年才真正完成證明。
如果把空間維度從三維提升到八維，事情就變得更加抽象。沒有人能真正想像八維空間長什麼樣子，但數學家仍能透過符號與公式研究其中的規律。
2016年，維亞佐夫斯卡成功解決八維空間的球體堆積問題，被視為近年最重要的數學突破之一，也讓她在2022年獲得被稱為「數學界諾貝爾獎」的菲爾茲獎（Fields Medal）。
但證明完成，不代表所有工作都結束了。
近年數學界興起一項新運動：把數學證明轉換成電腦可驗證的形式化語言。
這不只是為了確認證明沒有漏洞，更希望建立一個未來可供AI學習、推理與延伸的知識庫。
哈里哈蘭當初主動找上維亞佐夫斯卡，希望一起完成這項形式化工作。對他而言，這不只是研究計畫，更是一堂深入理解大師思想的課。
維亞佐夫斯卡其實知道，若只是想完成形式化，她自己挑選較小的題目或許更有效率。但她沒有這麼做。因為她認為，研究的價值不只在成果。
「或許我自己做個比較簡單的題目最快，但那一點也不好玩。」於是她負責傳授高層次數學概念，哈里哈蘭則教她如何使用Lean數學證明系統，目前最重要的數學形式化軟體之一。
後來又有4名數學家加入，大家共同制定藍圖，把原本艱深的證明一步步拆解。一年後，團隊進一步對外開放合作。不少AI公司也參與其中。原因很簡單：這些形式化證明正是訓練數學AI最珍貴的教材。
當時的AI還相當有限，只能協助完成少量程式碼片段，沒有人認為它能取代整個研究團隊。
因此，當一家名為Math, Inc.的新創公司表示，其AI系統Gauss已經完成部分尚未完成的段落時，數學家們反而感到興奮。他們希望看到更多成果。沒想到，對方之後突然失去聯絡。
幾個月後，消息再度傳來。Math, Inc.利用升級版Gauss重新測試這項計畫。結果令人震驚，AI不只完成部分內容，更完成整個證明的形式化驗證。而且只花了5天。
消息傳回維亞佐夫斯卡耳中時，她一時語塞。後來公司研究員向她展示成果，希望分享這份突破帶來的喜悅。但現場氣氛並不如預期。研究人員後來回憶：「我很快就發現，對方並沒有和我一樣興奮。」
不久後，哈里哈蘭收到那封翻天覆地的電子郵件。接著，他打電話給遠在杜拜的父母。父母給他的回答很簡單：「相信你的老師。」「相信這個過程。」
消息曝光後，Math, Inc.執行長韓恩（Jesse Han）立刻搭乘紅眼班機飛往匹茲堡。隔天早晨，一群人約在星巴克見面。包括哈里哈蘭、他的指導教授阿維加德（Jeremy Avigad），以及韓恩本人。韓恩原本以為，大家會一起慶祝這項突破。他的想法是立即公布成果，然後投入下一個計畫。但學者們的反應完全不同。
他們認為，形式化驗證的目的從來不只是得到一份可運作的程式碼，真正重要的是理解證明背後的思想。哈里哈蘭說：「結果本身確實令人印象深刻，但那不是我們這個計畫真正想達成的目標。」
雙方的認知落差，在這場會議中徹底浮現。對AI公司而言，重點是問題已經解決。對數學家而言，重點是人類是否真正理解了問題。
這場風波之所以引起廣泛討論，不只是因為一篇證明被AI完成。它更像數學界自己的ChatGPT時刻。
多年來，數學一直被視為人類理性能力的最高殿堂之一。即使AI能寫文章、畫圖、寫程式，許多人仍認為純數學研究距離自動化非常遙遠。但近一年情況快速改變。OpenAI日前宣布，旗下模型推翻一項被數學界接受80年的定理。隨後Google DeepMind也公布多項新的數學成果。愈來愈多研究者開始相信，AI已經從解題工具，逐漸走向研究夥伴。
菲爾茲獎得主陶哲軒（Terence Tao）便坦言，一年前還能把這些成果視為有趣實驗，如今已經無法這樣看待。AI正在成為真正有用的數學工具。問題是，接下來呢？
不少數學家最擔心的，並非AI能力本身。而是榮耀與資源如何分配。
許多研究人員指出，Gauss之所以能完成任務，很大程度建立在人類多年累積的成果之上。如果沒有哈里哈蘭團隊先建立完整藍圖，如果沒有數學界多年來投入形式化驗證工作，AI也無從學習。然而，外界看到新聞時，頭條往往只剩一句話：「AI解決了問題」。
真正奠定基礎的人類研究者，卻很少獲得同等關注。部分學者也擔心，財力雄厚的AI公司正在改變學術研究生態。據透露，Math, Inc.為完成這項專案投入超過10萬美元運算資源。這筆錢足以支應數名研究生一年的研究經費。面對資金緊縮的大學數學系，新創公司擁有完全不同的競爭優勢。
不過，即使親身經歷這場衝擊，哈里哈蘭最終沒有離開數學。相反地，他開始使用AI工具協助整理Gauss留下的大量程式碼。他甚至將到另一家數學AI公司實習。只是，他對未來有了一個新的想法。
過去，他研究的是如何把別人的定理形式化。未來，他希望先證明屬於自己的定理。然後再交給AI整理。
「下一個我要形式化的定理。」他說，「我希望是我自己證明出來的。」或許，這也是許多知識工作者未來共同面對的課題。當AI愈來愈擅長完成既有工作，人類真正的價值，可能不再只是把事情做完。而是提出下一個值得被解決的問題。
原文出自《好讀周報》892期
