把數學變成遊戲：DeepMind 的 AlphaProof 如何從棋盤走向奧數金牌

2021 年底的某個晚上，Thomas Hubert 在倫敦的公寓裡點開了一支 YouTube 影片。

影片是兩年前在微軟研究院一間小會議室錄的，講者是倫敦帝國學院的數學家 Kevin Buzzard，講題叫「數學的未來」。Buzzard 剃著光頭，穿著黑色數學 T-shirt 配一條鮮豔的花褲子，在投影幕前來回踱步，用一種幾近狂熱的語氣描述他的夢想：如果全世界的數學家都用一套叫 Lean 的程式語言來寫證明，會發生什麼事。他的想像從瑣碎（Lean 幫教授改考卷）到末日（AI 靠數學推理稱霸世界），每一個都講得信誓旦旦。

在 Buzzard 上台之前，Lean 的創造者 Leo de Moura 做了簡短的開場。他提到他的年輕同事 Daniel Selsam 剛剛發起了一項挑戰，叫做「IMO 大挑戰」（IMO Grand Challenge），目標是打造一個能在國際數學奧林匹亞（IMO）拿到金牌的 AI 系統。de Moura 說了一句讓 Hubert 印象深刻的話：「如果你覺得圍棋很難，那是一個有限的行動空間。這項競賽是無限的行動空間，充滿了展現人性的神奇招數。」

看著這支影片，Hubert 意識到一件事：他可能是全世界最適合接下這個挑戰的人。

圍棋之子

Hubert 的人生軌跡像是專門為這一刻設計的。他在巴黎長大，父親是法國圍棋全國冠軍，為了讀圍棋書自學了日文，後來到日本參加世界錦標賽，在那裡遇見了 Hubert 的日本母親。Hubert 跟著父親學棋，拿下法國高中圍棋全國冠軍。但他的野心不只是當棋手。

在巴黎中央理工學院和史丹佛大學取得數學金融碩士學位後，Hubert 進了金融業。工作一開始很刺激，但很快就無聊了。他覺得自己學得太慢，缺少能互相激盪的同事。同時，他父親很久以前提過的一個想法始終揮之不去：寫一個能下圍棋的電腦程式。

Hubert 花了一年自修，上遍 Coursera 的相關課程，讀了無數論文。有一天他發現了 DeepMind 研究員 David Silver 的個人網站，上面展示了早期用神經網路預測圍棋下一手的研究。這個網站像是一道閃電。它也證實了 Hubert 的直覺：DeepMind 已經把圍棋定位為人工智慧的試金石。2015 年中，他申請了 DeepMind 的工作，第一次面試失敗了。六個月後他再試一次，憑著圍棋選手的背景，被錄取為研究工程師，加入目標是打造超人類圍棋 AI 的團隊。

從 AlphaGo 到 AlphaZero：征服有限遊戲

接下來的故事已經被寫進了 AI 的經典敘事，但《The Proof in the Code》提供了內部視角。

團隊首先打造了 AlphaGo。他們用數千局人類棋譜訓練神經網路，讓系統學會下棋的基本模式和判斷。然後用「強化學習」讓系統自我對弈數百萬局，根據輸贏來更新對好棋的理解。2016 年，AlphaGo 對上世界排名第一的韓國棋手李世乭。第二局的第 37 手成為歷史時刻：AlphaGo 把棋子放在棋盤右側一個看起來像錯誤的位置，李世乭站起來離開房間，花了將近十五分鐘才決定下一手。那一手不是錯誤，它扭轉了整盤棋。AlphaGo 最終以四勝一負贏得系列賽。

但 AlphaGo 的棋風仍然帶有人類的痕跡，因為它的初始訓練來自人類棋譜。DeepMind 想知道：如果完全不給人類知識，只給規則，AI 能下得更好嗎？他們打造了 AlphaGo Zero，一個從零開始的系統。它只知道規則，其他一切都要自己摸索。第一局它亂下一通，但透過強化學習迅速進步。三天的自我對弈訓練之後，DeepMind 讓 AlphaGo Zero 和擊敗李世乭的 AlphaGo 對弈一百局。AlphaGo Zero 全勝。

DeepMind 把這套方法推廣成更通用的 AlphaZero，訓練它下西洋棋和日本將棋。它在這些遊戲中同樣達到超人類水準，包括擊敗了經過多年人工調校的頂級西洋棋引擎 Stockfish。Alpha 系列有效征服了棋盤遊戲的領域。

尋找下一座山

征服棋盤之後，DeepMind 共同創辦人 Demis Hassabis（哈薩比斯）開始推動第二階段的願景。他在 2016 年告訴 Pushmeet Kohli：圍棋只是第一階段，真正的目標是把這些方法用在對人類有實際意義的問題上。Kohli 接受了邀請，在 DeepMind 成立了「AI for Science」部門。

這個部門像一個大學研究系，多個小團隊各自追尋不同方向。其中一個團隊打造了 AlphaFold，能預測蛋白質的三維結構，讓哈薩比斯和同事 John Jumper 拿到了 2024 年的諾貝爾化學獎。另一個團隊 AlphaTensor 尋找更快的矩陣乘法演算法，在某些情況下打破了 1969 年以來的紀錄。還有 AlphaCode，一個能撰寫 Python 和 C++ 程式碼的 AI 模型。

但這些不同的計畫有一個共同的核心邏輯：強化學習的本質是在龐大的可能性空間中找到最佳選項。棋盤遊戲是這個概念的完美試驗場，因為規則清楚、勝負明確。問題是：還有什麼領域也具備這些特徵？

Hubert 參與了 AlphaTensor 和 AlphaCode 之後，知道答案。下一座山是數學。

為什麼數學比圍棋難得多

從萊布尼茲到希爾伯特，雄心勃勃的思想家早就認定數學是形式推理的巔峰。解數學題和下圍棋在結構上確實有相似之處：兩者都有規則，都有明確的勝利標準（圍棋是佔領更多領地，數學是建構一個邏輯完整的證明）。這正是 Selsam 在提出 IMO 大挑戰時的洞察：數學可以被「玩」。

但圍棋和數學之間的複雜度差距是天文數字級的。圍棋的行動空間是有限的：一步棋大約有 250 個合法落子點，一盤棋通常在 150 到 250 手之間結束。所有可能的棋局數量估計在 10 的 360 次方到 10 的 700 次方之間，已經是天文數字，但終究是有限的。

數學則是無限的行動空間。在證明的任何一步，你都面對無窮多個可能的下一步。更棘手的是，有些最關鍵的「棋步」可能是從未被人類發現過的概念或技巧。圍棋 AI 可以透過暴力搜尋找到好棋，但數學 AI 無法暴力搜尋所有可能的推理路徑。de Moura 在那場演講裡的警告是認真的：這是一個「充滿展現人性的神奇招數」的無限空間。

這就是 Lean 扮演的關鍵角色。要做強化學習，你需要一個「遊戲」。幾千年來，人類沒有一個能讓電腦「下數學棋」的環境。但 Lean 改變了這個局面。在 Lean 裡，每一步推導要嘛被接受，要嘛被拒絕。一個證明要嘛完整通過，要嘛存在缺陷。這種清晰的「贏或輸」回饋訊號，正是強化學習需要的。Hubert 看著 Buzzard 的影片，意識到了這一點：Lean 就是數學的棋盤。

AlphaProof 的誕生

書中沒有詳細披露 AlphaProof 的內部技術架構，這不意外，DeepMind 對核心方法向來保密。但 Hartnett 透過 Hubert 和 Kohli 的訪談，勾勒出了基本輪廓。

AlphaProof 的訓練方式延續了 AlphaGo Zero 的核心理念：從規則出發，透過大量自我對弈學習。只不過這次的「棋盤」是 Lean 的形式化數學環境，「下棋」是嘗試建構數學證明，「贏」是 Lean 接受了你的證明。系統會反覆嘗試不同的推導路徑，根據成功或失敗來更新對「好的推理步驟」的理解。

這和大型語言模型的做法截然不同。ChatGPT 之類的 LLM 是透過模仿人類文本的模式來生成回應，它們很有創意，但不可靠。它們會用流暢的語言包裝錯誤的推理，也就是所謂的「幻覺」問題。在日常對話中這也許可以接受，但在數學中，一步錯就全盤皆錯。

AlphaProof 選擇了另一條路。它不模仿人類怎麼寫數學，而是透過反覆嘗試和 Lean 的即時回饋來發展自己的推理策略。這更慢，也更困難，但產出的每一步都經過 Lean 的驗證。書中引述數學家們早期測試 LLM 的經驗做為對比。Kevin Buzzard 曾和同事試用 ChatGPT 做數學，發現它的表現就像他在課堂上看到的普通學生一樣：對簡單問題回答得頭頭是道，但一碰到陌生題目就開始胡說八道，而且說得極有自信。陶哲軒的評語更直接：LLM 像是「過度自信的大學生」，會提供建議但分不清好壞。

2024 年 IMO：金牌等級

2024 年七月，國際數學奧林匹亞在英國巴斯（Bath）舉行。這是全球最頂尖的中學生數學競賽，六道題目每題七分，滿分 42 分。那一年，金牌的門檻是 29 分。

DeepMind 派出了兩套系統聯合應戰：AlphaProof 負責代數和數論題，另一套系統 AlphaGeometry 2 負責幾何題。聯合成績拿到了 28 分，距離金牌門檻 29 分只差一分。但讓觀察者印象深刻的不只是分數：AlphaProof 解出了被認為那屆最難的第 6 題，展現出的推理深度令人意外。Google DeepMind 宣布這是 AI 在數學推理領域的歷史性里程碑。

陶哲軒也在巴斯。他在 IMO 期間發表了一場演講，描繪他對 AI 輔助數學的願景。他認為 AlphaProof 的成功驗證了一個核心思路：形式化驗證系統（Lean）加上強化學習，能讓 AI 在純粹推理任務中達到頂尖水準。但他也清楚指出，IMO 題目和真正的數學前沿研究之間仍有巨大鴻溝。IMO 題目是精心設計過的，保證有解，而且用初等方法就能解決。前沿數學問題可能需要發明全新的概念和框架，這是目前任何 AI 都做不到的。

不只是數學

AlphaProof 的意義遠不止於數學競賽。

書中描述了 AI 實驗室內部一個更大的野心：他們希望在數學推理中鍛鍊出來的 AI 能力，可以移植到其他需要嚴格邏輯推理的領域。蛋白質結構預測（AlphaFold）、程式碼生成（AlphaCode）、矩陣運算最佳化（AlphaTensor），這些都是在不同領域驗證同一套核心能力。數學被視為這條路線的最終試煉場，因為它要求的推理深度和精確度遠超其他領域。

de Moura 自己也看到了這個趨勢。他在書中承認，連他這個習慣性只看到 Lean 缺點的人，都不得不承認 Lean 正在產生的影響。AI 實驗室開始把 Lean 視為一塊關鍵拼圖：它能提供清晰的回饋訊號來訓練 AI，也能驗證不可靠的大型語言模型的輸出。在通往通用人工智慧（AGI）的路上，數學推理和形式化驗證被認為是核心能力之一。

但 Hartnett 的書也誠實地呈現了另一面。Lean 的使用者介面仍然「麻煩得要命」（Carnegie Mellon 大學 Jeremy Avigad 的用語），使用者必須記住各種特殊語法，一個字元打錯就會讓整個證明失敗。Mathlib 裡有數十萬條定理，你得記住它們的名字才能快速引用。陶哲軒在 PFR 形式化的最後，就因為不知道一個內建指令的存在，多寫了一百行不必要的程式碼。

從棋盤到證明

Thomas Hubert 在那個倫敦的夜晚看完 Buzzard 的影片之後，開始了一段將近三年的旅程。從父親教他的圍棋，到 DeepMind 的 AlphaGo，到征服棋盤遊戲的 AlphaZero，再到把數學變成 AI 可以「下棋」的 AlphaProof。這段旅程的弧線清晰得像是事後編排的，但書中呈現的是一連串不確定的選擇和賭注。

Hubert 第一次面試 DeepMind 失敗了。圍棋 AI 在 AlphaGo 之前看起來還是科幻。從棋盤遊戲跳到數學推理，在大型語言模型席捲一切的 2022 年，看起來像是逆潮流而行。但 Hubert 和他的團隊押注的是一個簡單的洞察：如果你能把一個問題變成「遊戲」，有明確的規則和勝負判定，那強化學習就能發揮威力。Lean 讓數學變成了這樣的遊戲。

這本書的副標題是「一部真理機器如何改變數學與 AI」。AlphaProof 的故事告訴我們，這個改變是雙向的。數學家用 Lean 來驗證自己的證明，AI 用 Lean 來學習如何推理。一個巴西工程師十年前為了抓軟體 bug 而寫的程式語言，正在成為連接人類數學智慧和機器推理能力的橋樑。這大概是 Leo de Moura 當初完全沒有預料到的。