# 語義保真與命題身份守衛：從可驗證結構變種到判定域狀態語義的橋接 **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： ```text 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 再增加： ```text 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。 最小欄位： ```text 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： ```text SEMANTICALLY_ALIGNED SEMANTICALLY_DRIFTED DOMAIN_SHIFTED REFERENT_SHIFTED JUDGMENT_SHIFTED AMBIGUOUS UNAUDITED ``` --- # 16. 形式有效與語義對齊必須分開存 不能再只有： ```text verified = true ``` 建議： ```text formal_status = PROVED semantic_status = UNAUDITED ``` 或： ```text formal_status = PROVED semantic_status = DOMAIN_SHIFTED ``` 甚至： ```text 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 中新增服務： ```text 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 的橋接後版本 原本： ```text Candidate ↓ Parse ↓ Type ↓ Canonicalize ↓ Prove / Attack ↓ Commit ``` 橋接後： ```text 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}. \] 例如： ```text KANT-001-A KANT-001-B KANT-001-C ``` 都可以形式化。 但不能先偷偷 merge 成： ```text 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, \] 最好的系統行為可能是： ```text maintain both branches ``` 而不是： ```text average them ``` 或： ```text 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. 一個完整狀態範例 ```text 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, \] 不要一律丟掉。 可以存成： ```text 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 只保留： ```text natural language formal statement compile = PASS ``` 可能混入大量： \[ \text{compile-valid semantic drift}. \] 因此高品質 dataset 更接近： ```text 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 插件 新增： ```text anker/semantic/ ├── state.py ├── capture.py ├── compare.py ├── drift.py ├── certificate.py └── review.py ``` 最小 API： ```text 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}. \] 它只要求作者／文本／上下文提供足夠外顯標記，例如： ```text goal: base_space: object: definition: domain: judgment_rule: known_ambiguity: ``` 因此： \[ \boxed{ \text{Semantic State} } \] 是： \[ \text{declared / inferred working state}, \] 不是形而上的「真正思想讀取」。 --- # 43. Semantic State 的來源權重 可以記： ```text 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, \] 就標： ```text SEMANTIC_UNSTABLE ``` 而不是讓其中一個自動覆蓋另一個。 這將 AI 的「互相質疑」變成 semantic safety mechanism。 --- # 45. Human Semantic Review 的真正用途 Human review 不需要重做所有 proof。 只看： \[ \boxed{ \text{high semantic-friction nodes}. } \] 例如 scheduler 可以選： ```text 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 \] 個短命題， 每個明確提供： ```text 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 新增： ```json "semantic": { "intent": null, "base_space": null, "referent": null, "signifier": null, "signified": null, "signification": null, "judgment_domain": null, "history": [] } ``` 以及： ```json "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 若大量節點： ```text 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. 研究邊界 本文不主張： 1. 人類原始意圖可以被完全讀取； 2. \(\Psi\) 八個欄位足以描述所有語義； 3. 作者對自身思想的解釋永遠正確； 4. semantic equivalence 可以被一般演算法完全判定； 5. 多模型一致就代表真正語義一致； 6. formal proof 可以解決哲學詮釋； 7. Semantic Guard 可以取代專家； 8. 所有語義漂移都是錯誤； 9. high-semantic domains 都能使用同一 ontology； 10. 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. } \] 也就是： 1. 先知道原始語義身份； 2. 再建立形式命題； 3. 再證明； 4. 再驗證 proof； 5. 最後確認這條形式鏈仍然指向原本要處理的對象。 因此： \[ \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.