AlphaGeometry DSL 教程：Google 幾何構造語言、defs.txt 與 Predicate 詳解

本文僅討論 AlphaGeometry DSL 本身，不討論模型訓練、搜尋策略或論文結果。

目標是把這套 DSL 當作一份面向研發的協議說明書來拆解，回答以下問題：

問題輸入如何編碼
defs.txt 中 action 如何定義
幾何關係如何映射為 predicate
數值構造與符號推理如何銜接

如果要復現 AlphaGeometry、編寫幾何資料生成器，或為自定義 solver 設計相容層，理解 DSL 協議是基礎前置工作。

一、DSL 的角色定義

AlphaGeometry DSL 是一套面向幾何構造與關係表達的領域語言。它主要承擔 3 個職責：

表達初始幾何前提
表達可執行的構造動作
表達待驗證的幾何目標

其輸出不是最終證明文本，而是可供推理引擎消費的幾何關係集合。

從實作角度看，DSL 更接近一層中間表示：

上游連接題目描述或資料生成器
中游連接 action 定義與關係展開
下游連接 rules.txt 與 DDAR 推理

協議核心不在「圖形繪製」，而在「關係生成」。

二、問題檔案結構

一個完整問題通常寫成：

problem_name
premises ? goal

示例：

orthocenter
a b c = triangle;
h = on_tline b a c, on_tline c a b
? perp a h b c

可以拆成 3 個區塊：

a b c = triangle; 初始前提與自由對象
h = on_tline b a c, on_tline c a b 基於已知對象執行構造
? perp a h b c 目標 predicate

這段 DSL 的含義不是自然語言題解，而是一段幾何程式：

Premises
  -> constructions
  -> predicate graph
  -> goal checking

解析後，系統通常需要產出：

初始對象表
action 呼叫序列
predicate 初始集合
待檢查目標

三、基本語法約定

DSL 的核心表達形式是：

output = action(parameters)

示例：

h = on_tline b a c, on_tline c a b

表示點 h 同時滿足兩個構造約束：

過 b 作直線，垂直於 ac
過 c 作直線，垂直於 ab

因此 h 是兩條垂線的交點。

這類表達具有兩個特點：

輸出變數統一使用點變數
幾何對象透過點集隱式表示，而非獨立對象型別

例如：

line a b
circle o a

line a b 表示由點 a、b 定義的直線
circle o a 表示圓心 o、經過點 a 的圓

這種設計簡化了解析器與關係圖結構，但要求 predicate 系統足夠強，能覆蓋直線、圓與角的高層語義。

四、`defs.txt` 中 action 的定義結構

defs.txt 是 action 註冊表。每個 action 通常由 5 個部分組成：

action_name outputs inputs

variable dependency

input conditions

geometric constraints

numerical constructions

示例：

midpoint x a b
x : a b
a b = diff a b
x : coll x a b, cong x a x b
midp a b

各部分作用如下。

1. action 簽名

midpoint x a b

表示：

action 名稱為 midpoint
輸出點為 x
輸入點為 a b

2. 變數依賴

x : a b

表示輸出變數 x 依賴於輸入 a、b。

這部分通常用於構造依賴圖或變數作用域管理。

3. 輸入合法性條件

a b = diff a b

表示 a 和 b 必須是不同點。

這一層用於阻止退化構造，不直接生成證明關係。

4. 幾何約束

x : coll x a b, cong x a x b

表示 action 完成後必須成立的 predicate：

coll x a b，即 x 與 a、b 共線
cong x a x b，即 XA = XB

這部分是 action 的符號語義定義，也是後續推理系統消費的主要輸入。

5. 數值構造介面

midp a b

表示底層數值引擎應呼叫中點構造。

數值層的典型用途包括：

生成具體座標實例
檢查構造是否退化
為 predicate 提供數值真值校驗

五、predicate 系統

predicate 是 AlphaGeometry 推理系統的核心輸入格式。

常見核心謂詞包括：

predicate	含義
`coll A B C`	三點共線
`cong A B C D`	`AB = CD`
`perp A B C D`	`AB ⟂ CD`
`para A B C D`	`AB ∥ CD`
`eqangle ...`	角相等
`cyclic A B C D`	四點共圓

這些 predicate 會進入 rules.txt 所定義的規則系統，觸發進一步推導。

典型流程如下：

construction
  -> initial predicates
  -> rule firing
  -> new predicates
  -> goal reached / not reached

因此 DSL 的核心不是動作目錄本身，而是 predicate 生成能力。

一個 action 是否有價值，主要取決於：

能引入哪些 predicate
這些 predicate 是否容易觸發規則鏈
是否能顯著縮短目標證明路徑

六、常見 action 類型

1. 基礎對象

free a
triangle a b c
quadrangle a b c d

free 生成自由點
triangle 生成三角形的 3 個基礎點
quadrangle 生成四邊形的 4 個基礎點

2. 點落在線或圓上

on_line x a b
on_circle x o a
on_pline x a b c
on_tline x a b c

on_line 對應共線約束
on_circle 對應等半徑約束
on_pline 對應平行約束
on_tline 對應垂直約束

3. 交點構造

intersection_ll x a b c d
intersection_lc x a o b
intersection_cc x o w a

分別表示：

兩線交點
線與圓交點
兩圓交點

4. 基本幾何構造

midpoint x a b
foot x a b c
mirror x a b

midpoint 生成中點
foot 生成垂足
mirror 生成對稱點

這類 action 的特點是單次呼叫即可引入多條高密度關係。

5. 三角形中心

例如：

circumcenter x a b c
incenter x a b c
excenter x a b c
centroid x y z i a b c
ninepoints x y z i a b c

這類 action 通常會一次性引入多組關係，如等距、角平分與垂直平分等。

6. 特殊多邊形

例如：

square a b x y
rectangle a b c d
parallelogram a b c x
trapezoid a b c d
eq_trapezoid a b c d

這類 primitive 的特點是初始關係更強，更適合生成結構化題目或高約束訓練樣本。

七、示例解析

示例：

orthocenter
a b c = triangle;
h = on_tline b a c, on_tline c a b
? perp a h b c

執行過程如下。

第一步：解析前提

triangle a b c 生成基礎點集與非退化條件。

第二步：執行構造

h 被定義為以下兩條約束的交點：

過 b 且垂直於 ac
過 c 且垂直於 ab

第三步：落成 predicate

構造動作被轉成：

perp b h a c
perp c h a b

第四步：驗證目標

系統檢查是否能推出：

perp a h b c

如果可以推出，則目標成立；否則該問題在當前構造與規則集下尚未被證明。

八、執行 pipeline

從問題文本到目標驗證，典型 pipeline 如下：

Problem DSL
  -> parse.py
  -> action expansion via defs.txt
  -> geometry graph
  -> predicate inference via rules.txt
  -> DDAR solver

各階段職責如下：

解析問題文本，識別前提、構造與目標
查找 defs.txt 中對應的 action 定義
展開變數依賴、輸入條件與幾何約束
把約束寫入幾何關係圖
依據 rules.txt 觸發新的 predicate
對目標 predicate 做可達性檢查

數值構圖與符號推理在該流程中通常並行存在：

數值層負責實例化與真值檢查
符號層負責嚴格推導與證明追蹤

九、實作注意事項

1. action 設計應面向關係產出

一個 action 是否值得保留，應優先評估其 predicate 產出品質，而不是幾何含義是否「直觀」。

2. 必須顯式處理退化條件

如點重合、平行線無交點、零半徑圓等情況，都應在輸入條件或數值層被攔截。

3. predicate 集合決定可表達上限

若系統只能表達共線、平行與垂直，複雜幾何題的表示能力會很快受限。

4. 數值層介面不應省略

如果只有符號定義而沒有數值構造介面，資料生成、除錯與真值校驗成本會顯著上升。

十、最小可實作子集建議

若需要實作與 AlphaGeometry 思路相容的最小版本，可優先支援以下 action：

triangle
on_line
on_tline
on_pline
intersection_ll
midpoint
foot

並至少支援以下 predicate：

coll
perp
para
cong
cyclic
eqangle

這是一個較小但可工作的協議核心。

十一、協議本質

AlphaGeometry DSL 可以概括為：

Geometry Construction DSL
+ Predicate Interface
+ Rule-System Input Layer

它的主要價值不在於「描述圖形」，而在於把幾何問題壓縮成一個可執行、可驗證、可推理的協議層。

十二、靠譜推薦：大角幾何（Dino-GSP）

如果需要一個比 AlphaGeometry DSL 更開放、面向產品與生態整合的幾何表達環境，可以看我推出的大角幾何（Dino-GSP）。

它同樣把幾何對象表示為可執行結構，並且也定義了自己的 DSL 與約束表示層，用於支援：

更開放的幾何構造與編輯流程
面向教學、內容生產與 AI 幾何應用的生態接入
圖形生成、約束驗證、輔助結構構造等可程式化能力

如果把 AlphaGeometry DSL 看成偏求解器與研究系統內部協議，大角幾何則更偏向可擴展產品層與開放生態介面。