前言
最近我在做 AI for Math 相關的產品，不是那種讓大模型講題的工具，而是更偏向結構化的幾何表達、約束關係、圖形結構、推理能力這些方向。
做著做著會發現一個問題：讓 AI 聊數學不難，讓 AI 真正做數學，很難。
尤其是幾何。
我可以讓模型解釋「為什麼內錯角相等」，但要它在一張複雜圖裡自己找到關鍵輔助線，它就開始胡說八道。
這時候再回頭看 Google 的路線，會發現他們其實很早就開始系統性地做這件事。
AlphaGeometry（AG1）是第一代。
AlphaGeometry2（AG2）是升級版。
如果把兩代系統連起來看，它其實很像一份非常清晰的數學 AI 系統踩坑紀錄。
我寫這篇文章，就是想站在 Google 的肩膀上，看一看：
- 他們卡在哪裡
- 怎麼解決
- 哪些地方是工程問題
- 哪些地方是認知誤區
一、第一代 AlphaGeometry：它到底解決了什麼？
AG1 的核心思路其實很務實：不要指望大模型自己證明幾何題，而是讓大模型負責「猜」，符號系統負責「算」，搜尋負責「找」。
具體來說：
- LLM 提出輔助構造
- DDAR 符號引擎做角度和比例推理
- 搜尋系統遍歷可能路徑
這個架構本身非常理性，它承認語言模型不擅長嚴謹推理，而是擅長模式匹配與生成可能有用的構造。真正的證明則交給符號系統。
這裡的關鍵元件是 DDAR 推理引擎。
DDAR 的全名是 Deductive Database of Angle and Ratio。
簡單理解，它其實是一個專門為幾何設計的推理系統。
系統會維護一個不斷擴展的「幾何關係資料庫」，一開始它只知道一些基礎事實。比如：
A,B,C 共線
D 在 AB 上
然後持續套用幾何定理，例如：
共線 → 角度為 180°
圓 → 共圓角相等
相似三角形 → 比例關係
每推導出一個新的關係，就加入資料庫，然後繼續推理。這個過程會一直持續，直到推導出目標結論。
換句話說，DDAR 做的事情就是把所有能推出的幾何關係全部推導出來。
二、AG1 卡在哪裡？（這些問題我也踩過）
AG1 很強，但問題也很明顯。
我從工程角度看，主要有三個卡點。
1️⃣ 表達能力太弱
AG1 的幾何語言非常克制，它只支援一些基礎關係，例如：
collinear(A,B,C)
parallel(l1,l2)
perpendicular(l1,l2)
concyclic(A,B,C,D)
equal_angle(...)
但很多 IMO 題目其實需要表達距離關係、比例關係、角度數值計算，這些在 AG1 中都表達不了。例如：
AB = CD
AB / CD = EF / GH
∠ABC = 60°
如果語言裡沒有這些表達能力，系統就無法正確理解題目。
我們給 AI 的表達空間，決定了它能做多複雜的事情。 就像人類文明的語言系統一樣，當一個概念在語言裡不存在時，我們很難真正理解它。
AG1 在這裡明顯受限，因為語言太窄了。
2️⃣ 搜尋會爆炸
幾何證明本質上是在巨大的可能構造空間裡，找到一條正確路徑。
例如：連哪條輔助線？作哪條垂線？哪些點可能共圓？
AG1 是「試一個構造 -> 跑推理 -> 不行再換」。
問題是輔助線的可能性太多了，系統很容易卡在局部搜尋。
3️⃣ 資料問題
數學 AI 最大的難題之一：沒有大規模高品質資料。
AG1 的解法是隨機生成幾何圖、自動生成定理、自動生成證明。
但第一代系統生成的題目複雜度還是有限，這會影響模型的構造能力，讓它無法真正解決複雜題目。
三、AlphaGeometry2：升級了什麼
很多人會以為 AG2 的進步是因為 Gemini 底模更強了。
當然這是原因之一，但我認為下面幾個升級更關鍵。
1️⃣ 語言擴展
AG2 擴展了幾何 DSL，新增了很多 predicate。例如：
dist_eq(A,B,C,D) → AB = CD
ratio_eq(A,B,C,D,E,F) → AB/CD = EF
angle_compute(...) → 角度數值關係
DSL 擴展之後，IMO 題目的表達覆蓋率從 66% 提升到 88%。
換句話說，上個版本 不是 AI 不會做題，而是很多題 AI 根本沒辦法讀懂。
2️⃣ 搜尋方式升級
AG1 基本上是單樹搜尋。AG2 引入多棵搜尋樹 + 共享中間結論，可以理解成多個解題小組同時工作。
這顯著提高了找到關鍵輔助線的機率。
3️⃣ 推理引擎優化
DDAR 在 AG2 中被強化：新推理規則、推理圖壓縮、推理速度優化。
推理更快，搜尋空間自然更可控。
這不是 glamorous 的創新，但非常重要。
4️⃣ double points
AG2 裡還有一個很有意思的幾何 trick，叫 double points。
簡單說，就是允許系統在推理中建立兩個「重合點」。例如：
A ≡ A'
也就是說 A 和 A' 實際上是同一個點，但在推理系統裡可以參與不同關係。比如：
A 在直線 l 上
A' 在圓 c 上
因為 A = A'，最終可以推出：
A 在圓 c 上
這個技巧可以把很多複雜的角度問題轉化成共圓問題，而共圓關係更容易被推理系統處理。
如果你做過競賽幾何，會發現這種思路其實很熟悉，AlphaGeometry2 只是把這種技巧系統化了。
四、結果對比
看最終結果，AG2 的提升其實非常明顯。
在 DeepMind 的官方報告中，他們統計了 過去 25 年（2000–2024）所有 IMO 幾何題。
| 系統 | 解題率 |
|---|---|
| AlphaGeometry (AG1) | 54% |
| AlphaGeometry2 (AG2) | 84% |
AG2 在同一套題目上，解題能力提升了 30 個百分點。
DeepMind 研究團隊還給了一個很有意思的對比：
42/50 的成績已經超過平均 IMO 金牌選手的水平。
另一個指標是 問題覆蓋率。
很多幾何題在 AG1 中根本無法表達，因為語言太窄。
AG2 擴展 DSL 後：
| 指標 | AG1 | AG2 |
|---|---|---|
| IMO 題目可表達覆蓋率 | 66% | 88% |
語言一擴展，系統能力就直接上了一個台階。
DeepMind 在官方部落格中也提到，在 IMO 2024 的測試環境裡，AG2 在形式化之後 19 秒就解出一道競賽題，整體成績達到 28/42 分，接近金牌線。
五、寫在最後
AlphaGeometry2 說明了一件事：
在結構化系統裡，AI 可以非常強。
如果你期待純 LLM 能直接證明 IMO 幾何題，我認為短期幾年內不現實。
但 LLM + 領域語言 + 符號引擎 + 搜尋系統 是一個非常穩健的方向。
站在巨人的肩膀上看一眼，可以少走很多彎路。
如果未來幾年 AI 數學系統會繼續進化，我猜關鍵詞是：
- 更強的結構
- 更合理的語言
- 更精細的搜尋
這可能比我們想像中重要得多。