AlphaGeometry2 - 金牌等級的 AI 幾何定理自動證明系統

1. 專案概述 (Project Overview)

1.1 什麼是 AlphaGeometry2

AlphaGeometry2 是 Google DeepMind 開發的 幾何定理自動證明系統 (automated geometry theorem prover)，為 2024 年發表的 AlphaGeometry 之重大升級版本。該系統在解決 國際數學奧林匹克 (International Mathematical Olympiad, IMO) 幾何問題上，已達到甚至超越 金牌得主 (gold medalist) 的平均水準。

相關論文於 2025 年發表於 Journal of Machine Learning Research (JMLR)：

Chervonyi, Y., Trinh, T.H., Olsak, M., et al. (2025). Gold-medalist performance in solving olympiad geometry with AlphaGeometry2. JMLR, 26(241), 1-39.

1.2 核心能力

1.3 專案基本資訊

1.4 系統定位

graph TD
    subgraph "AI for Mathematics (AI 數學應用)"
        A["AlphaProof
代數 / 數論"] 
        B["AlphaGeometry2
幾何證明"]
        C["FunSearch
組合數學"]
    end

    subgraph "核心方法"
        D["Symbolic Engine
符號引擎 DDAR"]
        E["Language Model
語言模型"]
    end

    B --> D
    B --> E
    D -->|"邏輯推導"| F["完整證明
(Complete Proof)"]
    E -->|"輔助點建議"| D

    style B fill:#4285F4,color:#fff,stroke:#1a73e8
    style D fill:#34A853,color:#fff
    style E fill:#FBBC04,color:#333

2. 核心架構與技術原理 (Architecture & Technical Principles)

2.1 雙引擎架構 (Dual-Engine Architecture)

AlphaGeometry2 的核心設計是 神經符號混合系統 (neuro-symbolic hybrid system)，結合兩個互補的引擎：

1. DDAR 符號引擎 (Deductive Database with Algebraic Rules)：基於嚴格的幾何公理 (axioms) 與推理規則 (inference rules) 進行邏輯推導。
2. 語言模型 (Language Model)：當 DDAR 無法直接完成證明時，由語言模型提議輔助構造 (auxiliary constructions)，例如新增輔助點 (auxiliary points)、輔助線 (auxiliary lines) 等。

flowchart LR
    subgraph Input["輸入層 (Input)"]
        P["幾何問題
形式化描述"]
        C["點座標
(Point Coordinates)"]
    end

    subgraph DDAR["DDAR 符號引擎"]
        D1["幾何公理庫
(Axiom Database)"]
        D2["代數規則
(Algebraic Rules)"]
        D3["前向推導
(Forward Chaining)"]
        D4["反向推導
(Backward Chaining)"]
    end

    subgraph LM["語言模型"]
        L1["問題編碼
(Problem Encoding)"]
        L2["輔助點預測
(Auxiliary Point Prediction)"]
    end

    P --> D3
    C --> D3
    D1 --> D3
    D2 --> D3
    D3 --> D4
    D4 -->|"證明完成"| R1["Proven :-)"]
    D4 -->|"需要輔助構造"| L1
    L1 --> L2
    L2 -->|"新增輔助點"| D3

    style DDAR fill:#e8f5e9,stroke:#2e7d32
    style LM fill:#fff3e0,stroke:#e65100
    style R1 fill:#c8e6c9,stroke:#2e7d32,color:#1b5e20

2.2 程式碼模組結構

本倉庫開源的是 DDAR 符號引擎部分，共包含五個核心 Python 模組：

2.3 DDAR 推理流程

DDAR (Deductive Database with Algebraic Rules) 是 AlphaGeometry2 的核心邏輯引擎。其推理流程 (reasoning pipeline) 可拆解為以下步驟：

1. 問題解析 (Problem Parsing)：將形式化的幾何描述轉換為內部表示 (internal representation)。
2. 事實資料庫初始化 (Fact Database Initialization)：根據問題條件建立初始已知事實 (known facts)。
3. 前向推導 (Forward Chaining)：基於公理規則，從已知事實推導出新事實。
4. 反向推導 (Backward Chaining)：從目標結論 (goal) 反向尋找所需條件。
5. 代數消去 (Algebraic Elimination)：對包含代數關係的幾何條件進行化簡。
6. 數值驗證 (Numerical Verification)：以座標數值確認推導結果的一致性。

2.4 AlphaGeometry2 vs AlphaGeometry (v1) 改進

3. 安裝與環境設定 (Installation & Setup)

3.1 系統需求 (System Requirements)

3.2 安裝步驟

步驟一：安裝系統依賴

1# Ubuntu / Debian
2sudo apt install python3 python3-pip python3-venv
3
4# macOS (透過 Homebrew)
5brew install python3

步驟二：建立虛擬環境 (virtual environment)

1python3 -m venv ag2
2source ag2/bin/activate

步驟三：安裝 Python 套件

1pip install numpy

步驟四：下載專案程式碼

1git clone https://github.com/google-deepmind/alphageometry2.git
2cd alphageometry2

3.3 驗證安裝

1python -m test

成功時會看到 26 道 IMO 題目逐一被證明，每題結尾顯示 Proven :-)。

3.4 安裝流程圖

flowchart TD
    A["開始安裝"] --> B{"作業系統?"}
    B -->|"Ubuntu/Debian"| C["apt install python3
python3-pip python3-venv"]
    B -->|"macOS"| D["brew install python3"]
    B -->|"Windows"| E["安裝 WSL2
→ 回到 Ubuntu 路徑"]
    
    C --> F["python3 -m venv ag2"]
    D --> F
    E --> C
    
    F --> G["source ag2/bin/activate"]
    G --> H["pip install numpy"]
    H --> I["git clone repo"]
    I --> J["python -m test"]
    J --> K{"26 題全部 Proven?"}
    K -->|"Yes"| L["安裝完成"]
    K -->|"No"| M["檢查 Python 版本
與 numpy 安裝"]
    M --> F

    style L fill:#c8e6c9,stroke:#2e7d32
    style A fill:#e3f2fd,stroke:#1565c0

4. 使用教學與範例 (Usage Tutorial & Examples)

4.1 執行內建測試集

最直接的使用方式是執行內建的 26 道 IMO 幾何題測試：

1# 啟動虛擬環境
2source ag2/bin/activate
3
4# 進入專案目錄
5cd alphageometry2
6
7# 執行完整測試
8python -m test

4.2 測試集分類

test.py 中包含兩類問題：

類別 A：DDAR 獨立可解 (DDAR-only solvable)

這些問題不需要語言模型提供輔助點，DDAR 引擎可以獨立完成證明：

類別 B：需手動輔助點 (requires manually provided auxiliary points)

這些是更具挑戰性的問題，在本倉庫中以手動提供輔助點的方式求解（完整系統中由語言模型自動生成）：

4.3 理解 AlphaGeometry2 形式化語言

AlphaGeometry2 使用自訂的 形式化幾何語言 (formal geometry language) 來描述問題。核心元素包括：

基本構造 (basic constructions)：

• 點定義 (point definitions)：透過幾何關係（如交點、中點）定義新點
• 約束條件 (constraints)：如共線 (collinear)、共圓 (concyclic)、垂直 (perpendicular)、平行 (parallel)

座標補充 (coordinate supplements)：

• 每個問題會附帶數值座標，用於數值驗證 (numerical verification)
• 座標並不影響符號證明的邏輯正確性

目標聲明 (goal statement)：

• 明確指出需要證明的幾何性質

4.4 DDAR 推理輸出解讀

執行時，每個 . 代表一輪推理迭代 (reasoning iteration)：

1Problem: 2008_p6
2...... Proven :-)

• 6 個點表示 DDAR 經過 6 輪前向/反向推導
• Proven :-) 表示目標結論已從推導事實中導出
• 若未能證明，則不會輸出 Proven

4.5 模組化呼叫

各模組也可獨立匯入使用：

 1# 解析幾何問題
 2from parse import parse_problem
 3
 4# 執行 DDAR 推理
 5from ddar import run_ddar
 6
 7# 數值驗證
 8from numericals import compute_coordinates
 9
10# 代數消去
11from elimination import eliminate

5. 進階功能與最佳實踐 (Advanced Features & Best Practices)

5.1 自訂幾何問題

雖然本倉庫主要提供內建測試集，但可以參考 test.py 中的問題格式，嘗試定義自己的幾何問題：

1. 以 AlphaGeometry2 形式化語言撰寫問題描述
2. 提供數值座標作為輔助驗證
3. 指定證明目標 (proof goal)
4. 若問題超出 DDAR 能力，手動提供輔助構造

5.2 理解推理深度

不同問題需要的推理深度 (reasoning depth) 差異很大：

5.3 符號引擎的限制與規避

DDAR 作為純符號系統，有其固有限制：

• 無法自動生成輔助構造：本倉庫不含語言模型部分，複雜問題需手動提供輔助點
• 問題必須形式化：需將自然語言題目翻譯為 AlphaGeometry2 語言
• 推理規則有限：某些涉及極端技巧的幾何問題可能超出規則庫

5.4 與完整系統的關係

本倉庫是 AlphaGeometry2 完整系統的符號核心。完整系統還包括：

• Gemini 語言模型：用於自動生成輔助構造（未開源）
• 搜尋與回溯機制 (search and backtracking)：嘗試多種輔助構造組合
• 訓練資料生成管線 (training data pipeline)：合成幾何問題用於訓練

5.5 效能調優建議

• 本系統為 CPU-only，不需 GPU 加速
• NumPy 用於座標數值計算，確保安裝正確版本
• 對於大規模批次測試，可修改 test.py 選擇性執行特定問題子集
• 推理過程記憶體佔用低（純符號運算），適合資源受限環境

6. 應用價值與整合潛力 (Application Value & Integration Potential)

6.1 學術研究價值

AlphaGeometry2 在多個面向具有重要的學術意義：

• 自動定理證明 (Automated Theorem Proving, ATP)：展示了神經符號混合方法在數學推理中的突破性進展
• AI for Science：作為 AI 解決高等數學問題的標竿案例
• 形式化驗證 (Formal Verification)：DDAR 引擎的推理過程可追蹤、可驗證，不同於純神經網路的黑箱推理

6.2 教育應用

6.3 技術整合方向

graph LR
    AG2["AlphaGeometry2
DDAR 引擎"]
    
    AG2 --> I1["教育平台
(Education Platform)"]
    AG2 --> I2["形式化數學系統
(Lean / Coq / Isabelle)"]
    AG2 --> I3["幾何繪圖工具
(GeoGebra 等)"]
    AG2 --> I4["自動出題系統
(Problem Generation)"]
    AG2 --> I5["數學研究輔助
(Research Assistant)"]

    I1 -->|"互動式證明教學"| U1["學生 / 教師"]
    I2 -->|"證明轉換與驗證"| U2["數學家 / 研究員"]
    I3 -->|"視覺化 + 自動證明"| U3["競賽教練"]
    I4 -->|"程序化生成題庫"| U4["考試命題"]
    I5 -->|"猜想驗證"| U5["數學研究"]

    style AG2 fill:#4285F4,color:#fff,stroke:#1a73e8
    style I1 fill:#e8f5e9,stroke:#2e7d32
    style I2 fill:#fff3e0,stroke:#e65100
    style I3 fill:#e3f2fd,stroke:#1565c0
    style I4 fill:#fce4ec,stroke:#c62828
    style I5 fill:#f3e5f5,stroke:#7b1fa2

6.4 產業應用潛力

雖然 AlphaGeometry2 專注於幾何證明，其底層技術（神經符號混合推理 neuro-symbolic reasoning）可延伸至：

• 電路設計驗證 (circuit design verification)：幾何約束求解
• 機器人運動規劃 (robotic motion planning)：空間幾何推理
• 電腦視覺 (computer vision)：場景幾何理解
• 建築設計 (architectural design)：空間關係推導

7. 常見問題與限制 (FAQ & Limitations)

7.1 常見問題 (Frequently Asked Questions)

Q1: 這個倉庫是完整的 AlphaGeometry2 系統嗎？

不是。本倉庫僅包含 DDAR 符號引擎 (symbolic engine)，即邏輯推理核心。完整系統中用於生成輔助構造的 Gemini 語言模型部分 未開源。因此，對於需要輔助構造的複雜問題，本倉庫中是以手動提供輔助點的方式示範。

Q2: 我可以用它來解任意幾何問題嗎？

理論上可以，但有前提：

• 問題必須以 AlphaGeometry2 的形式化語言表達
• 需要提供數值座標
• 若問題超出 DDAR 能力範圍，需手動提供輔助構造

Q3: 為什麼不需要 GPU？

DDAR 引擎是純符號推理系統 (purely symbolic reasoning system)，所有運算都是邏輯推導與代數操作，不涉及神經網路計算。NumPy 僅用於座標的數值驗證。

Q4: 與 Lean / Coq 等形式化證明助手有何不同？

Q5: 論文在哪裡可以取得？

論文發表於 JMLR：

• 標題：Gold-medalist performance in solving olympiad geometry with AlphaGeometry2
• JMLR Vol 26, No. 241, 2025
• URL: https://www.jmlr.org/papers/v26/25-1654.html

7.2 已知限制 (Known Limitations)

1. 僅包含符號引擎：語言模型部分未開源，無法完全重現論文中報告的完整系統效能
2. 問題形式化瓶頸 (formalization bottleneck)：將自然語言題目轉換為 AlphaGeometry2 語言需要專業知識
3. 推理規則有限 (limited inference rules)：DDAR 的公理庫覆蓋歐幾里得平面幾何 (Euclidean plane geometry)，不支援射影幾何 (projective geometry)、非歐幾何 (non-Euclidean geometry) 等
4. 無視覺化輸出 (no visualization output)：系統僅輸出文字證明步驟，不生成幾何圖形
5. 無互動式介面 (no interactive interface)：目前僅提供命令列批次執行方式
6. 座標依賴 (coordinate dependency)：問題描述需附帶數值座標，增加了問題準備的工作量

7.3 延伸資源 (Further Resources)

• 論文：JMLR Vol 26, 2025
• 前作 AlphaGeometry：Nature, 2024
• Google DeepMind 部落格：搜尋 “AlphaGeometry2” 獲取科普介紹
• IMO 題目資料庫：Art of Problem Solving

附錄：引用格式 (Citation)

 1@article{chervonyi2025gold,
 2  title={Gold-medalist performance in solving olympiad geometry 
 3         with alphageometry2},
 4  author={Chervonyi, Yuri and Trinh, Trieu H and Ol{\v{s}}{\'a}k, 
 5          Miroslav and Yang, Xiaomeng and Nguyen, Hoang H and 
 6          Menegali, Marcelo and Jung, Junehyuk and Kim, Junsu and 
 7          Verma, Vikas and Le, Quoc V and others},
 8  journal={Journal of Machine Learning Research},
 9  volume={26},
10  number={241},
11  pages={1--39},
12  year={2025}
13}

本教學文件基於 google-deepmind/alphageometry2 倉庫內容撰寫。 軟體部分以 Apache 2.0 授權，其他素材以 CC-BY 4.0 授權。 This is not an official Google product.