title: "跨世界符號橋的多層架構：AI-native、形式驗證、專家理解與人類可讀層" english_title: "A Multi-Layer Architecture for Cross-World Symbolic Bridges: AI-Native, Formal Verification, Expert, and Human-Readable Layers" author: "Neo.K（許筌崴）" institution: "EveMissLab（一言諾科技有限公司）" series: "異質智慧動態協議生成系列" paper_no: "06" version: "v0.1" date: "2026-08-14" status: "正式研究草稿" canonical_source_encoding: "UTF-8"

跨世界符號橋的多層架構：AI-native、形式驗證、專家理解與人類可讀層

A Multi-Layer Architecture for Cross-World Symbolic Bridges: AI-Native, Formal Verification, Expert, and Human-Readable Layers

作者：Neo.K（許筌崴）
機構：EveMissLab（一言諾科技有限公司）
系列：異質智慧動態協議生成系列，第 6 篇
版本：v0.1
日期：2026 年 8 月 14 日

摘要

若未來人工智慧在數學、程式設計、物理學與科學發現中逐步形成高度壓縮、機器原生、甚至人類無法直接閱讀的工作表示，一個極端答案是：人類只保留意圖與最終接受／拒絕權，中間推理、形式化與操作世界全部交給 AI 黑箱。本文主張這不是唯一可能的架構，也不是一個理想的預設。

本文不要求 AI-native 表示退化成人類自然語言，而提出四層跨世界符號橋：

\boxed{ L_A \leftrightarrow L_F \leftrightarrow L_E \leftrightarrow L_H }

其中：

$L_A$ ：AI-native / machine-operational layer；
$L_F$ ：formal / verifiable shared layer；
$L_E$ ：expert-facing semantic layer；
$L_H$ ：general human-readable layer。

此架構的核心不是「每層翻譯成相同內容」，而是每一層有不同責任： $L_A$ 優先效率與可執行； $L_F$ 優先可驗證規格、證書與語義約束； $L_E$ 優先專家能重建理論結構、假設、證據與失敗條件； $L_H$ 優先讓非專家理解目的、風險、不確定性與可採取行動。各層之間使用任務充分語義同態，而非完整同構。

本文進一步提出雙平面架構：

\boxed{ \text{Execution Plane} \quad\parallel\quad \text{Audit / Understanding Plane} }

Execution Plane 允許 AI 在 $L_A$ 中運行，經工具與 runtime 造成真實狀態轉移；Audit Plane 則要求每個重要操作能產生可追蹤 artifact、formal obligation、certificate、counterexample 或 provenance，沿 $L_F\to L_E\to L_H$ 被驗證與解釋。因此：

\boxed{ \text{Human-readable explanation} \neq \text{source of correctness}. }

正確性應盡量由 $L_F$ 的 machine-checkable certificate、formal verification、test witness 或可重現計算支撐； $L_E,L_H$ 則負責理解、審查與決策。

本文與 CompCert 的語義保持式多中介語言、Proof-Carrying Code 的「程式＋可驗證安全證明」、autoformalization 的自然語言—形式語言橋、以及 2025 年「intermediate language challenge」存在直接結構親緣。近期研究顯示，不同 formal intermediate languages 會實際影響 LLM neurosymbolic reasoning 的 syntactic / semantic performance；ProofBridge 等工作則開始同時要求自然語言與 Lean 形式化之間的 type correctness 與 semantic correctness。這支持本文的中心論點：中介層不是透明管道；其表示選擇本身會影響可計算性、可驗證性與保真度。

本文定義 Multi-Layer Bridge System（MLBS）、層間契約、forward execution path、reverse audit path、semantic anchor graph 與 translation-loss budget；證明一個簡單的逐層誤差累積上界，並提出 certificate separation、anti-laundering、traceability、uncertainty preservation 與 human intervention depth 等八項設計原則。本文亦承接作者既有「主體—語言—對象對齊模型」的多層語言棧與 Symbol-as-Operator System（SOS）的「符號可同時攜帶語義與操作結構」觀，但不將這些既有內部框架直接當成本文已驗證的 universal solution。

本篇最後提出五類失敗：形式層失真、解釋洗白、不可追溯壓縮、跨層權限漂移與專家層空洞化。Paper 07 將進一步研究：何時任何有限多層橋都不可避免地失真、過貴、不可驗或不可計算。

關鍵詞： 多層符號橋、AI-native representation、formal intermediate language、autoformalization、proof-carrying code、semantic preservation、human-readable explanation、expert layer、provenance、traceability、AI for Science

0. 問題：未來人類是否只剩意圖層？

考慮一個極端但合理的未來結構：

\boxed{ H_{\mathrm{intent}} \rightarrow A_{\mathrm{opaque}} \rightarrow Y. }

人類只提供：

我要更好的電池。
我要一個新的數學定理。
我要這段程式安全且更快。
我要一個符合這些條件的新材料。

AI 在內部：

\mathfrak W_A

完成：

高維搜尋；
machine-native 推理；
多代理協作；
自動證明；
模擬；
程式生成；
實驗規劃。

最後只回：

完成。

技術上這可能非常高效。

但對科學文明而言，這種架構有一個巨大代價：

\boxed{ \text{結果能力上升} \quad \text{但中間可承接知識下降。} }

1. 「可讀」不是只有一種

我們首先反對一個常見二分：

\text{human-readable} \quad\text{vs}\quad \text{machine-readable}.

這太粗。

實際上至少有：

machine-operational；
machine-verifiable；
expert-readable；
general-human-readable。

因此：

\boxed{ \text{readability is layer-relative}. }

一個 Lean proof：

對一般人很難讀；
對數學形式化專家可讀；
對 kernel 可驗；
對 theorem prover 可操作。

一個 latent vector：

對人可能不可讀；
對模型卻可以直接參與後續計算。

所以：

\boxed{ \text{不可被一般人直接讀} \neq \text{完全不可審核}. }

2. 四層架構

本文定義：

\boxed{ \mathbb L = ( L_A,L_F,L_E,L_H ). }

2.1 $L_A$ ：AI-native / Machine-Operational Layer

這一層只要求：

對 AI / Agent 高效率；
可進入 tool / runtime；
可壓縮；
可組合；
可高速搜索；
可以是人類陌生格式。

例如可能包括：

latent code；
graph state；
operator representation；
machine-specific DSL；
structured protocol；
learned tokens；
multimodal states；
future AI-oriented symbol formats。

本文不假設任何目前格式，例如 JSON，是 AI 的「內在語言」。

2.2 $L_F$ ：Formal / Verifiable Shared Layer

這一層的任務不是漂亮。

而是：

\boxed{ \text{把可驗證義務寫清楚。} }

包括：

formal specification；
theorem statement；
proof object；
type；
invariant；
contract；
pre/postcondition；
execution certificate；
test witness；
model-checking condition；
proof-carrying artifact。

$L_F$ 的價值是：

不需要知道 AI 內部每一步怎麼想，仍可檢查它聲稱的重要結論是否滿足形式條件。

2.3 $L_E$ ：Expert-Facing Semantic Layer

這一層面向：

數學家；
物理學家；
工程師；
程式設計師；
醫學／領域專家。

它需要能回答：

問題是什麼？
哪些假設用了？
哪些步驟是定理？
哪些是數值逼近？
哪些是 heuristic？
哪些是證書？
哪些是模型外推？
失效條件是什麼？
怎麼重現？

所以：

L_E

不是「白話」。

它可以非常技術化。

2.4 $L_H$ ：General Human Layer

面向一般決策者／非專家。

它至少要提供：

目的；
主要結論；
重要限制；
風險；
不確定性；
下一步；
哪些內容不能只靠摘要相信。

它不是把全部數學翻成故事。

而是：

\boxed{ \text{decision-sufficient human interface}. }

3. 為什麼不能只做 $L_A\to L_H$

最直覺架構：

L_A \rightarrow L_H.

例如：

AI 做完 10 億步推理，最後自動寫一篇很好懂的報告。

問題在於：

\boxed{ \text{explanation fluency} \neq \text{semantic fidelity}. }

如果中間沒有：

L_F,

人類可能只得到一個「看起來合理」的故事。

這就是本文稱為：

\boxed{ \text{Explanation Laundering}. }

4. Explanation Laundering

定義：

若原始 AI artifact：

a_A

包含錯誤、不確定性或不可驗證跳躍，

但：

\tau_{AH}(a_A)

被生成為流暢、確定、合理的人類敘述，

使接收者無法再看到原始風險，

則稱：

\boxed{ \text{explanation laundering}. }

這是未來 AI 科學的一個重要風險。

5. Formal Layer 的角色：不要讓解釋負責真值

本文主張：

\boxed{ \text{Validity} \leftarrow L_F, }

而：

\boxed{ \text{Understanding} \leftarrow L_E,L_H. }

二者不可混。

例如：

數學

$L_F$ ：

Lean theorem + proof object

$L_E$ ：

這個證明依賴 Lemma A/B/C，核心使用 induction。

$L_H$ ：

在這些公理與定義下，形式證明已通過 kernel 檢查。

6. Proof-Carrying Code 提供的重要前例

Necula 的 Proof-Carrying Code（PCC）提出一個非常重要的架構：

不可信 code provider 除了傳送程式，也傳送一個 host 可以快速驗證的 safety proof。[1]

這裡最重要的不是歷史上的具體安全政策。

而是結構：

\boxed{ \text{artifact} + \text{certificate}. }

因此本文把它一般化成：

\boxed{ a_A + c_F. }

AI-native 結果可以很難讀，

但應盡可能附帶：

proof；
certificate；
witness；
invariant report；
reproducer；
test trace。

7. CompCert：中介表示可以多層，但語義保持要被證明

CompCert 的 verified compiler 工作展示：

\text{high-level source} \rightarrow \text{multiple intermediate representations} \rightarrow \text{assembly}

可以在 compiler pass 間建立 formal semantic preservation proof。[2]

這是一個對本文極重要的類比。

我們不應要求：

L_A=L_F=L_E=L_H.

真正需要的是：

\boxed{ \text{每一層轉換都具有明確 preservation contract}. }

8. 中介語言不是透明選擇

2025 年「Intermediate Languages Matter」研究直接指出，在 neurosymbolic LLM reasoning 中，不同 formal intermediate language 的選擇會影響模型 syntactic 與 semantic reasoning performance。[3]

因此：

\boxed{ \text{translation layer} \neq \text{neutral pipe}. }

它會：

改變 search space；
改變可表達性；
改變錯誤型態；
改變 syntax burden；
改變 solver interaction。

所以本文不尋找單一神聖 $L_F$ 。

9. Autoformalization：NL ↔ Formal Layer 正在成為真實工程問題

2024–2025 的 Lean autoformalization 工作顯示，自然語言到形式語言的 translation 需要：

compiler / type-check feedback；
semantic equivalence checking；
iterative repair；
process supervision。

ProofBridge 更進一步把自然語言 theorem+proof 到 Lean theorem+proof 的轉換視為 semantic alignment 問題，並同時評估 type correctness 與 semantic correctness。[4][5][6]

這支持：

\boxed{ L_E \leftrightarrow L_F }

不是單向「翻譯一次就算」。

它應是：

\boxed{ \text{translate} \rightarrow \text{verify} \rightarrow \text{repair}. }

10. Multi-Layer Bridge System

定義：

\boxed{ \mathfrak B = ( \mathbb L, \mathbb T, \mathbb V, \mathbb P ). }

其中：

\mathbb L = (L_A,L_F,L_E,L_H)

是各表示層。

\mathbb T = \{\tau_{ij}\}

是層間轉換。

\mathbb V = \{V_i,V_{ij}\}

是驗證器。

\mathbb P

是 provenance / traceability graph。

11. 不要求全互連

並不需要：

\forall i,j,\tau_{ij}

都存在。

實際上更合理的是：

L_A \rightleftarrows L_F \rightleftarrows L_E \rightleftarrows L_H.

再保留一些 shortcut：

L_A\to L_E,

但 shortcut 不能跳過必要 verifier。

12. 雙平面架構

12.1 Execution Plane

\boxed{ L_H/L_E \rightarrow L_F \rightarrow L_A \rightarrow \text{Runtime}. }

人類意圖不一定每次都經 formal proof 才能執行。

但高風險操作應提高 formal gate。

12.2 Audit / Understanding Plane

\boxed{ \text{Runtime} \rightarrow L_A \rightarrow L_F \rightarrow L_E \rightarrow L_H. }

它負責：

記錄；
證書；
形式核驗；
專家重建；
人類摘要。

13. Layer Contract

對：

\tau_{ij}:L_i\to L_j,

定義 contract：

\boxed{ \mathcal C_{ij} = ( S,O,U,N,P,R ). }

13.1 $S$ ：Semantic Fidelity

任務核心：

\mathcal K_T

不能被破壞。

13.2 $O$ ：Operational Fidelity

如果：

a_i

在上一層代表「只讀」，

下一層不能變成「可寫」。

13.3 $U$ ：Uncertainty Fidelity

\text{likely} \not\to \text{certain}.

13.4 $N$ ：Norm / Permission Fidelity

保留：

permission；
policy；
safety；
scope。

13.5 $P$ ：Provenance

每一個輸出能追到：

parent artifact；
model/tool；
version；
transform；
verifier；
timestamp / hash。

13.6 $R$ ：Reconstruction / Reverse Trace

不要求真正反函數：

\tau^{-1}.

但要求至少能回答：

這個敘述對應哪個 formal object / native artifact？

14. Semantic Anchor Graph

定義：

\boxed{ \mathcal G_{\mathrm{anchor}} = (V,E). }

node 可以是：

AI artifact；
formal theorem；
source code；
proof；
expert claim；
human statement。

edge 標記：

translated-from；
proved-by；
compiled-to；
summarized-from；
depends-on；
contradicts；
approximates；
generated-by。

14.1 為什麼需要 graph，不只 hierarchy

因為一個：

L_H

句子可能同時依賴：

3 個 formal theorem；
1 個 simulation；
2 個 empirical datasets。

所以：

\boxed{ \text{provenance is a graph}. }

15. Claim-level anchors

每個 human/expert claim：

c

至少可以有：

\operatorname{anchor}(c) = \{v_1,\ldots,v_k\}.

例如：

「此演算法在條件 $C$ 下安全。」

anchor 到：

formal specification；
proof certificate；
compiler artifact；
regression tests。

16. Translation Loss Budget

每層都有可能損失資訊。

令：

\epsilon_{AF}, \epsilon_{FE}, \epsilon_{EH}

為三段 task-semantic distortion。

16.1 最簡加法界

若：

d

滿足 triangle inequality，

則：

\boxed{ d(L_A,L_H) \le \epsilon_{AF} + \epsilon_{FE} + \epsilon_{EH}. }

因此：

\boxed{ \text{多一層} }

不是免費的。

每層都增加新的失真風險。

17. 一般 Lipschitz 誤差累積上界

假設：

\tau_i

的 Lipschitz constant：

K_i.

而第 $i$ 層引入局部誤差：

\epsilon_i.

遞迴：

e_{i+1} \le K_i e_i+\epsilon_i.

則經 $n$ 層：

\boxed{ e_n \le \left( \prod_{j=0}^{n-1}K_j \right)e_0 + \sum_{i=0}^{n-1} \left( \epsilon_i \prod_{j=i+1}^{n-1}K_j \right). }

若：

e_0=0,

則：

\boxed{ e_n \le \sum_{i=0}^{n-1} \epsilon_i \prod_{j=i+1}^{n-1}K_j. }

17.1 證明

由：

e_{i+1} \le K_i e_i+\epsilon_i

逐層代入即可。

\square

17.2 意義

不是只有：

translation error 每層加一點。

如果後面的轉換：

K_i>1,

前面的小錯誤可能被放大。

所以：

\boxed{ \text{early semantic error can amplify downstream}. }

18. Formal Layer 應優先擋住什麼

$L_F$ 不應試圖形式化一切。

優先級應由風險決定。

18.1 Tier 0：無形式義務

低風險：

美學文字；
非關鍵摘要；
brainstorming。

18.2 Tier 1：Schema / Type

data shape；
argument type；
interface contract。

18.3 Tier 2：Invariant / Tests

file scope；
permission；
safety property；
regression behavior。

18.4 Tier 3：Proof / Certificate

高風險：

theorem；
cryptographic property；
memory safety；
compiler transformation；
high-stakes decision rule。

因此：

\boxed{ \text{formalization depth} = f(\text{risk},T). }

19. Human Intervention Depth

人類不是只有：

\text{Intent}

與：

\text{Accept}.

定義：

D_H

為 human intervention depth。

19.1 $D_H=0$ ：Intent-only

只給目的。

19.2 $D_H=1$ ：Outcome audit

看結果、風險、不確定性。

19.3 $D_H=2$ ：Expert-structure audit

可以讀：

L_E.

19.4 $D_H=3$ ：Formal audit

能檢查：

L_F

或依賴 proof assistant / verifier。

19.5 $D_H=4$ ：Native forensic access

必要時可對：

L_A

做 instrumentation / probe / trace。

不是要求人「理解全部 latent state」。

而是：

具有調查與驗證通道。

20. 科學文明的最低要求不是所有人懂全部

不可能要求：

每個一般人理解 AI 的全部量子材料模型。

傳統科學也不是這樣。

真正需要的是：

\boxed{ \text{layered epistemic access}. }

不同角色：

public；
domain expert；
formal-method expert；
machine verifier；

各自在不同層工作。

21. 人類的角色重新分配

未來人類可保留：

問題與價值選擇；
任務定義；
驗證標準；
反例設計；
expert theory reconstruction；
formal obligation selection；
ethical / political decision；
provenance audit。

所以：

\boxed{ \text{AI-native reasoning} \not\Rightarrow \text{human epistemic eviction}. }

前提是架構真的提供中間層。

22. 內部理論：多層語言棧已存在前置原型

既有《主體—語言—對象對齊模型》已提出至少十二層的語言棧，包括：

前意圖壓力；
被指生成；
意圖；
底空間尋址；
對象切分；
命名；
概念自然語言；
結構化自然語言；
形式骨架；
約束驗證；
共同底空間比對；
證書輸出。

該框架把語言看成：

\boxed{ \text{前符號意圖} \rightarrow \text{可共享對象} }

的多層編譯過程，而非一次性文字輸出。

本文不完整承接其認識論主張。

但其「多層棧＋約束驗證＋證書」結構與 MLBS 高度相容。

23. 內部理論：SOS 作為 AI-native layer 候選之一

既有 Symbol-as-Operator System（SOS）主張符號不只是識別碼，而可封裝：

geometry；
semantics；
composition；

並把符號組合理解成 operator composition。

本文不主張 SOS 已經是：

L_A^\ast

或 universal AI-native language。

它在本文中的地位只是：

\boxed{ \text{一個 }L_A \text{ 候選設計空間。} }

Paper 02 已經證明：

不應把某個固定格式輕易提升為 universal solution。

24. 內部 AICL 的啟示：machine-facing layer 也可拆 governance

既有 AICL（AI Ingestion & Capability Layer）把網站的 AI-facing architecture 分成：

manifest；
corpus；
capability；
governance；

使 agent 能 ingest、cite、invoke、verify 網站能力。

這提醒本文：

L_A

本身也不必是一層單一 blob。

可以進一步拆：

L_A = ( L_A^{\mathrm{data}}, L_A^{\mathrm{cap}}, L_A^{\mathrm{gov}} ).

也就是：

給 AI 看懂資料、知道能做什麼、知道不可以做什麼，是三件不同的事。

25. 跨層權限漂移

考慮：

$L_H$ ：

「幫我看看檔案，不要修改。」

$L_E$ ：

inspect repository.

$L_F$ ：

permission = read_only

$L_A$ ：

tool = write_file

即使最後輸出：

「已查看。」

整個系統仍發生：

\boxed{ \text{permission drift}. }

因此 norm / permission 必須是：

\boxed{ \text{cross-layer invariant}. }

26. 跨層不確定性漂移

$L_A$ ：

P(H)=0.63.

$L_F$ ：

confidence ∈ [0.55,0.70]

$L_E$ ：

證據略偏向 H。

$L_H$ ：

H 已被證明。

失敗。

所以：

\boxed{ U_A \rightarrow U_F \rightarrow U_E \rightarrow U_H }

必須有 fidelity contract。

27. Formal 層不能洗白不完整模型

另一種 laundering：

AI-native model：

heuristic approximation.

自動形式化：

theorem specification.

如果：

L_F

只形式化「AI 自己編的一個錯誤 surrogate」，

即使 proof checker 通過，

也不能推出：

\text{original-world claim true}.

因此：

\boxed{ \text{formal correctness} \neq \text{model adequacy}. }

這是科學 AI 特別重要的邊界。

28. 必須區分三種證明鏈

28.1 Syntactic validity

形式 object 可 parse / type-check。

28.2 Internal semantic validity

proof 對 formal specification 成立。

28.3 External adequacy

formal specification 是否忠實表達：

原始科學命題；
現實系統；
使用者需求。

ProofBridge 等 autoformalization 工作開始把 type correctness 與 semantic correctness分開評估，正是同一問題的實際版本。[6]

29. Multi-Layer Verification Matrix

Transform	必查項
$L_H\to L_E$	intent / uncertainty / scope
$L_E\to L_F$	formalization adequacy
$L_F\to L_A$	executable binding / permission
$L_A\to Runtime$	operational safety
Runtime $\to L_F$	certificate / trace
$L_F\to L_E$	theorem / evidence interpretation
$L_E\to L_H$	decision fidelity / uncertainty

30. Round-Trip Consistency

理想但不要求字面一致：

x_H \rightarrow x_F \rightarrow x'_H.

要求：

x_H \approx_T^\delta x'_H.

即 Paper 04 的 TSSH。

30.1 Round-trip test

對每個 high-risk instruction：

human input；
formalize；
compile / bind；
reverse-render；
compare task core。

如果：

D_T(x_H,x_H')>\delta,

禁止執行。

31. Commutativity Test

若一個高層意圖可以經兩條路：

L_E \rightarrow L_F \rightarrow L_A

與：

L_E \rightarrow L_A,

則要求在 runtime 相關結果上：

\boxed{ \tau_{FA}\circ\tau_{EF} \approx_T \tau_{EA}. }

若兩路結果差太多，

代表：

formalization 不足；
direct translator 漂移；
layer contract 不一致。

32. Multi-Layer Bridge 不是越多層越好

層太少：

\text{opaque}.

層太多：

\text{translation loss} + \text{latency} + \text{maintenance cost}.

因此層數也是一個最佳化問題：

\boxed{ n^\ast = \arg\min_n \left[ E_{\mathrm{semantic}} + C_{\mathrm{compute}} + C_{\mathrm{audit}} + C_{\mathrm{latency}} \right]. }

33. Layer skipping

低風險 micro-task：

L_H \rightarrow L_A

可以合理。

例如：

把按鈕 margin 加 2 px。

不需要 Lean proof。

33.1 高風險不得任意跳層

例如：

飛控 code；
cryptographic code；
medicine；
theorem claim；
irreversible database migration。

可要求：

L_H \rightarrow L_E \rightarrow L_F \rightarrow L_A.

因此：

\boxed{ \text{bridge depth is risk-adaptive}. }

34. Certificate-Carrying Scientific Result

本文提出一個未來 AI Science artifact：

\boxed{ \mathcal R = ( y, c, p, u, e ). }

其中：

$y$ ：result；
$c$ ：certificate / proof / verifier output；
$p$ ：provenance；
$u$ ：uncertainty；
$e$ ：expert explanation。

一般人看到：

L_H(y,u).

專家可以下鑽：

L_E.

形式驗證者可以下鑽：

L_F.

系統 forensic 可追：

L_A.

35. 五類失敗

F1：Formalization Mismatch

L_E\not\approx L_F.

形式證明正確，但證明錯命題。

F2：Explanation Laundering

L_H

比原始證據更確定、更完整。

F3：Trace Collapse

$L_H$ claim 找不到：

L_F/L_A

anchor。

F4：Permission Drift

跨層 action scope 改變。

F5：Expert Hollowing

系統只保留：

L_A,L_H,

形式層與專家層逐漸消失。

結果是：

一般人聽得懂故事，但沒有專家能重建中間科學。

這正是本文最想避免的文明級失敗。

36. 八項設計原則

Native Freedom
不強迫 $L_A$ 人類可讀。
Formal Obligation
高風險 claim 應有 $L_F$ obligation。
Certificate Separation
correctness 不靠 explanation。
Expert Recoverability
$L_E$ 必須能重建假設、依賴與失效條件。
Human Decision Sufficiency
$L_H$ 必須保留風險、不確定性與可行選項。
Cross-Layer Permission Invariance
權限不可漂移。
Claim-Level Provenance
每個重要 claim 可追 anchor。
Risk-Adaptive Depth
低風險可跳層；高風險加深驗證鏈。

37. 一個簡單的 Human Inclusion Metric

定義：

\boxed{ I_H(T) = w_0D_0 + w_1D_1 + w_2D_2 + w_3D_3 + w_4D_4 }

其中：

$D_0$ ：能給意圖；
$D_1$ ：能審結果；
$D_2$ ：有專家可重建；
$D_3$ ：形式層可驗；
$D_4$ ：native forensic 可追。

這不是「民主指數」。

只是用來避免：

I_H\approx D_0.

即：

人類唯一剩下的能力就是下 prompt。

38. 五項可證偽預測

P1：加入 $L_F$ 可降低 fluent-but-wrong explanation acceptance

在高風險任務，

有 formal verification / certificate 的架構應比：

L_A\to L_H

直譯更容易抓出 explanation laundering。

P2：中介語言選擇會影響最終 reasoning / formalization 表現

不同：

L_F^{(1)},L_F^{(2)}

應造成不同 syntax error、semantic error 與 solve rate。

這已與 2025 intermediate-language study 一致。[3]

P3：Claim-level provenance 提高錯誤定位速度

有 anchor graph 的 system，

在發現錯誤 claim 時應降低：

T_{\mathrm{root\ cause}}.

P4：高風險任務的 multi-layer roundtrip 可降低 permission / scope drift

相較單次 direct translation，

加入：

H\to F\to A\to H'

task-core consistency check 應降低重大執行漂移。

P5：保留 expert layer 可提高長期知識承接

若兩個系統 task accuracy 相同，

具有：

L_E

的系統應在：

expert reproduction；
theory modification；
counterexample generation；

上高於只有：

L_A+L_H

的系統。

39. Benchmark v0.1

39.1 Domain A：程式設計

Input：

修改指定 file，不得改其他 file。

比較：

Direct NL→Agent；
NL→schema→Agent；
NL→formal permission contract→Agent。

39.2 Domain B：數學

Input：

自然語言 theorem。

測：

L_E \to L_F(\text{Lean}) \to L_E'

的：

type correctness；
semantic equivalence；
proof correctness；
human theorem fidelity。

39.3 Domain C：科學模型

AI 產出：

equation；
simulation；
prediction。

要求：

L_F

包含：

assumptions；
dimensions；
boundary conditions；
executable model；
uncertainty certificate。

39.4 Domain D：AI-native symbolic format

允許 AI 自己設計：

L_A.

但必須產生：

\tau_{AF}

與 verifier。

測：

AI-native 表示是否提高效率，而不摧毀 auditability？

40. 與前五篇的統一

Paper 01：

\mathfrak W_A\neq\mathfrak W_B.

Paper 02：

\exists\mathcal M

而不是固定 universal language。

Paper 03：

(A,B,T)\in\mathcal C^\ast.

Paper 04：

\exists\mathcal Q_T

只保持 task core。

Paper 05：

\widehat{\mathcal Q}_{T,t} \rightarrow \widehat{\mathcal Q}_{T,t+1}.

Paper 06：

\boxed{ \mathcal Q_T \text{ 可以被實現在多個人／機層級。} }

即：

\boxed{ L_A \leftrightarrow L_F \leftrightarrow L_E \leftrightarrow L_H. }

41. 下一篇：不可翻譯、不可計算與代價界

現在還剩最危險的問題。

即使有：

L_A,L_F,L_E,L_H,

也可能：

根本沒有足夠保真的 $\tau$ ；
$\tau$ 不可計算；
formalization cost 太高；
audit cost 超過任務價值；
AI-native structure 無法有限壓縮；
不同世界沒有共同 task quotient；
adversarial agent 故意欺騙 bridge。

所以 Paper 07 將研究：

\boxed{ \text{Impossibility} + \text{Trade-offs} + \text{Lower Bounds}. }

42. 結論

未來 AI 不需要永遠用人類看得懂的語言工作。

這種要求可能限制：

效率；
搜索；
新表示；
新數學；
新科學。

但反過來，

也不應接受：

\boxed{ \text{Human Intent} \rightarrow \text{Opaque AI} \rightarrow \text{Unverifiable Result} }

作為唯一未來。

本文提出第三種架構：

\boxed{ \text{Native Freedom} + \text{Formal Verifiability} + \text{Expert Recoverability} + \text{Human Decision Sufficiency}. }

也就是：

\boxed{ L_A \leftrightarrow L_F \leftrightarrow L_E \leftrightarrow L_H. }

AI 可以在它自己的世界高速運作。

人類不必逐步模仿 AI 的內部計算。

但每個重要結果，都應盡可能留下足夠的：

\boxed{ \text{certificate} + \text{provenance} + \text{expert bridge} + \text{human explanation}. }

這樣未來的人類才不是只剩：

「請做。」

與：

「我相信你。」

中間仍存在：

\boxed{ \text{可驗、可學、可反駁、可承接的知識層。} }

參考文獻

[1] Necula, G. C. (1997). Proof-Carrying Code. Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '97), 106–119. DOI: 10.1145/263699.263712.

[2] Leroy, X. (2009). Formal Verification of a Realistic Compiler. Communications of the ACM, 52(7), 107–115. DOI: 10.1145/1538788.1538814.

[3] Beiser, A., Penz, D., & Musliu, N. (2025). Intermediate Languages Matter: Formal Languages and LLMs affect Neurosymbolic Reasoning. arXiv:2509.04083 / NeSy Workshop 2025.

[4] Lu, J., Wan, Y., Liu, Z., et al. (2024). Process-Driven Autoformalization in Lean 4. arXiv:2406.01940.

[5] Poiroux, A., Weiss, G., Kunčak, V., & Bosselut, A. (2024). Improving Autoformalization using Type Checking. arXiv:2406.07222.

[6] Jana, P., Kale, K., Tanriverdi, A. E., Song, C., Vishwanath, S., & Ganesh, V. (2025/2026). ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings. arXiv:2510.15681; ICLR 2026.

[7] Wang, C., Scazzariello, M., & Chiesa, M. (2025). From Scientific Texts to Verifiable Code: Automating the Process with Transformers. arXiv:2501.05252.

[8] Drechsler, R. (2025). Towards LLM-based Generation of Human-Readable Proofs in Polynomial Formal Verification. arXiv:2505.23311.

[9] Carmeli, B., Belinkov, Y., & Meir, R. (2024). Concept-Best-Matching: Evaluating Compositionality In Emergent Communication. Findings of ACL 2024, 3186–3194. DOI: 10.18653/v1/2024.findings-acl.189.

內部理論依賴

Neo.K（2026-08-14），異質智慧動態協議生成系列 Paper 01–05。
Neo.K（2026-06-27），《主體—語言—對象對齊模型：從前符號意圖、被指生成到共同底空間校正的多層語言棧》。本文承接多層語言棧、共同底空間校正、約束驗證與證書輸出的結構思想。
Neo.K（2026-05/06），《符號算子系統（Symbol-as-Operator System, SOS）》v0.1。本文只把它視為 AI-native operator representation 的候選設計之一，不主張其普遍性。
Neo.K（2026），AICL / AI Ingestion & Capability Layer。本文只承接 machine-facing layer 可區分 corpus、capability、governance 等子層的工程觀。

跨世界符號橋的多層架構：AI-native、形式驗證、專家理解與人類可讀層

跨世界符號橋的多層架構：AI-native、形式驗證、專家理解與人類可讀層

摘要

0. 問題：未來人類是否只剩意圖層？

1. 「可讀」不是只有一種

2. 四層架構

2.1 LAL_ALA​：AI-native / Machine-Operational Layer

2.2 LFL_FLF​：Formal / Verifiable Shared Layer

2.3 LEL_ELE​：Expert-Facing Semantic Layer

2.4 LHL_HLH​：General Human Layer

3. 為什麼不能只做 LA→LHL_A\to L_HLA​→LH​

4. Explanation Laundering

5. Formal Layer 的角色：不要讓解釋負責真值

數學

6. Proof-Carrying Code 提供的重要前例

7. CompCert：中介表示可以多層，但語義保持要被證明

8. 中介語言不是透明選擇

9. Autoformalization：NL ↔ Formal Layer 正在成為真實工程問題

10. Multi-Layer Bridge System

11. 不要求全互連

12. 雙平面架構

12.1 Execution Plane

12.2 Audit / Understanding Plane

13. Layer Contract

13.1 SSS：Semantic Fidelity

13.2 OOO：Operational Fidelity

13.3 UUU：Uncertainty Fidelity

13.4 NNN：Norm / Permission Fidelity

13.5 PPP：Provenance

13.6 RRR：Reconstruction / Reverse Trace

14. Semantic Anchor Graph

14.1 為什麼需要 graph，不只 hierarchy

15. Claim-level anchors

16. Translation Loss Budget

16.1 最簡加法界

17. 一般 Lipschitz 誤差累積上界

17.1 證明

17.2 意義

18. Formal Layer 應優先擋住什麼

18.1 Tier 0：無形式義務

18.2 Tier 1：Schema / Type

18.3 Tier 2：Invariant / Tests

18.4 Tier 3：Proof / Certificate

19. Human Intervention Depth

19.1 DH=0D_H=0DH​=0：Intent-only

19.2 DH=1D_H=1DH​=1：Outcome audit

19.3 DH=2D_H=2DH​=2：Expert-structure audit

19.4 DH=3D_H=3DH​=3：Formal audit

19.5 DH=4D_H=4DH​=4：Native forensic access

20. 科學文明的最低要求不是所有人懂全部

21. 人類的角色重新分配

22. 內部理論：多層語言棧已存在前置原型

23. 內部理論：SOS 作為 AI-native layer 候選之一

24. 內部 AICL 的啟示：machine-facing layer 也可拆 governance

25. 跨層權限漂移

26. 跨層不確定性漂移

27. Formal 層不能洗白不完整模型

28. 必須區分三種證明鏈

28.1 Syntactic validity

28.2 Internal semantic validity

28.3 External adequacy

29. Multi-Layer Verification Matrix

30. Round-Trip Consistency

30.1 Round-trip test

31. Commutativity Test

32. Multi-Layer Bridge 不是越多層越好

33. Layer skipping

33.1 高風險不得任意跳層

34. Certificate-Carrying Scientific Result

35. 五類失敗

F1：Formalization Mismatch

F2：Explanation Laundering

F3：Trace Collapse

F4：Permission Drift

F5：Expert Hollowing

36. 八項設計原則

37. 一個簡單的 Human Inclusion Metric

38. 五項可證偽預測

P1：加入 LFL_FLF​ 可降低 fluent-but-wrong explanation acceptance

P2：中介語言選擇會影響最終 reasoning / formalization 表現

2.1 $L_A$ ：AI-native / Machine-Operational Layer

2.2 $L_F$ ：Formal / Verifiable Shared Layer

2.3 $L_E$ ：Expert-Facing Semantic Layer

2.4 $L_H$ ：General Human Layer

3. 為什麼不能只做 $L_A\to L_H$

13.1 $S$ ：Semantic Fidelity

13.2 $O$ ：Operational Fidelity

13.3 $U$ ：Uncertainty Fidelity

13.4 $N$ ：Norm / Permission Fidelity

13.5 $P$ ：Provenance

13.6 $R$ ：Reconstruction / Reverse Trace

19.1 $D_H=0$ ：Intent-only

19.2 $D_H=1$ ：Outcome audit

19.3 $D_H=2$ ：Expert-structure audit

19.4 $D_H=3$ ：Formal audit

19.5 $D_H=4$ ：Native forensic access

P1：加入 $L_F$ 可降低 fluent-but-wrong explanation acceptance