語義保真與命題身份守衛：從可驗證結構變種到判定域狀態語義的橋接

English Title: Semantic Preservation and Proposition Identity Guards: Bridging Verified Structural Variation with Base Spaces, Pre-Symbolic Referents, and Judgment Domains
Position: Bridge Paper — AI-Native Knowledge Expansion ↔ Domain-Transition Information Logic
Author: Neo.K
Collaborator: Aletheia (GPT-5.6 Sol)
Institution: EveMissLab / 一言諾科技有限公司
Version: v0.1
Date: 2026-08-10
Status: Series I → Series II Bridge

摘要

Series I 已建立一套相對完整的 AI 原生知識展開架構：命題可以被大量變種、去重、分叉、反駁、形式化、交叉驗證並存入 Research Graph。然而，只要研究對象從高度形式化的數學轉向自然語言、哲學、法律、概念科學或其他高語義領域，一個更前置的問題立即出現：

\boxed{ \text{How do we know the transformed statement is still about the same thing?} }

形式系統能驗證：

\Pi:F,

即 proof $\Pi$ 確實證明 formal statement (F)。但這並不自動證明：

I\equiv_{\mathrm{sem}}F,

其中 (I) 是原始意圖或非形式命題。Lean 官方目前也明確區分「theorem 是否具有 valid proof」與「theorem statement 到底意味著什麼」；形式 proof 的可信性仍依賴 formal statement 是否正確對應 intended informal meaning。

2026 年的 autoformalization 研究已直接量化這個問題：一個高等數學 benchmark 上，完整 tool-augmented agent 可達 89.5% compilation，但只有 60.5% consensus faithfulness，形成 29.0 個百分點的「compile-pass but semantically unfaithful」缺口。研究指出，可編譯的 Lean statement 仍可能遺漏假設、改變 domain 或表達 vacuous claim。

本文因此提出 Semantic Identity Guard（SIG） 與 Semantic Preservation Certificate（SPC），作為 Series I 與 Series II 的橋接層。對一個知識物件，不只保存其形式結構指紋：

\Phi(P),

還保存語義身份狀態：

\Psi(P) = ( \iota, \mathcal B, \rho, s, d, \sigma, J, H ),

其中分別表示前符號意圖壓力、概念底空間、被指、能指、所指、意指映射、判定域與歷史狀態。AI 生成變種 (P') 時，不再只問：

\Phi(P')\stackrel{?}{\sim}\Phi(P),

還必須問：

\Psi(P')\stackrel{?}{\sim}\Psi(P).

本文將語義漂移分成符號漂移、所指漂移、被指漂移、底空間漂移、判定域漂移、目標漂移與歷史狀態漂移，並提出一個可實作的語義守衛流程，使 ANKER Runtime 可以把 FORMALLY_VALID 與 SEMANTICALLY_ALIGNED 分別保存。

本文的核心命題是：

\boxed{ \text{Formal validity protects inference identity; semantic guards protect object identity.} }

Series I 解決「這個推導是否合法」；Series II 將進一步解決「我們現在判定、指涉與重新分類的，究竟還是不是原來那個對象」。

關鍵詞： Semantic Preservation；Semantic Identity Guard；命題身份；底空間；被指；能指；所指；意指；判定域；autoformalization；semantic drift；ANKER

1. 橋接問題：形式上是同一個，語義上真的是同一個嗎？

Series I 的 Paper II 定義命題結構指紋：

\Phi(P) = ( \mathcal D, \mathcal O, \mathcal Q, \mathcal A, \mathcal R, \mathcal C, \mathcal K ).

它適合處理：

domain；
object type；
quantifier；
assumption；
relation；
conclusion；
dependency kernel。

這在數學中非常有效。

但自然語言還可能有另一種失真。

兩句話：

P_1, P_2

形式結構非常接近：

\Phi(P_1)\approx\Phi(P_2),

卻可能根本不是在談同一個對象。

反過來：

\Phi(P_1)\neq\Phi(P_2)

也不必然代表兩者語義核心不同。

因此：

\boxed{ \text{structural identity} \neq \text{semantic identity}. }

2. 最危險的錯誤：正確地證明了錯的命題

假設人類原始命題：

[ I. ]

AI 將它形式化：

[ F. ]

Lean 找到：

\Pi:F.

Kernel 驗證：

K(\Pi,F)=PASS.

這最多表示：

\boxed{ F\text{ 在該形式系統中具有一條有效 proof。} }

它沒有自動證明：

\boxed{ I\equiv_{\mathrm{sem}}F. }

這就是：

\boxed{ \text{correct proof of the wrong formalization}. }

對 autonomous mathematics 而言，這可能比 proof failure 更危險。

因為 proof failure 會報錯。

語義漂移卻可能：

[ PASS. ]

3. Lean 自己已經把這條邊界說得很清楚

Lean 官方 proof-validation guidance 現在直接區分：

\text{“does the theorem have a valid proof?”}

與：

\text{“what does the theorem statement mean?”}.

日常 kernel acceptance 的信任前提之一，就是使用者相信 formal theorem statement 對應 intended informal meaning。

因此：

\boxed{ \text{Kernel} }

並不是 semantic-intent checker。

這不是 Lean 的缺陷。

而是形式驗證本來就有的職責邊界。

4. Autoformalization 已經量出這個 Gap

2026 年的 Beyond Compilation 專門研究 natural-language-to-Lean statement formalization。

其核心警告是：

compilation 只能確認 Lean declaration 形式有效；它仍可能省略 hypotheses、改變 domains，或產生語義上空洞的 statement。

該工作在 400 個 graduate-level entries 上報告：

[ 89.5% ]

compile rate，

但只有：

[ 60.5% ]

consensus faithfulness，

兩者相差：

[ 29.0 ]

個百分點。

因此：

\boxed{ \text{Compile Success} \not\Rightarrow \text{Semantic Preservation}. }

這不是純哲學問題。

它已經是一個可測量的 AI formalization failure mode。

5. 一個極簡例子：Domain 偷換

原始自然語言：

對所有實數 (x)， $x^2\ge0$ 。

預期形式：

\forall x\in\mathbb R,\quad x^2\ge0.

但一個錯誤 formalizer 可能輸出：

\forall x\in\mathbb N,\quad x^2\ge0.

後者：

可以形式化；
可以證明；
甚至更容易證明。

但：

\boxed{ \mathbb R\rightarrow\mathbb N }

已經改變原命題的 domain。

所以：

\text{PROVED}

仍然不代表：

\text{FAITHFUL}.

6. Series I 的 Fingerprint 還不夠

Paper II 的：

\Phi(P)

可以發現很多 domain、quantifier、assumption shift。

但到了哲學與高階自然語言，問題比這更早發生。

因為：

\text{formal proposition}

可能尚未形成以前，

主體就已經：

選了不同底空間；
切出了不同被指；
用同一能指壓縮了不同對象；
站在不同判定域；
想回答不同問題。

所以需要比：

\Phi

更前置的：

\boxed{ \Psi. }

7. 語義身份狀態

本文暫定：

\boxed{ \Psi(P,t) = ( \iota_t, \mathcal B_t, \rho_t, s_t, d_t, \sigma_t, J_t, H_t ) }

其中：

$\iota_t$ ：Pre-Symbolic Intent Pressure

尚未完全形成符號之前，主體正在嘗試捕捉什麼問題、差異或結構。

$\mathcal B_t$ ：Base Space

什麼對象、規則、分類與關係在這次討論裡被允許成立的底層空間。

$\rho_t$ ：Pre-Symbolic Referent / 被指

尚未穩定成所指之前，已具可切分性與可定義性的抽象被指。

$s_t$ ：Signifier / 能指

可見的詞、符號、公式、程式名稱或其他表示形式。

$d_t$ ：Signified / 所指

目前被穩定化、可由符號承載的概念或對象。

$\sigma_t$ ：Signification / 意指

s_t\rightarrow d_t

的映射關係。

$J_t$ ：Judgment Domain / 判定域

當前用來判定「是／不是／等價／不同／合法／非法」的分類域。

$H_t$ ：History

此前經歷過的身份、判定與轉態歷史。

8. 為什麼需要 $\rho$ 而不只需要 (d)？

傳統能指—所指模型通常從：

s\rightarrow d

開始。

但高階概念生成中，可能先存在：

\rho

也就是：

我知道我正在抓一個東西，但還沒有完全決定它該怎麼被命名、定義與封裝。

因此：

\boxed{ \rho\neq d. }

可以暫時寫成：

\rho \rightarrow \text{definition compression} \rightarrow d \rightarrow s.

這一層對 AI-human collaborative theorizing 尤其重要。

因為很多語義錯位不是在「同一詞有多義」時才發生。

而是在：

\boxed{ \text{符號形成之前就已經切出了不同對象。} }

9. 同一能指，不同所指

若：

s_1=s_2,

不能推出：

d_1=d_2.

例如雙方都說：

\text{“自由”}.

一方可能指：

d_1=\text{免於外在干預},

另一方：

d_2=\text{實現自身能力}.

所以：

\boxed{ s_1=s_2 \land d_1\neq d_2. }

若 AI 只看 lexical identity：

\text{same token} \Rightarrow \text{same concept},

就會錯誤合併。

10. 更深一層：同一能指、不同被指

甚至：

d_1,d_2

還沒有真正穩定之前，

兩個主體已經從不同底空間：

\mathcal B_1,\mathcal B_2

切出：

\rho_1\neq\rho_2.

之後卻都壓成同一符號：

[ s. ]

流程：

\boxed{ \rho_1\neq\rho_2 \rightarrow s_1=s_2 \rightarrow \text{apparent agreement} \rightarrow \text{later conflict}. }

這就是語義守衛必須比 keyword alignment 更早工作的原因。

11. 不同能指，也可能是同一被指

反過來：

s_1\neq s_2

也不必然：

\rho_1\neq\rho_2.

兩個人可能使用不同語言、術語或符號，

但實際捕捉到：

\rho_1\approx\rho_2.

因此：

\boxed{ \text{surface mismatch} \not\Rightarrow \text{semantic mismatch}. }

這也是為什麼純 embedding / string distance 不能獨自充當 semantic identity checker。

12. Semantic Identity Signature

定義：

\boxed{ \Psi(P) = ( \iota, \mathcal B, \rho, s, d, \sigma, J, H ). }

它不是說人類思想真的可以被八個欄位完整捕捉。

而是一個工程上的：

\boxed{ \text{semantic state interface}. }

目的是讓 AI 至少知道：

哪些語義層可能被改變了？

而不是把所有變化壓成：

\text{sentence changed}.

13. Semantic Preservation 不是要求所有欄位不變

這非常重要。

假設做：

T_{\mathrm{translate}}

中英翻譯。

那麼：

[ s ]

一定會改。

但：

\rho,d,J

應盡量保持。

所以對 transformation (T)，定義：

\boxed{ M_T = \text{allowed semantic-change mask}. }

例如 translation：

signifier: allowed_to_change
signified: preserve
referent: preserve
base_space: preserve
judgment_domain: preserve
history: extend

因此語義保真不是：

\Psi(P)=\Psi(P').

而是：

\boxed{ \operatorname{Preserve}_{M_T} ( \Psi(P), \Psi(P') ). }

14. Formal Variation Certificate 需要升級

Paper II 的 Variation Certificate 記：

parent；
operator；
fingerprint；
changed dimensions；
formal relation。

Bridge Layer 再增加：

semantic_source
semantic_target
base_space_relation
referent_relation
signified_relation
judgment_domain_relation
goal_relation
history_relation
semantic_preservation_status

於是同一個 variation 同時具有：

\boxed{ \Phi\text{-certificate} + \Psi\text{-certificate}. }

15. Semantic Preservation Certificate

本文提出：

\boxed{ SPC(P,P',T) }

即 Semantic Preservation Certificate。

最小欄位：

source_id
target_id
transformation
source_base_space
target_base_space
referent_relation
signified_relation
judgment_domain_relation
preserved_constraints
changed_constraints
known_ambiguities
evidence
review_status

Status：

SEMANTICALLY_ALIGNED
SEMANTICALLY_DRIFTED
DOMAIN_SHIFTED
REFERENT_SHIFTED
JUDGMENT_SHIFTED
AMBIGUOUS
UNAUDITED

16. 形式有效與語義對齊必須分開存

不能再只有：

verified = true

建議：

formal_status = PROVED
semantic_status = UNAUDITED

或：

formal_status = PROVED
semantic_status = DOMAIN_SHIFTED

甚至：

formal_status = UNKNOWN
semantic_status = ALIGNED

三者都是合理狀態。

因此：

\boxed{ \text{formal epistemic state} \neq \text{semantic identity state}. }

17. 七類語義漂移

本文先建立七類。

17.1 Signifier Drift

\Delta s\neq0.

單純換詞、翻譯、符號。

未必有問題。

17.2 Signified Drift

\Delta d\neq0.

同一詞逐漸改變概念邊界。

例如 definition creep。

17.3 Referent Drift

\Delta\rho\neq0.

更前置地換了真正想捕捉的抽象對象。

17.4 Base-Space Drift

\Delta\mathcal B\neq0.

允許的對象、規則或分類空間改變。

17.5 Judgment-Domain Drift

\Delta J\neq0.

「是／不是」判定標準改了。

17.6 Goal Drift

原本問：

Q_1

後來實際回答：

Q_2.

這是非常常見的 AI answer drift。

17.7 Historical-State Drift

當前輸出相同：

Y_t=Y_{t+2},

但：

H_t\neq H_{t+2}.

因此「又是」不應被壓成普通「是」。

這一類將由 Series II 正式展開。

18. Semantic Drift Vector

可以定義：

\boxed{ \Delta_\Psi = ( \delta_\iota, \delta_{\mathcal B}, \delta_\rho, \delta_s, \delta_d, \delta_\sigma, \delta_J, \delta_H ). }

但本文不主張立刻把每一項壓成單一 scalar。

因為：

\delta_\rho

和：

\delta_s

不具有同樣重要性。

翻譯造成：

\delta_s\gg0

可能完全安全。

但：

\delta_\rho\gg0

即使文字只改一個字，也可能代表命題已經變了。

19. Semantic Distance 不應只有一個分數

可以保留向量：

\boxed{ \mathbf F_S(P,P') = ( f_{\mathrm{pre}}, f_{\mathrm{sym}}, f_{\mathrm{base}}, f_{\mathrm{ref}}, f_{\mathrm{signified}}, f_{\mathrm{judgment}}, f_{\mathrm{goal}}, f_{\mathrm{history}} ). }

這比：

sim(P,P')=0.83

更有診斷價值。

因為使用者需要知道：

到底是哪一層不同？

20. ASSESS 類工作提供了一個外部近鄰

2025 年的 ASSESS 已經指出，autoformalization statement evaluation 中，純字串／結構 similarity 無法捕捉完整語義，而 proof-based equivalence 雖能檢查 provability，卻又不能表達 structural likeness 的連續程度；因此該工作同時建模 semantic 與 structural similarity，並建立 524 對 expert-annotated formal statements 的 EPLA benchmark。

這與本文有明顯交集。

但本文的重點更偏：

\boxed{ \text{semantic identity state across a transformation history} }

而不是只比較兩個 formal statements 的 likeness。

21. Faithfulness 比 Compilation 更接近真正目標

2026 年另一項 Faithful Autoformalization of Natural Language Assertions 工作，也把問題明確寫成：

\text{natural-language developer intent} \rightarrow \text{formal executable assertion},

並針對 ambiguity 與 validity 建立 conformance-based filtering；其實驗顯示，單純 naive LLM translation 並不足以可靠保留原始規格意圖。

所以：

\boxed{ \text{faithfulness} }

正逐漸成為 autoformalization 的獨立研究目標。

22. 但 Bridge Paper 還多做了一步

外部 autoformalization 工作大多假設：

[ I ]

已經是一句相對確定的 natural-language assertion。

本文則再往前追問：

\boxed{ I\text{ 自己是怎麼形成的？} }

也就是：

\iota \rightarrow \mathcal B \rightarrow \rho \rightarrow d \rightarrow s.

這對純數學題可能不重要。

但對：

哲學；
新理論命名；
跨領域類比；
AI-human co-creation；
模糊概念 formalization；

就非常重要。

23. Semantic Identity Guard

在 ANKER 中新增服務：

SemanticGuard.capture_source(node)
SemanticGuard.compare(source, target)
SemanticGuard.detect_drift(source, target)
SemanticGuard.issue_certificate(source, target)
SemanticGuard.require_review(node)

它不負責證明 theorem。

它負責：

\boxed{ \text{protect the identity of what is being proved}. }

24. ANKER Pipeline 的橋接後版本

原本：

Candidate
↓
Parse
↓
Type
↓
Canonicalize
↓
Prove / Attack
↓
Commit

橋接後：

Intent / Source Claim
↓
Semantic Capture
↓
Formal Candidate
↓
Structural Identity Check
↓
Formal Verification
↓
Semantic Identity Guard
↓
Literature / External Audit
↓
Canonical Commit

因此：

\boxed{ \text{formal verification} }

被包在更大的：

\boxed{ \text{knowledge admission pipeline} }

裡。

25. Semantic Guard 不一定每次都昂貴

數學領域中：

\mathcal B,\rho,J

常常已經相對穩定。

例如一個 Mathlib theorem 的同型 rewrite，

可以使用：

\text{fast semantic lane}.

但若偵測到：

domain change；
definition change；
translation；
philosophy text；
new concept；
cross-domain analogy；

則提升：

\text{deep semantic lane}.

所以：

\boxed{ \text{semantic verification rigor is domain-sensitive}. }

26. 三級 Semantic Lane

S-Bronze

檢查：

domain；
quantifier；
named entities；
explicit assumptions。

S-Silver

加入：

concept definition diff；
object relation；
goal alignment；
source-target paraphrase audit。

S-Gold

加入：

base-space declaration；
pre-symbolic referent note；
judgment domain；
multi-agent semantic comparison；
human author review。

高語義理論建議：

S\text{-Gold}.

27. 作者仍然可能是最高權重語義來源

如果原始概念作者仍在場，

對：

\rho,\iota,\mathcal B

的判斷，

作者通常具有很高資訊權重。

但：

\boxed{ \text{authorial intent} \neq \text{logical correctness}. }

作者可以最了解：

我原本想說什麼。

卻不一定能保證：

我說的東西是對的。

所以：

\text{Semantic Authority}

與：

\text{Logical Authority}

仍然分開。

28. 這正好解決哲學重構的一個難點

哲學重構如果只做：

\text{Natural Language} \rightarrow \text{Formal Logic},

很容易在形式化途中：

\boxed{ \text{formalize the interpreter instead of the philosopher}. }

因此需要保存：

\text{source interpretation branch}.

例如：

KANT-001-A
KANT-001-B
KANT-001-C

都可以形式化。

但不能先偷偷 merge 成：

KANT-001

除非語義身份真的被證明足夠接近。

29. Competing Interpretation Branches

因此高語義圖允許：

\operatorname{ForkSemantic}(P).

例如：

\Psi_A, \Psi_B, \Psi_C.

每一支都有自己的：

base space；
referent；
definition；
judgment domain。

後續可以比較：

\Delta_\Psi(A,B).

這比：

A 學派和 B 學派都在討論同一句話。

更精確。

30. 不要過早追求「唯一正確解讀」

Semantic Guard 的目的不是：

\operatorname{ForceOneMeaning}.

而是：

\boxed{ \operatorname{MakeDifferencesExplicit}. }

如果：

\Psi_A\neq\Psi_B,

最好的系統行為可能是：

maintain both branches

而不是：

average them

或：

choose one silently

31. 判定域必須是一級物件

設：

[ J ]

為判定域。

一個命題：

X=Y

可能在：

J_1

成立，

在：

J_2

不成立。

所以完整形式應是：

\boxed{ X=_{J_1}Y }

而：

X\neq_{J_2}Y.

這不是矛盾。

因為判定函數不同。

32. 「是又不是」在這裡第一次有正式接口

Bridge Paper 不完整展開 Series II，

但可以先留接口。

若：

J_0(X)=Y

後來：

J_1(X)=N,

則不是靜態：

B=(1,1).

而是有向轉態：

Y\rightarrow N.

若系統保留：

H=(Y,N),

則：

\boxed{ \text{current state} + \text{historical state} }

共同構成資訊。

因此：

\text{“又”}

需要：

[ H. ]

這就是 Series II 將正式展開的歷史信息算子。

33. Semantic Admission Rule

ANKER 的 canonical admission 從：

\operatorname{Admit}(K)

升級成：

\boxed{ \operatorname{Admit}(K) = F(K)\land S(K) }

但不是要求：

F=S=1

才能保存。

更實際是保存多軸：

\operatorname{State}(K) = ( F, S, L, V ).

其中：

(F)：formal status；
(S)：semantic status；
(L)：literature status；
(V)：verification coverage。

34. 一個完整狀態範例

CLAIM-221

formal:
  status = PROVED_FORMAL
  checker = Lean

semantic:
  status = DOMAIN_SHIFTED
  source_domain = Real
  target_domain = Nat

literature:
  status = UNCHECKED

proof:
  families = 1

canonical:
  admission = REJECT_AS_FAITHFUL_TRANSLATION
  preserve_as = SEMANTIC_DRIFT_EXAMPLE

注意：

\text{formal proof}

沒有被刪掉。

它只是不能再被叫做：

\text{faithful formalization of source}.

35. Semantic Drift 本身也是資料

這非常重要。

如果 AI formalization 產生：

[ F' ]

而：

\Delta_\Psi\neq0,

不要一律丟掉。

可以存成：

SEMANTIC_DRIFT_EXAMPLE

並標：

drift type；
smallest drift；
why it passed formal checks；
repair。

這會形成：

\boxed{ \text{semantic error neighborhood}. }

它正是 Paper III 的高語義版本。

36. Minimal Semantic Failure Delta

與 Paper III 對應，

定義：

\boxed{ \Delta_\Psi^\ast = \arg\min_{\Delta_\Psi} \|\Delta_\Psi\| }

subject to：

\operatorname{Preserve}_{M_T} ( \Psi, \Psi+\Delta_\Psi )=0.

即：

最小改變哪一層語義，就足以讓它不再是同一個命題？

這可能是：

一個 domain；
一個量詞；
一個 referent；
一個 judgment criterion；
一個 goal。

37. Minimal Semantic Repair

反方向：

\boxed{ R_\Psi^\ast = \arg\min_R\|R\| }

使：

\operatorname{Preserve} ( \Psi_{\mathrm{source}}, R(\Psi_{\mathrm{target}}) )=1.

例如修回：

\mathbb N \rightarrow \mathbb R.

或者補回：

x\neq0.

或者明確把：

\text{自由}_A

改名：

\text{自由-免干預}.

38. 對 AI Dataset 的意義

如果大量 autoformalization dataset 只保留：

natural language
formal statement
compile = PASS

可能混入大量：

\text{compile-valid semantic drift}.

因此高品質 dataset 更接近：

source
target
compile_status
proof_status
semantic_alignment
drift_type
domain_diff
assumption_diff
review

這能降低：

\boxed{ \text{formally clean but semantically wrong training signal}. }

39. Series I 的 Effective Structural Dataset Size 也要升級

原本：

[ E(D). ]

Bridge 後可以定義：

\boxed{ E_S(D) = \sum_i w_i C_i V_i R_i S_i }

其中：

S_i

表示 semantic-preservation quality。

因此：

\text{大量形式有效資料}

若：

S_i\approx0,

不應被當成同等高品質資料。

40. Semantic Coverage

也可以定義：

C_{\mathrm{sem}}

不是看有多少 paraphrases，

而是：

一個概念的哪些 base-space、referent、domain、judgment 邊界已經被明確測試？

例如一個概念：

[ X ]

已測：

正例；
反例；
邊界；
domain shift；
translation；
cross-context use。

則：

C_{\mathrm{sem}}(X)

較高。

41. Bridge Paper 的核心 Runtime 插件

新增：

anker/semantic/
├── state.py
├── capture.py
├── compare.py
├── drift.py
├── certificate.py
└── review.py

最小 API：

capture_semantic_state(source)
compare_semantic_state(source, target)
classify_semantic_drift(diff)
issue_spc(source, target, transform)

42. MVP 不需要先讀心

這點要非常清楚。

\Psi

不是要求 AI 真正直接讀取：

\text{human mind}.

它只要求作者／文本／上下文提供足夠外顯標記，例如：

goal:
base_space:
object:
definition:
domain:
judgment_rule:
known_ambiguity:

因此：

\boxed{ \text{Semantic State} }

是：

\text{declared / inferred working state},

不是形而上的「真正思想讀取」。

43. Semantic State 的來源權重

可以記：

source = author_explicit
source = source_text
source = expert_interpretation
source = model_inference

並分權重。

例如：

w_{\mathrm{author\ explicit}} > w_{\mathrm{model\ inference}}

通常合理，

但仍不是絕對真值排序。

44. 多 Agent Semantic Audit

可以讓兩個 AI 獨立抽取：

\Psi_A, \Psi_B.

如果：

\Delta_\Psi(A,B)\gg0,

就標：

SEMANTIC_UNSTABLE

而不是讓其中一個自動覆蓋另一個。

這將 AI 的「互相質疑」變成 semantic safety mechanism。

45. Human Semantic Review 的真正用途

Human review 不需要重做所有 proof。

只看：

\boxed{ \text{high semantic-friction nodes}. }

例如 scheduler 可以選：

formal = PROVED
semantic_disagreement = HIGH
impact = HIGH

優先給作者／專家確認。

這就是：

\boxed{ \text{human attention as scarce semantic oracle}. }

46. 最小實驗一：Autoformalization Faithfulness

選：

[ 200 ]

個自然語言 theorem。

每個生成：

[ 5 ]

個 formalization candidates。

形成：

[ 1000 ]

對。

比較：

Baseline

只用：

compile；
proof attempt。

SIG

增加：

domain diff；
quantifier diff；
assumption diff；
semantic state comparison；
cross-model audit。

測：

\text{Semantic Drift Detection Precision},

\text{Semantic Drift Recall},

\text{Faithful Admission Rate}.

47. 最小實驗二：哲學短命題

不要一開始用整本康德。

選：

[ 50 ]

個短命題，

每個明確提供：

author intent note
base space
working definition
judgment domain

讓 AI 生成：

paraphrase；
formal skeleton；
counterexample；
translation。

測：

\text{same-object preservation}.

這比直接測「AI 能不能形式化哲學」乾淨。

48. 最小實驗三：「又」的歷史資訊

Seed：

[ Y. ]

建立：

H_1=(Y),

H_2=(Y,N,Y).

要求系統辨識：

\operatorname{Current}(H_1) = \operatorname{Current}(H_2) = Y,

但：

\boxed{ H_1\neq H_2. }

這是 Series II 最簡單的 state-history interface test。

49. 與 DBQ4 的接口

DBQ4 已區分：

\text{evidence changed}

與：

\text{world/process itself changed}.

Bridge Layer 再增加：

\text{judgment domain changed},

\text{referent changed},

\text{formalization changed}.

所以未來完整 transition 可以是：

\boxed{ \Sigma_t = ( \Psi_t, E_t, \nu_t ). }

其中：

$\Psi_t$ ：semantic identity state；
$E_t$ ：evidence state；
$\nu_t$ ：Q4 projection。

這就是 Series II 的主要入口。

50. 不是所有 Semantic Drift 都是錯

如果 transformation 本來就是：

T_{\mathrm{generalize}},

那麼：

\Delta\mathcal B\neq0

可能是預期的。

關鍵不是：

\Delta_\Psi=0.

而是：

\boxed{ \Delta_\Psi \subseteq \operatorname{AllowedSemanticChange}(T). }

因此：

drift

和：

illegal drift

必須分開。

51. Semantic Branching

若改變超出 allowed mask，

不要直接 reject。

可以：

\boxed{ \operatorname{SemanticBranch}(P,P'). }

表示：

它已經不是原命題的保真變種，但可能是一個合法的新命題。

這與 Paper II 的 proposition branching 完全對稱。

52. 形式分叉與語義分叉可以不同步

可能：

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

但：

\Psi(P)\neq\Psi(P').

這是：

\boxed{ \text{hidden semantic branch}. }

也可能：

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

但：

\Psi(P)\approx\Psi(P').

這是：

\boxed{ \text{representational/formal branch with semantic preservation}. }

這兩種情況都不能只靠形式 fingerprint 解決。

53. Identity Matrix

可以建立：

\boxed{ M_I(P,P') = \begin{pmatrix} I_{\mathrm{formal}} & I_{\mathrm{semantic}}\\ D_{\mathrm{formal}} & D_{\mathrm{semantic}} \end{pmatrix} }

更簡單地分類四象限：

A

F=same,\quad S=same.

真正同義變種。

B

F=different,\quad S=same.

不同形式，同一語義核心。

C

F=same,\quad S=different.

最危險：形式看起來一樣，但實際換對象。

D

F=different,\quad S=different.

明確新命題。

54. 最危險的是 C 象限

即：

\boxed{ \Phi(P)\approx\Phi(P') \land \Psi(P)\not\approx\Psi(P'). }

例如：

同一術語；
同一公式骨架；
同一 predicate 名稱；

但：

domain 變了；
referent 變了；
judgment rule 變了；
goal 變了。

這就是 Semantic Identity Guard 最主要要抓的錯誤。

55. Bridge Paper 對 ANKER 的最小修改

ANKER Knowledge Object 新增：

"semantic": {
  "intent": null,
  "base_space": null,
  "referent": null,
  "signifier": null,
  "signified": null,
  "signification": null,
  "judgment_domain": null,
  "history": []
}

以及：

"semantic_verification": {
  "status": "UNAUDITED",
  "certificate": null
}

數學 seed 可以大多留空或自動推定。

高語義節點則要求填入。

56. Scheduler 也要看 Semantic Risk

Paper VI：

S_F(q).

Bridge 後加：

R_S(q) = \text{semantic drift risk}.

如果：

R_S\gg0

且：

Impact\gg0,

則優先：

\text{semantic audit}.

所以：

\boxed{ \text{semantic uncertainty itself becomes a frontier action}. }

57. Semantic Debt

若大量節點：

formal = PROVED
semantic = UNAUDITED

系統累積：

\boxed{ D_S=\text{Semantic Debt}. }

如果 downstream nodes 持續依賴這些節點，

風險會放大。

因此可以定義：

D_S(G) = \sum_{K} w(K) \mathbf 1[ semantic(K)=UNAUDITED ].

高 impact 未審核節點優先清償。

58. 這也是「沙丘上的城堡」問題的另一版本

如果：

F_1

語義已偏離原意，

後面：

F_1\Rightarrow F_2\Rightarrow F_3\Rightarrow\cdots

每一步都形式正確，

整棟系統仍可能：

\boxed{ \text{internally valid but externally misaligned}. }

因此形式化不只是「把城堡蓋牢」。

還要確認：

\boxed{ \text{城堡是不是蓋在你原本想蓋的那塊地上。} }

59. Series I 與 Series II 的正式分工

到這裡可以很清楚分：

Series I

問：

\boxed{ \text{How can knowledge structures be generated and verified?} }

主要處理：

structure；
proof；
counterexample；
graph；
scheduling。

Series II

問：

\boxed{ \text{How does the identity and judgment state of an object change across domains and history?} }

主要處理：

base space；
pre-symbolic referent；
signification；
judgment domain；
state transition；
“again”；
是又不是／不是又是。

Bridge Paper 的工作：

\boxed{ \text{protect the handoff}. }

60. 最終橋接公式

Series I 主要維持：

\Phi_t.

Series II 主要維持：

\Psi_t.

完整知識節點：

\boxed{ K_t = ( \Phi_t, \Psi_t, E_t, \nu_t, H_t ). }

其中：

$\Phi_t$ ：形式／結構身份；
$\Psi_t$ ：語義身份；
$E_t$ ：證據狀態；
$\nu_t$ ：當前 Q4 判定；
$H_t$ ：歷史轉態。

這已經足夠支撐下一系列。

61. 研究邊界

本文不主張：

人類原始意圖可以被完全讀取；
$\Psi$ 八個欄位足以描述所有語義；
作者對自身思想的解釋永遠正確；
semantic equivalence 可以被一般演算法完全判定；
多模型一致就代表真正語義一致；
formal proof 可以解決哲學詮釋；
Semantic Guard 可以取代專家；
所有語義漂移都是錯誤；
high-semantic domains 都能使用同一 ontology；
Series II 已經在本篇被完整形式化。

本文只提出：

\boxed{ \text{semantic identity must be represented separately from formal validity}. }

62. 外部學術定位

本文與近年的 faithful autoformalization、statement-similarity evaluation 有直接鄰近關係。

ASSESS 將 formal-statement evaluation 拆成 semantic 與 structural similarity，並建立 EPLA benchmark 來同時標註 provability 與 structural likeness。

Beyond Compilation 則直接證明 compile success 與 semantic faithfulness 存在顯著缺口，並提出 compilation、semantic judging 與 human calibration 的分離評測。

Faithful Autoformalization of Natural Language Assertions 也把 informal intent 與 formal assertion 之間的 conformance 當成獨立問題處理。

因此本文不宣稱：

\text{semantic faithfulness in autoformalization}

是新的研究問題。

本文的差異較窄：

\boxed{ \text{semantic faithfulness as a persistent state-and-lineage layer inside AI-native knowledge expansion}. }

並將其接到：

\text{base space} + \text{pre-symbolic referent} + \text{judgment domain} + \text{historical transition}.

63. 結論：不要只保護 Proof，也要保護「被證明的那個東西」

Series I 已經可以讓 AI：

生成；
去重；
分叉；
找反例；
證明；
交叉驗證；
保存研究圖；
排程下一步。

但這些能力仍然可能發生一種最高階錯誤：

\boxed{ \text{the machine proves something perfectly that nobody originally meant}. }

因此 Bridge Layer 加入：

\boxed{ \text{Semantic Identity Guard}. }

完整研究鏈從：

I \rightarrow F \rightarrow \Pi \rightarrow K

升級為：

\boxed{ \Psi_I \rightarrow \Phi_F \rightarrow \Pi \rightarrow K \rightarrow SPC. }

也就是：

先知道原始語義身份；
再建立形式命題；
再證明；
再驗證 proof；
最後確認這條形式鏈仍然指向原本要處理的對象。

因此：

\boxed{ \text{Formal validity protects inference.} }

而：

\boxed{ \text{Semantic preservation protects identity.} }

這就是 Series I 與 Series II 的真正接縫。

下一篇正式進入 Series II / Paper I，處理：

\boxed{ \text{Judgment-Domain Transition and Historical Information State}. }

也就是從「見 (X) 是 (X) → 見 (X) 不是 (X) → 見 (X) 又是 (X)」開始，把「是又不是／不是又是」從自然語言直覺正式拆成：

\text{判定域} + \text{局部四態} + \text{有向轉態} + \text{歷史保留}

的動態信息邏輯。

參考文獻

Lean Project. Validating a Lean Proof. Lean Language Reference, 2026.

Liu, X., Zhu, T., Dong, Z., et al. (2025). ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity. arXiv:2509.22246.

Zhang, K., Gallardo Candela, P., Murthy, S., et al. (2026). Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization. arXiv:2606.31002.

Liu, H., Parthasarathy, M., & Murali, A. (2026). Faithful Autoformalization of Natural Language Assertions. arXiv:2607.13303.

Xie, J., Liu, C., Yuan, Y., et al. (2025). FMC: Formalization of Natural Language Mathematical Competition Problems. arXiv:2507.11275.

語義保真與命題身份守衛：從可驗證結構變種到判定域狀態語義的橋接

語義保真與命題身份守衛：從可驗證結構變種到判定域狀態語義的橋接

摘要

1. 橋接問題：形式上是同一個，語義上真的是同一個嗎？

2. 最危險的錯誤：正確地證明了錯的命題

3. Lean 自己已經把這條邊界說得很清楚

4. Autoformalization 已經量出這個 Gap

5. 一個極簡例子：Domain 偷換

6. Series I 的 Fingerprint 還不夠

7. 語義身份狀態

ιt\iota_tιt​：Pre-Symbolic Intent Pressure

Bt\mathcal B_tBt​：Base Space

ρt\rho_tρt​：Pre-Symbolic Referent / 被指

sts_tst​：Signifier / 能指

dtd_tdt​：Signified / 所指

σt\sigma_tσt​：Signification / 意指

JtJ_tJt​：Judgment Domain / 判定域

HtH_tHt​：History

8. 為什麼需要 ρ\rhoρ 而不只需要 (d)？

9. 同一能指，不同所指

10. 更深一層：同一能指、不同被指

11. 不同能指，也可能是同一被指

12. Semantic Identity Signature

13. Semantic Preservation 不是要求所有欄位不變

14. Formal Variation Certificate 需要升級

15. Semantic Preservation Certificate

16. 形式有效與語義對齊必須分開存

17. 七類語義漂移

17.1 Signifier Drift

17.2 Signified Drift

17.3 Referent Drift

17.4 Base-Space Drift

17.5 Judgment-Domain Drift

17.6 Goal Drift

17.7 Historical-State Drift

18. Semantic Drift Vector

19. Semantic Distance 不應只有一個分數

20. ASSESS 類工作提供了一個外部近鄰

21. Faithfulness 比 Compilation 更接近真正目標

22. 但 Bridge Paper 還多做了一步

23. Semantic Identity Guard

24. ANKER Pipeline 的橋接後版本

25. Semantic Guard 不一定每次都昂貴

26. 三級 Semantic Lane

S-Bronze

S-Silver

S-Gold

27. 作者仍然可能是最高權重語義來源

28. 這正好解決哲學重構的一個難點

29. Competing Interpretation Branches

30. 不要過早追求「唯一正確解讀」

31. 判定域必須是一級物件

32. 「是又不是」在這裡第一次有正式接口

33. Semantic Admission Rule

34. 一個完整狀態範例

35. Semantic Drift 本身也是資料

36. Minimal Semantic Failure Delta

37. Minimal Semantic Repair

38. 對 AI Dataset 的意義

39. Series I 的 Effective Structural Dataset Size 也要升級

40. Semantic Coverage

41. Bridge Paper 的核心 Runtime 插件

42. MVP 不需要先讀心

43. Semantic State 的來源權重

44. 多 Agent Semantic Audit

45. Human Semantic Review 的真正用途

46. 最小實驗一：Autoformalization Faithfulness

Baseline

SIG

47. 最小實驗二：哲學短命題

48. 最小實驗三：「又」的歷史資訊

49. 與 DBQ4 的接口

50. 不是所有 Semantic Drift 都是錯

51. Semantic Branching

52. 形式分叉與語義分叉可以不同步

53. Identity Matrix

A

B

C

D

$\iota_t$ ：Pre-Symbolic Intent Pressure

$\mathcal B_t$ ：Base Space

$\rho_t$ ：Pre-Symbolic Referent / 被指

$s_t$ ：Signifier / 能指

$d_t$ ：Signified / 所指

$\sigma_t$ ：Signification / 意指

$J_t$ ：Judgment Domain / 判定域

$H_t$ ：History

8. 為什麼需要 $\rho$ 而不只需要 (d)？