AlphaProof 怎麼學會證明 · No Priors 筆記

090 · AlphaProof 怎麼學會證明

39:22YouTube 上架 2024-11-14Laurent Sartran, Rishi Mehta & Thomas Hubert（Google DeepMind AlphaProof）

No Priors Ep. 90 | With Google's DeepMind's AlphaProof Team

AlphaProof 團隊說明如何把 AlphaZero 的做法搬到數學證明、test time RL 怎麼慢慢逼近難題，以及形式化數學對數學家和 AI 各代表什麼。

090 講了什麼

從棋類搬到證明AlphaProof 以 AlphaZero 為基礎，也就是神經網路、大規模強化學習加上搜尋。動作空間從棋步換成證明的每一行，用形式語言寫，證明完成時機器會回報對或錯，系統可以從正確的證明學習，再挑戰更難的題。
test time RL遇到解不出來的題目，agent 會在附近造出許多變體題，全部都試；解開任何一個就從中學到東西，一步步逼近原題。解得最久的題目就是靠這個迴圈，花了數天的推論算力。
強項與缺口IMO 的題目分四類，AlphaProof 最強的是代數和數論，組合學較弱，今年的比賽沒有用在幾何。團隊也說它還不會 theory building，組合題難在許多需要的概念在現有函式庫裡根本沒有。
為什麼選數學一位來賓說數學是描述與預測世界的語言，也可能是通往 AI 的一條路，因為它需要推理、概括與抽象。另一位想做「想得越久就越好」的系統，數學是少數還有很長路要走的領域；還有一位把純數學看成對真理的探索。
人類資料與證明的樣子AlphaProof 自己找證明、自己形成風格，外界評論看起來很陌生。其中一位來賓說，少量珍貴的人類資料適合拿來給 agent 起步，之後 RL 再往上推；證明寫得好懂則可以另外優化，用於可解釋性與教學。
對數學社群的意義目前數學家還不能使用 AlphaProof，團隊也說現在完全比不上 Terry Tao 這樣的數學家。他們引 Terry Tao 近來受訪的說法：數學合作的規模小，是因為很難檢查別人做的東西，交給形式系統檢查，就能跟更多人合作。團隊也建議學數學的人及早學 Lean。

從哪一段開始看15 段

00:05開場與背景主持人介紹 AlphaProof 團隊。Rishi 是技術負責人之一，下西洋棋，看了 AlphaZero 的棋局才想做這個，進 DeepMind 時 Thomas 帶的 AlphaZero 團隊正在做數學；另一位來賓做過電腦網路的偵測與廣告投放才轉做 AI 研究；第三位從小下圍棋，做過 AlphaGo、AlphaZero、AlphaCode 與 AlphaTensor。
03:17數學與棋類的差別棋類有對手可以自我對弈；數學沒有對手，只能多想。數學幾乎是純粹的認知活動，不能到現實世界做實驗。
04:34AlphaProof 的架構以 AlphaZero 的三個部分為基礎：神經網路、大規模強化學習、搜尋。動作空間變成證明的每一行，用形式語言寫，驗證完成就能學習。
06:25數學的搜尋空間數學證明不是從工具箱裡挑，常要憑空構造函數或換寫法，搜尋空間很難走。AlphaProof 在代數和數論最強，組合較弱，今年沒有用在幾何。
08:15test time RL解不出來就造許多附近的變體題來試，解開的就學習，一步步逼近原題。解了數天的題目都經過這個迴圈。
09:34限制：theory building目前不會自己建立理論。組合題難在翻成形式語言，現有函式庫缺少需要的概念，之後得能自己發展新定義與新的數學物件。
11:58大問題與黎曼猜想從 Hilbert 的問題談到千禧年大獎難題。來賓說無從估計黎曼猜想還有多遠，也認為要走到那裡，需要創造全新的數學。
14:35為什麼做數學三位各自的理由：數學是描述世界的語言，也可能是通往 AI 的路；想做越想越強的系統；把數學當成對真理的探索。
18:47興趣與應用Elad 問有沒有特別期待的應用。一位來賓想先了解數學家在乎什麼，也提到 Langlands program；另一位期待程式碼驗證，讓程式的性質能用證明確認，再把技術轉到其他領域。
21:53不可驗證的領域主持人問能否用在語言、例如幽默。來賓回答有些領域沒有標準答案，要靠人當依據或靠現實世界，RL 的框架仍然適用，但依賴機器驗證的部分搬不過去。
24:15人類資料與陌生的證明主持人問：如果能無限請 Terry Tao 來標註，有沒有用？來賓說 AlphaProof 自己發現證明，風格被評論為很陌生；有人類標註的話可以往好懂的證明優化。少量人類資料可以讓 agent 起步，RL 再接手。
28:15數學社群與合作數學家目前還不能使用 AlphaProof。形式系統能檢查別人的工作，合作的人數可以更多，團隊希望像研究生一樣幫忙回答數學家的問題。
30:53IMO 第六題來賓拿出 AlphaProof 解第六題的部分證明。這題大約 500 位參賽者只有 5 位解出；AlphaProof 已證明 C 不超過 2，再構造出一個函數讓 C 等於 2。評審之一、Fields 獎得主 Tim Gowers 試了幾個小時也沒找到這種函數。
34:45給數學人的建議形式數學會越來越重要，建議及早學 Lean。形式語言可以依自己的程度放大細節，也能自己驗證有沒有把證明做對。
36:35品味與提問一位來賓認為建立理論比證明定理更需要人類的創意與品味，主持人也說品味越來越重要。也有來賓轉述一個說法：機器越會找答案，人越要會找問題；自己寫程式的工作也越來越從低階細節轉向高階決定。

值得記的話5 句

we should actually try to think exponentially我們其實應該試著用指數的方式去想13:01
the software industry would be in a much better place if verification was much more common如果驗證更普遍，軟體業會好得多21:07
small amounts of precious human data can be really useful少量珍貴的人類資料可以很有用27:13
this is maybe the hardest problem that Alpha proof ever solved我認為這大概是 AlphaProof 解過最難的題目34:30
get better at finding the questions這句是轉述別處看到的說法：機器越會找答案，我們就越得會找問題38:26

名詞與人物9 個

AlphaProof: DeepMind 的 AI 系統，可以找出並驗證數學證明，在今年的 IMO 解出六題中的四題。
AlphaZero: AlphaProof 的基礎，由神經網路、大規模強化學習與搜尋三部分組成。
IMO: 針對年輕人的最古老、最具聲望的數學競賽，六題，分代數、數論、組合與幾何。
test time RL: 解不出來時造出許多變體題並從解開的學習，逐步逼近原題。
formal language: 用程式碼寫數學的形式語言，證明完成時機器會回報對錯。
Lean: 形式化證明的語言，團隊建議學數學的人及早學。
theory building: 自己發展新定義、新數學物件與理論，目前 AlphaProof 做不到。
Riemann hypothesis: 主持人說明它預測質數按特定模式分布；團隊拿它說明大問題離現在有多遠根本無從估計。
Langlands program: 想把數學不同領域連起來的研究計畫，像是數學的統一理論。

提到但沒有展開

談到 Bombelli 研究虛數時被當時重要的數學家嘲笑，多年後才有交流電與描述電的能力，所以機器自己發展出定理之後該朝哪裡去，是個很大的問題。
Elad 舉例：數論後來用在密碼學與零知識證明，群論與代數後來出現在量子力學，說明純理論最終會有應用。

在 YouTube 看原片 ↗

Google DeepMind