DeepMind agent 破解數學難題：AI 嘅推理能力去到邊？

Paul Erdős，上世紀最傳奇嘅數學家之一，成日周遊列國，瞓人哋梳化，夾錢都唔會多過一杯咖啡。佢有個著名習慣：對住自己解決唔到嘅難題，佢會直接開個「賞金」，幾十到幾千美金不等，邊個解得開就拎得走。呢啲問題後來被稱為 Erdős Problems，橫跨數論、組合數學、圖論等領域，幾十年嚟考起無數數學家。

2025 年，DeepMind 嘅 AlphaEvolve agent 對住超過 50 個呢類開放數學問題——其中包括 kissing number problem（三百年歷史嘅幾何問題）——喺 20% 嘅 cases 入面搵到比已知最佳解更好嘅答案。唔係背答案，唔係 pattern matching，係真係「發現」新知識。

呢件事，比佢哋之前 IMO 銀牌嘅成就更值得我哋留意。

Erdős 的賞金、IMO 的銀牌：agent 做咗啲乜？

先清楚 timeline。2024 年 7 月，DeepMind 嘅 AlphaProof 系統喺國際數學奧林匹克（IMO）攞到 28/42 分，相當於銀牌水平——係史上第一個 AI 系統做到 medal-level performance。佢哋解咗四題（代數兩題、數論一題、幾何一題），包括全場最難嗰題 P6，全球得五個參賽者解到。

技術上，AlphaProof 嘅核心係一個用 reinforcement learning 訓練嘅 agent，喺 Lean（形式化證明語言）嘅環境入面「打機咁打」數學證明。佢先用 3000 億 tokens 嘅 code 同數學文本做 pretraining，再用 Mathlib 入面嘅 30 萬條 human-written proof 做 supervised fine-tuning，最後進入主菜——AlphaZero-style 嘅 RL loop，自己對住 8000 萬條自動生成嘅 formal problems，一日打幾千個 TPU，自我對弈式咁進步。

2025 年 5 月，DeepMind 再出 AlphaEvolve。呢次唔係 Olympiad 問題，而係真嘅 open problems：佢哋用 Gemini 做 base model，加 evolutionary algorithm 框架，自動生成同改進 algorithm 代碼。結果係 Google 數據中心排程效率提升 0.7%（持續一年，已經 production），TPU 晶片設計改進，FlashAttention kernel 加速 32.5%，仲有上面提過嘅數學問題突破。

呢個進程唔係「AI 做數學功課」咁簡單——係 agent 由 benchmark 走到 real-world open-ended discovery。

形式推理 vs 自然語言：agent reasoning 嘅真正突破

好多人以為 AI 推理能力嘅進步單純係「model 大咗就得」。AlphaProof 嘅論文（2025 年 11 月刊於 Nature）話畀我哋知：唔係。

關鍵在於 formal environment。DeepMind 嘅 approach 同 OpenAI o1 或 DeepSeek-R1 嘅 chain-of-thought reasoning 有個本質分別：AlphaProof 嘅所有推理步驟，喺 Lean 入面每一步都係形式化嘅，可以被 kernel 驗證為完全正確。自然語言模型你可以叫佢 show reasoning，但佢永遠可以 hallucinate 一啲睇落合理但實際上錯嘅中間步驟。形式證明系統唔會——啱就係啱，錯就係錯。

呢個分別直接影響咗 agent design 嘅方向：

AlphaZero-style tree search + RL。AlphaProof 唔係「問一句答一句」嘅 chat model。佢係一個 agent，喺 Lean environment 入面行 tree search，每一條 tactic 都係一個 action，search 完之後 reinforcement signal 係「證明成唔成功」。呢個 loop 同 AlphaGo 學捉棋幾乎一樣——只係 game board 換咗做 mathematical proof state。

Test-time RL（TTRL）。呢個係成篇 paper 我覺得最實用嘅 insight。對住最難嘅問題，單靠加大 tree search budget 係唔夠嘅。AlphaProof 嘅做法係：對住目標問題，自動生成大量變體（simplifications, generalizations），然後針對呢個問題-specific 嘅 curriculum 再做一輪 RL training。變相係 inference time 嘅時候「開個 workshop」，圍住問題打幾萬場練習賽，先正式落場。

呢種「inference-time adaptation」嘅思路，對開發者嚟講係一個好 powerful 嘅 pattern——唔洗每次重新 train 個 model，而係在 inference 層面畀 agent 多啲「熱身時間」。

對香港開發者嚟講：agent 時代嘅三個信號

我哋唔係 DeepMind 嘅研究員，冇幾百萬 TPU 小時嘅 budget。但 AlphaProof 同 AlphaEvolve 嘅故事，對每一個做 product 嘅香港 tech 人都有啟示。

第一，Formal verification 開始 practical。 以前形式化驗證係 academic 玩具，得 PL 研究者玩。AlphaProof 證明咗 formal environment 可以作為 RL agent 嘅訓練場。對我哋嚟講，呢個趨勢意味住邊個學識用 Lean、Rust 呢類「嚴格語言」去 wrap critical logic，邊個就可以 build 到 AI 可以信賴嘅系統。

第二，Agent 嘅架構核心係「搜尋 + 驗證」，唔係「生成」。 太多人以為 agent = LLM + function calling。AlphaProof 嘅走勢係用 LLM 做 policy network，真正嘅 intelligence 嚟自 tree search 同 verification loop。你而家寫 production code 嘅時候，係咪可以開始諗「我個 agent 點樣可以自己 verify 自己嘅 output」？

第三，Evolutionary search 係 scaling law 嘅另一條腿。 AlphaEvolve 唔係就咁 train 一個更大嘅 model，而係用多個 model（Gemini Flash + Pro）做生成，再用 evolutionary algorithm 去迭代。呢種「generation + evaluation + selection」嘅 loop，喺 code generation、prompt engineering、甚至 startup idea validation 都可以用。

推理嘅天花板仲有幾高？

講完興奮嘅嘢，都要講 reality check。

AlphaProof 解 IMO 問題，每題要用 2-3 日嘅 TTRL training。人類選手得 4.5 個鐘。AlphaProof 嘅 training 用咗 80,000 TPU days——即係差唔多 4000 部 TPU 行足 20 日。呢個 compute budget，地球上冇幾多個機構負擔得到。

更重要嘅係，AlphaProof 目前嘅成功局限於「已知範圍內嘅難題」。IMO 問題雖然難，但主題係已知嘅（代數、數論、幾何、組合），解法有跡可尋。去到真正嘅前沿數學 research——唔係解難，係建構新理論、定義新概念——仲有好大距離。DeepMind 自己都承認，乜嘢係「數學品味」、邊個問題值得研究，呢啲仍然係 open question。

AlphaEvolve 嘅結果都有同樣嘅限制。雖然佢哋話喺 50 個 open problems 入面 20% 有進步，但大部分 improvement 係 incremental 嘅（lower bound 由 590 推到 593 呢種），而且每個 problem 都要人手 setup。呢個仲未係你掟個問題入去就搞掂嘅水平。

但趨勢係清晰嘅。 一年前 AI 連 IMO 銅牌都攞唔到；今日已經銀牌。AlphaEvolve 已經喺 Google production 行咗一年。Next step 係走向真正嘅 research-level discovery。呢個 timeline 可能比大部分人想像中快。

Erdős 當年最鍾意講嘅一句話係：“Another roof, another proof。” 數學家嘅工作係永遠在路上嘅。而家 AI agent 加入咗呢場旅程。佢唔會取代數學家——正如 AlphaGo 冇取代圍棋棋手。但佢會改寫「推理」呢兩個字嘅定義。

對我哋嚟講，問題唔係「AI 會唔會取代我」，而係「我有冇準備好用呢啲新工具去解決以前解決唔到嘅問題」。

開始 tune 你個 agent 嘅 verification loop 啦。