結構變種、表面變種與命題分叉：AI 原生知識展開中的合法變換判定

Q: 4. 不變量：什麼必須被保留？

對一個指定變換類型 $T$，不應要求所有元素都不變，而應指定「該類變換允許改什麼、禁止改什麼」。

English Title: Structural Variation, Surface Variation, and Proposition Branching: Legality Tests for AI-Native Knowledge Expansion
Series: AI-Native Knowledge Expansion, Paper II
Author: Neo.K
Collaborator: Aletheia (GPT-5.6 Sol)
Institution: EveMissLab / 一言諾科技有限公司
Version: v0.1
Date: 2026-08-10

摘要

〈基底知識空間擴張〉提出：可靠基礎知識經過大量合法、可驗證的展開與重組，可以形成高品質的 AI 推理資料。然而，只要允許大規模自動生成，立即會出現一個更基本的問題：什麼才算真正不同的變種？

若僅更換變數名稱、數值、自然語言措辭或公式排列方式，資料量可以快速膨脹，但有效結構資訊幾乎沒有增加。反之，一個看似只修改單一條件的命題，卻可能已經改變其定義域、量詞、充分必要條件、依賴圖或可證性，從「同一命題的變種」分叉為新的命題族。

本文建立 AI 原生知識展開中的「合法變換判定框架」。我們區分四個層級：表面變種、表示變種、結構變種與命題分叉；定義命題的結構指紋、保留不變量、變換算子、標準形與分叉條件；並提出「變種證書」（Variation Certificate），使每一個 AI 生成節點都必須回答：它從哪個母命題產生、改變了什麼、保留了什麼、與母命題是等價、強化、弱化、特化、泛化、對偶、反例，還是已形成新的命題。

本文主張：AI 原生資料生成真正需要最大化的不是樣本數，而是經過等價類去重後的有效結構覆蓋。在此意義上，canonicalization、equivalence detection 與 proposition branching 不是資料清理的後處理，而是 BKSE 的核心生成規則。

關鍵詞： 結構變種；表面變種；命題分叉；基底知識空間擴張；標準形；等價類；形式驗證；AI 合成資料；知識圖；變種證書

1. 從「生成更多」轉向「生成真正不同」

Paper I 定義：

\mathcal E(P) = \{\text{legal verified neighbors of }P\}.

但這個定義留下了一個關鍵詞：

\text{legal}.

什麼是合法？

更進一步：

P_1\neq_{\text{text}}P_2

是否就代表：

P_1\neq_{\text{structure}}P_2?

答案顯然不是。

例如：

a^2+b^2=c^2

和：

c^2=a^2+b^2

在字面順序上不同，但數學命題沒有增加。

甚至：

x^2+y^2=z^2

也只是變數重新命名。

因此：

\boxed{ \text{Surface Difference} \not\Rightarrow \text{Structural Difference}. }

反方向也成立。一個只修改一個符號的命題：

\forall x,\ P(x)

改成：

\exists x,\ P(x)

文字差異極小，但邏輯結構已根本不同。

所以 AI-native generation 若只以文字差異率、embedding distance 或 token diversity 衡量資料多樣性，很容易製造大量「看起來不同、其實相同」的資料，或把真正的新命題誤歸為原命題的同義變種。

2. 四層變種分類

本文先定義四個層級。

2.1 L0：表面變種（Surface Variation）

只改變外部表示，不改變可識別的語義或形式結構。

例如：

a^2+b^2=c^2

與：

x^2+y^2=z^2.

或自然語言：

兩股平方和等於斜邊平方。

與：

在直角三角形中，斜邊平方等於兩直角邊平方之和。

若兩者指向完全相同的形式命題，則屬於：

V_0.

典型操作包括變數重新命名、語序調整、同義改寫、格式改變、括號或排版改變，以及不改變意義的符號替換。

這類資料可服務語言魯棒性，但不應被計入主要的結構擴張量。

2.2 L1：表示變種（Representational Variation）

核心數學對象不變，但使用不同表示系統。

例如畢氏定理可寫為：

a^2+b^2=c^2,

也可寫成內積形式：

\|u+v\|^2 = \|u\|^2+\|v\|^2, \qquad \langle u,v\rangle=0.

或座標形式：

(x_2-x_1)^2+(y_2-y_1)^2=d^2.

此時不同表示可能揭露不同推理路徑，所以資訊價值高於 L0，但它們仍可能屬於同一個核心定理族。

記為：

V_1.

2.3 L2：結構變種（Structural Variation）

至少一個推理結構發生改變，但仍能明確追溯到母命題。

例如：

正命題轉逆命題；
固定部分變數，改成求解問題；
將定理嵌入幾何／代數／向量不同模組；
移除或增加條件；
從二維推廣到 (n) 維；
將存在性問題改為分類問題；
把結果改成極值或可實現域問題。

這一層記為：

V_2.

2.4 L3：命題分叉（Proposition Branching）

當變換改變了核心定義域、量詞、依賴、真值條件、對象類型或主要結論，使新節點不能再合理稱為「同一命題的變種」，則應建立新的命題 ID。

記為：

V_3.

例如：

P: \forall x\in D,\ A(x)\Rightarrow B(x)

若改成：

P': \exists x\in D,\ A(x)\Rightarrow B(x),

即使只改一個量詞，也應視為命題分叉。

因此：

\boxed{ V_0 \rightarrow V_1 \rightarrow V_2 \rightarrow V_3 }

不是單純難度排序，而是「結構偏離母命題程度」的分類。

3. 命題結構指紋

為了判斷兩個命題是否仍屬於同一結構族，本文定義一個概念性的結構指紋：

\boxed{ \Phi(P) = ( \mathcal D, \mathcal O, \mathcal Q, \mathcal A, \mathcal R, \mathcal C, \mathcal K ) }

其中：

$\mathcal D$ ：domain，定義域；
$\mathcal O$ ：objects，主要對象與型別；
$\mathcal Q$ ：quantifiers，量詞結構；
$\mathcal A$ ：assumptions，假設；
$\mathcal R$ ：relations，核心關係；
$\mathcal C$ ：conclusion，結論；
$\mathcal K$ ：dependency kernel，必要依賴骨架。

如果 AI 只把 (a,b,c) 改成 (x,y,z)，則：

\Phi(P')=\Phi(P).

若把平面改成任意內積空間，但仍保持正交平方和結構，則可能：

\Phi(P')\neq\Phi(P)

但存在清楚的泛化映射：

P\hookrightarrow P'.

這應標記為 structural generalization，而不是普通等價。

4. 不變量：什麼必須被保留？

對一個指定變換類型 (T)，不應要求所有元素都不變，而應指定「該類變換允許改什麼、禁止改什麼」。

定義：

I_T(P)

為變換 (T) 必須保留的不變量集合。

例如變數重新命名：

T_{\alpha}

必須保留：

I_{T_\alpha} = \{ \mathcal D, \mathcal O, \mathcal Q, \mathcal A, \mathcal R, \mathcal C, \mathcal K \}.

而泛化算子：

T_{\mathrm{gen}}

則允許 $\mathcal D$ 擴張，但要求原命題可嵌入新命題：

P = P'|_{\mathcal D_0}.

因此，合法性不是一個全域布林值，而是：

\boxed{ \operatorname{Legal}(T,P,P') }

依變換種類而定。

5. 八種基本變換算子

BKSE 可以先定義一套最小操作語彙。

5.1 Alpha / Surface Renaming

T_\alpha(P)

只改變符號或名稱。

預期：

P\equiv T_\alpha(P).

5.2 Equivalent Rewrite

T_{\mathrm{eq}}(P)

使用已證明等價規則重新表示。

預期：

P\leftrightarrow T_{\mathrm{eq}}(P).

5.3 Specialization

T_{\mathrm{spec}}(P)

把一般命題限制到子域：

D'\subseteq D.

通常：

P\Rightarrow T_{\mathrm{spec}}(P),

但反向不一定成立。

5.4 Generalization

T_{\mathrm{gen}}(P)

擴張定義域或對象類型。

要求至少能證明在原域嵌入下：

T_{\mathrm{gen}}(P) \Rightarrow P.

5.5 Assumption Ablation

對：

A=\{A_1,\ldots,A_n\}

移除 $A_i$ ，得到：

P_{-A_i}.

若仍可證，則原假設可能冗餘；若找到反例，則得到假設必要性證據。

5.6 Converse / Dualization

若：

P:A\Rightarrow B,

則生成：

T_{\mathrm{conv}}(P): B\Rightarrow A.

它不預設成立，而是問題生成器。

5.7 Composition

T_{\mathrm{comp}}(P,Q)

把兩個已有命題接成新結構。

若：

P:A\Rightarrow B, \qquad Q:B\Rightarrow C,

可生成候選：

A\Rightarrow C.

但只有中間型別、假設與語義接口一致時才合法。

5.8 Counterfactual / Error-Neighborhood Mutation

刻意修改一個條件，使命題成為 near-miss：

T_{\mathrm{err}}(P).

其目標不是保存真值，而是產生錯誤鄰域，並附最小反例或失敗原因。

6. 標準形與等價類

如果 AI 每生成一個節點都直接存進資料庫，BKSE 很快就會被等價重複淹沒。

因此定義 canonicalization：

\operatorname{Can}(P) = P^\ast.

若：

\operatorname{Can}(P_1) = \operatorname{Can}(P_2),

則優先將兩者歸入同一等價類：

[P] = \{Q:Q\sim P\}.

這裡的 $\sim$ 可以分層：

\sim_{\alpha}, \quad \sim_{\mathrm{def}}, \quad \sim_{\mathrm{logic}}, \quad \sim_{\mathrm{semantic}}.

分別表示變數重命名等價、定義展開等價、可證邏輯等價，以及更高層語義等價。

不能把所有等價都混成單一關係。

因此資料庫應區分：

\text{identity} \neq \text{equivalence} \neq \text{useful alternative representation}.

7. 結構距離

為了做自動 frontier scheduling，可以定義概念性的結構距離：

d_S(P,Q) = \sum_i w_i \delta_i( \Phi_i(P), \Phi_i(Q) ).

例如：

d_S = w_D\Delta_D + w_Q\Delta_Q + w_A\Delta_A + w_R\Delta_R + w_C\Delta_C + w_K\Delta_K.

這個距離不是普通 embedding distance。

兩段自然語言可以 embedding 很接近，但若一個使用 $\forall$ 、另一個使用 $\exists$ ，結構距離應很大。

反之，一條公式與一段長篇自然語言說明，字面距離很大，但形式結構距離可以接近 0。

因此：

\boxed{ d_{\mathrm{text}} \neq d_{\mathrm{semantic}} \neq d_{\mathrm{structural}}. }

8. 命題分叉條件

何時必須建立新 proposition ID？

本文提出最小規則：若以下任一核心元素發生未被父變換類型允許的改變，則應 branch：

定義域改變；
主要對象型別改變；
量詞改變；
核心假設改變；
真值條件改變；
主要結論改變；
必要依賴骨架改變；
從 theorem 變成 optimization / classification / existence 等不同任務型別。

形式上：

\exists i: \Phi_i(P)\neq \Phi_i(P') \land i\notin \operatorname{AllowedChange}(T)

則：

\boxed{ \operatorname{Branch}(P,P')=1. }

9. 變種證書（Variation Certificate）

每個生成節點應附：

variation_id
parent_id
operator
source_fingerprint
target_fingerprint
preserved_invariants
changed_dimensions
formal_relation
verification_method
canonical_form
equivalence_class
branch_status
counterexample_status

其中：

\text{formal\_relation} \in \{ =,\leftrightarrow,\Rightarrow,\Leftarrow, \subset,\supset, \text{incomparable}, \text{unknown} \}.

因此 AI 不能只說：

我生成了一個新變種。

而必須能說：

它是 (P) 的 specialization；保留核心關係與結論，縮小 domain；canonicalization 後不與現有節點重複；形式關係已驗證。

這才是可用的 AI-native research object。

10. 畢氏定理的最小示例

令：

P_0: \angle C=90^\circ \Rightarrow a^2+b^2=c^2.

若只是：

x^2+y^2=z^2,

則主要是：

V_0.

若改寫成：

c=\sqrt{a^2+b^2}, \qquad c>0,

則在適當 domain 下屬表示等價：

V_1.

若改成：

a^2+b^2=c^2 \Rightarrow \angle C=90^\circ,

則是 converse：

V_2.

若進一步研究：

a^2+b^2>c^2

與角度分類，則已進入新的分類命題家族，應建立獨立 proposition ID，但保留 lineage。

若推廣到內積空間：

u\perp v \Rightarrow \|u+v\|^2 = \|u\|^2+\|v\|^2,

則屬 generalization，原直角三角形命題可以視為其具體 instance。

因此：

P_{\mathrm{Pyth}} \hookrightarrow P_{\mathrm{inner}}.

兩者不應被壓成同一節點。

11. 與形式證明器的接口

形式系統特別適合判定 L0–L2 的部分關係，例如：

definitional equality；
alpha-equivalence；
equality proof；
iff proof；
implication；
subtype specialization；
instance inheritance。

Lean 的 simp 使用已註冊的 equality / iff theorem 把表達式改寫成較標準的形式；Lean 官方也明確區分 simplification 與一般 rewriting：前者強調把問題 reformulate 成較標準、適合後續證明的形態，而後者是更具方向性的手選改寫。

這給 BKSE 一個重要啟示：

\boxed{ \text{Canonicalization is not merely text normalization.} }

它應盡可能由：

\text{proved rewrite rules}

驅動。

但形式證明器仍無法單獨回答所有「研究上是否值得視為新結構」的問題。

所以：

\text{formal equivalence} \neq \text{research redundancy}.

12. 從抽象結構到 instance

近期 autoformalization 工作已開始明確使用「抽象結構 → 具體 instance」方向。SITA 將抽象數學結構視為包含 definitions、assumptions、operations 與 theorems 的 reusable template，再生成具體 Lean instance 並檢查結構假設。

這非常接近：

T_{\mathrm{spec}}: P_{\mathrm{abstract}} \rightarrow P_{\mathrm{instance}}.

其核心不是產生更多文字，而是保留：

\text{structural assumptions}.

因此 transformation lineage 可以直接成為形式資料集 metadata。

13. 程式語言中的對應問題

相同框架也適用程式碼。

若只改：

x -> item

屬 L0。

若 Python 改寫成 Rust，但演算法與輸入輸出語義保持一致，可能屬 L1。

若把：

O(n^2)

演算法改為：

O(n\log n),

即使輸出功能一致，內部演算法結構已不同，屬 L2。

若 API 行為、輸入域或 side-effect contract 改變，則可能屬 L3。

因此：

\text{behavioral equivalence} \neq \text{algorithmic identity}.

BKSE 必須維護多種 equivalence relation，而不能只靠 hash 或 embedding。

14. 有效結構覆蓋

Paper I 定義概念性的有效結構資料量。本篇進一步提出：

\boxed{ C_{\mathrm{eff}}(D) = \sum_{[P]\in D/\sim} w([P]) }

即：先依適當等價關係去重，再計算有效覆蓋。

因此資料集報告應同時給：

[ |D|, ]

|D/\sim|,

\text{branch count},

\text{operator distribution},

\text{verification rate}.

這比只說「合成了多少 samples」更能反映知識增量。

15. 最小演算法

BKSE 的變種引擎可以寫成：

INPUT: verified node P

1. fingerprint(P)
2. choose operator T
3. generate candidate P'
4. infer intended relation R(P,P')
5. canonicalize(P')
6. search equivalent existing nodes
7. verify relation R
8. compare fingerprints
9. classify V0 / V1 / V2 / V3
10. if duplicate:
       attach alternative representation/proof
    elif legal variation:
       add child node
    elif proposition branch:
       create new proposition ID with lineage
    else:
       reject or store as negative/error node
11. emit Variation Certificate

核心不是第 3 步的「生成」。

真正困難的是：

[ 4,5,6,7,8,9,10. ]

也就是分類、標準化、去重、驗證與身份管理。

16. 可否證實驗

選擇一組已形式化的基礎 theorem。

對每個 theorem 生成四組候選：

A：paraphrase / rename；
B：equivalent representation；
C：structural mutation；
D：branch / invalid mutation。

再要求系統完成：

四層分類；
formal relation 預測；
canonical duplicate detection；
branch detection；
counterexample generation；
proof verification。

評測：

\text{Acc}_{\mathrm{class}},

\text{Acc}_{\mathrm{relation}},

\text{Precision}_{\mathrm{dedup}},

\text{Recall}_{\mathrm{branch}},

\text{VerifiedRate}.

更重要的 downstream 實驗則比較：

D_{\mathrm{raw}}

與：

D_{\mathrm{structure-aware}}

在相同 token budget 下的推理與 theorem-proving 表現。

若結構感知去重與變種分類沒有任何收益，則本框架的工程價值會被削弱。

17. 研究邊界

本文不主張存在一個對所有數學與程式都完美有效的全域結構距離。

也不主張：

P\leftrightarrow Q

即可自動推出 P 與 Q 在教育、搜尋、證明策略、表示學習上完全冗餘。

此外，對自然語言哲學、法律、社會科學等高語義領域，「同一命題」本身可能缺乏穩定形式核心，因此本篇框架不能直接無條件移植。這些領域需要額外的語義保真層、底空間與判定域分析；本系列之後的橋接論文將另行處理。

18. 結論

AI-native knowledge expansion 的真正單位不應是：

\text{sample}.

而應是：

\boxed{ \text{verified structural node}. }

一個高品質節點必須知道：

它從哪裡來；
經過什麼變換；
保留什麼；
改變什麼；
與父節點是什麼形式關係；
是否與既有節點等價；
是否應建立新的 proposition identity；
如何被驗證。

因此：

\boxed{ \text{Generate More} \rightarrow \text{Generate Distinguishably More}. }

再進一步：

\boxed{ \text{Structural Diversity} = \text{Variation} - \text{Equivalence Redundancy} + \text{Verified Branching}. }

Paper I 的問題是：

基礎知識能不能被大量展開？

Paper II 的答案是：

可以，但如果沒有等價類、標準形、合法變換與命題分叉判定，「大量展開」很快就會退化為大量重複。

因此，BKSE 的第二個核心不是生成器，而是：

\boxed{ \text{Identity Management for Knowledge}. }

下一篇將處理第三個問題：

\boxed{ \text{How should errors and counterexamples be systematically generated?} }

亦即建立「錯誤鄰域與反例空間」：如何讓 AI 不只學會證明一個命題，也學會辨認與母命題距離極近、卻因一個條件、量詞、定義域或推導步驟而失敗的命題。

參考文獻

Lean Language Reference. Simp Sets; Rewrite Rules; Simplification vs Rewriting. Lean Project.

Leang, J. O. J., Hong, G., Li, W., & Cohen, S. B. (2025). Theorem Prover as a Judge for Synthetic Data Generation. arXiv:2502.13137.

Lai, J., Zhang, J., Xu, S., et al. (2025). LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation. arXiv:2505.12031.

Li, C., Ma, W., Wang, Z., & Wen, Z. (2025). SITA: A Framework for Structure-to-Instance Theorem Autoformalization. arXiv:2511.10356.

Lean Community. Mathlib: A Foundation for Formal Mathematics Research and Verification. Lean.