可觀測性、可驗證性與反證框架

廣義相位交流中的觀測等價、性質可辨識、形式證書、模型落差與可證偽科學

英文題名： Observability, Verifiability, and Falsification: Observational Equivalence, Property Identifiability, Formal Certificates, Model Gaps, and Falsifiable Science in Generalized Phase Communication
系列： 廣義相位交流與載體安全（Generalized Phase Communication and Carrier Safety, GPC-CS）
Paper： 10
作者： Neo.K（許筌崴）
機構： EveMissLab／一言諾科技有限公司
理論協作： Aletheia（GPT-5.6 Sol）
版本： v1.0
日期： 2026-08-14
狀態： Public Theoretical Paper / Core-Series Closure / Non-operational Safety Theory

摘要

Paper 00–09 已建立廣義相位交流與載體安全的一套形式語言：載體狀態 $\mathcal X$ 、安全域 $\mathcal S$ 、跨載體轉導 $T$ 、重建 $D$ 、容量域 $\mathfrak C$ 、狀態算子 $O$ 、雙向耦合 $\Gamma_{AB}$ 、歷史與恢復、身份相關連續向量、共模失效，以及全域網路級聯 $\Gamma_G$ 。然而，這些對象大多被寫在「真實內部狀態」層。本文處理整個核心系列最後一個問題：

外部觀察者究竟能不能從有限輸出、有限實驗、形式模型與部署紀錄，判斷前九篇定義的內部性質真的成立？

本文首先定義觀測映射：

\boxed{ H: \mathcal X \rightarrow \mathcal Y, }

以及觀測等價：

x \sim_H x' \iff H(x)=H(x').

若安全性由指示函數：

\chi_{\mathcal S}(x)

表示，本文證明一個基本性質可觀測判準：存在只依賴觀測值的分類器：

g: H(\mathcal X) \rightarrow \{0,1\}

使：

\boxed{ \chi_{\mathcal S} = g\circ H }

當且僅當 $\chi_{\mathcal S}$ 在 $H$ 的每一個 fiber 上為常數。等價地，不存在同一觀測值同時對應安全與不安全狀態。本文定義安全歧義輸出集：

\boxed{ \mathcal A_H^{\mathcal S} = \left\{ y: H^{-1}(y)\cap\mathcal S\neq\varnothing, \; H^{-1}(y)\cap(\mathcal X\setminus\mathcal S)\neq\varnothing \right\}. }

若：

\mathcal A_H^{\mathcal S} \neq\varnothing,

則任何只看當前 $y$ 的 deterministic safety classifier 都不可能對所有狀態完全正確。

第二，本文把靜態觀測提升成時間窗觀測。對確定動力學：

x_{t+1}=F(x_t),

定義：

\boxed{ \mathcal O_T(x_0) = \left( H(x_0), H(F(x_0)), \ldots, H(F^T(x_0)) \right). }

兩個初始狀態若具有相同 $\mathcal O_T$ ，則在 $T$ 步輸出窗內不可區分。經典 Kalman 線性可觀測性正是此概念在：

x_{t+1}=Ax_t, \qquad y_t=Cx_t

下的有限維版本：觀測矩陣：

\boxed{ \mathscr O_n = \begin{pmatrix} C\\ CA\\ \vdots\\ CA^{n-1} \end{pmatrix} }

滿列秩 $n$ 當且僅當初始狀態可由長度 $n$ 的無雜訊輸出序列唯一辨識。Hermann–Krener 則將 observability 推廣到非線性系統的微分幾何設定。Takens delay embedding 提供另一條成熟鄰近路線：在特定 generic dynamical assumptions 下，單一觀測的 delay coordinates 可以重建 attractor 的嵌入結構。但本文明確不把 Takens theorem 誤寫成「任意黑箱只靠時間序列就能完整知道內部狀態」。

第三，本文區分狀態可觀測性與性質可觀測性。安全判定未必需要重建完整 $x$ ；只要所有 observationally equivalent states 對安全規格具有同一真值即可。這使驗證問題可以直接在 quotient：

\mathcal X/\sim_H

上研究，而不必把完整心智、模型或網路內部狀態全部反演。

第四，本文建立有限測試不推出全域安全的最小 no-go theorem。若測試只覆蓋有限集合：

D = \{x_1,\ldots,x_n\} \subsetneq \mathcal X,

且規格類沒有額外結構限制，則對任意未測點：

x^\star\in\mathcal X\setminus D,

總可構造兩個候選 safety predicates $s_1,s_2$ ，它們在 $D$ 上完全相同，卻在 $x^\star$ 上相反。因此任何只依賴有限測試結果、且沒有額外模型假設的程序，都不能由「全部測試通過」推出對所有 $\mathcal X$ 的 universal safety。這不是反對測試，而是把 testing、probabilistic certification 與 formal proof 的證明強度分開。

第五，本文證明 universal safety 的反例不對稱性。對命題：

\forall x\in K,\quad P(x),

只要找到一個：

x^\star\in K

使：

\neg P(x^\star),

即可否證全稱命題；但任意有限個滿足 $P$ 的樣本，在 $K$ 無限或尚未完全枚舉時，一般不能證明全稱命題。Temporal-logic falsification、S-TaLiRo、robustness-guided search 等既有工作正是在此邏輯不對稱下，將「找一個違反軌跡」與「證明沒有違反軌跡」明確區分。

第六，本文定義三值 verifier：

\boxed{ V(M,\varphi) \in \{ \mathrm{PROVED}, \mathrm{REFUTED}, \mathrm{UNKNOWN} \}. }

其中 $M$ 是明確模型， $\varphi$ 是明確規格。Soundness 要求：

V(M,\varphi)=\mathrm{PROVED} \Rightarrow M\models\varphi,

而：

V(M,\varphi)=\mathrm{REFUTED}

必須伴隨可驗證 counterexample 或其他有效反證。 $\mathrm{UNKNOWN}$ 是合法結果，不能被靜默改寫成「大概安全」。本文以 barrier certificates、reachability、SMT / neural-network verification 作為不同形式證書的成熟背景。

第七，本文正式處理模型—部署落差。設 verified model 為 $\widehat M$ ，實際系統為 $M^\star$ 。即使：

\widehat M\models\varphi,

也不自動推出：

M^\star\models\varphi.

2025 年對 deployed neural-network verification 的研究已明確區分 theoretical soundness 與 practical soundness，指出浮點、隨機部署環境與執行細節可以破壞「理論 verifier 的 soundness」到實際 runtime guarantee 的直接推論。本文因而引入 model discrepancy：

d_{\mathrm{mdl}} ( x_t^\star, \hat x_t ) \le \varepsilon_t.

若 safety margin function $h$ 為 $L_h$ -Lipschitz，且 model trajectory 已證明：

h(\hat x_t)\ge m_t>0,

只要：

\boxed{ L_h\varepsilon_t<m_t, }

便可推出：

h(x_t^\star)>0.

這形成一個最小的robust verification transfer theorem：形式證明要從模型移到部署系統，必須有足夠大的規格 margin 吸收 model discrepancy。

第八，本文建立證據強度階梯：形式證明／證書、有限域完整枚舉、機率性保證、反例／falsification、系統化測試、案例觀察，分別支持不同強度的命題。對 iid Bernoulli failure trials，若 $n$ 次測試觀察到零失敗，則 one-sided exact confidence calculation 給出：

\boxed{ p \le 1-\delta^{1/n} }

作為 confidence $1-\delta$ 的 zero-failure 上界形式。這再次顯示「零失敗測試」可以提供統計上界，但不能證明 $p=0$ 。2025 年的 probabilistic / probably-approximately-global verification 工作正代表形式保證與抽樣保證之間仍在持續發展的中間層。

第九，本文把整個 GPC-CS 改寫成一個可反證研究計畫。每個理論層都必須指定：

\boxed{ (\text{claim}, \text{scope}, \text{observation map}, \text{assumptions}, \text{certificate or test}, \text{countercondition}). }

沒有 observation map 的內部變量只是 latent theoretical object；沒有 countercondition 的陳述不是完整可證偽命題；沒有 scope 的驗證結果不能合法被擴張成全域安全。

本文不提供任何高風險實驗刺激、攻擊測試、身份操控或級聯誘發方法。它只建立防禦性、抽象化的驗證語言。Paper 10 的最終原則是：

\boxed{ \text{A formal safety theory becomes science only when its claims are connected to observable evidence and possible refutation.} }

關鍵詞： 可觀測性、驗證、反證、觀測等價、Kalman observability、nonlinear observability、Takens embedding、barrier certificate、formal verification、falsification、model discrepancy、practical soundness

0. 文獻定位與非目標

Observability 是控制理論的經典核心概念。Kalman 1960 年的工作將 controllability 與 observability 系統化帶入線性 state-space theory；Hermann–Krener 1977 年則以 differential-geometric tools 發展 nonlinear controllability and observability。

Takens 1981 年的 delay embedding theorem 則提供另一種非常不同的可觀測性直覺：在特定 generic assumptions 下，系統 attractor 的狀態幾何可由單一 observable 的延遲座標重建。這不等同於控制理論 observability，也不等同於任意黑箱 state recovery。

形式安全驗證方面，Prajna–Jadbabaie–Pappas 的 barrier-certificate framework、後續 temporal verification、reachability，以及 Reluplex 等 neural-network verifier 都展示「證明一個 property」與「只測試很多案例」具有不同邏輯強度。

Temporal-logic robustness 與 falsification 文獻則提供 counterexample-driven verification 的成熟方法：Fainekos–Pappas、Donzé–Maler 與 S-TaLiRo 等工作把 specification satisfaction、robustness margin 與 falsification 搜尋連在一起。

本文不重新發明 observability、model checking、barrier certificates、SMT verification、temporal logic 或 statistical certification。

本文的工作是將它們接到前九篇 GPC-CS 所定義的 latent carrier-state theory。

1. 真實狀態與可見輸出

設真實載體狀態：

x \in \mathcal X.

外部觀察：

\boxed{ y = H(x), }

其中：

H: \mathcal X \rightarrow \mathcal Y

為 observation map。

若有 measurement noise：

y = H(x)+\nu

或更一般：

y \sim P(\cdot\mid x).

本文先從 deterministic $H$ 開始。

2. Observational Equivalence

定義：

\boxed{ x \sim_H x' \iff H(x)=H(x'). }

這是一個等價關係。

因此狀態空間可被 quotient：

\boxed{ \mathcal X/\sim_H. }

外部觀察者若只看到當前 $y$ ，最多能區分不同 observation fibers，而不能區分同一 fiber 內部的 states。

3. Observation Fiber

對：

y\in H(\mathcal X),

定義 fiber：

\boxed{ \mathcal F_H(y) = H^{-1}(y). }

若：

|\mathcal F_H(y)|>1,

則該輸出對應多個內部狀態。

這本身不一定是問題。

真正問題是：

這些不可區分狀態在我們關心的 property 上是否仍然相同？

4. 性質可觀測性

令：

P: \mathcal X \rightarrow \mathcal Z_P

為某個 property map。

例如 safety：

P(x) = \chi_{\mathcal S}(x) \in \{0,1\}.

定義：

$P$ 對 observation $H$ 可完全辨識，若存在 $$ g: H(\mathcal X) \rightarrow \mathcal Z_P $$ 使 $$ P=g\circ H. $$

5. Property Observability Fiber Theorem

定理 5.1

存在：

g: H(\mathcal X) \rightarrow \mathcal Z_P

使：

\boxed{ P = g\circ H }

當且僅當 $P$ 在 $H$ 的每個 fiber 上為常數：

\boxed{ H(x_1)=H(x_2) \Rightarrow P(x_1)=P(x_2). }

證明

若：

P=g\circ H,

則：

H(x_1)=H(x_2)

立即給出：

P(x_1)=g(H(x_1))=g(H(x_2))=P(x_2).

反之，若 $P$ 在每個 fiber 上為常數，對：

y\in H(\mathcal X)

任選：

x\in H^{-1}(y)

定義：

g(y)=P(x).

由 fiber 常數性， $g$ 良定義。

證畢。

6. Safety Observability

取：

P = \chi_{\mathcal S}.

則存在純 observation-based exact safety classifier：

g(y)

的充要條件是：

\boxed{ H(x_1)=H(x_2) \Rightarrow \chi_{\mathcal S}(x_1) = \chi_{\mathcal S}(x_2). }

這是一個比「完整 state observable」更弱、也更實用的條件。

7. 安全歧義輸出

定義：

\boxed{ \mathcal A_H^{\mathcal S} = \left\{ y: H^{-1}(y)\cap\mathcal S\neq\varnothing, \; H^{-1}(y)\cap ( \mathcal X\setminus\mathcal S ) \neq\varnothing \right\}. }

若：

\mathcal A_H^{\mathcal S} \neq\varnothing,

則存在外部看起來完全相同、但 safety truth 不同的 states。

8. Observation-Only Safety Impossibility

推論 8.1

若：

\mathcal A_H^{\mathcal S} \neq\varnothing,

則不存在：

g: H(\mathcal X) \rightarrow \{0,1\}

能對所有：

x\in\mathcal X

完全正確判斷：

x\in\mathcal S.

此結果直接由定理 5.1 得到。

9. 看起來正常不等於內部安全

因此：

\boxed{ \text{normal-looking output} \not\Rightarrow \text{safe hidden state} }

只要安全歧義 fiber 存在。

這並不是說外部行為觀測無用。

而是說：

任何 output-only safety claim 都需要先證明或假設 property observability。

10. 完整 State Observability 與 Property Observability

完整 state observability 要求：

H(x_1)=H(x_2) \Rightarrow x_1=x_2

或在時間展開後能唯一辨識 state。

Property observability 只要求：

H(x_1)=H(x_2) \Rightarrow P(x_1)=P(x_2).

因此：

\boxed{ \text{state observability} \Rightarrow \text{property observability}, }

但反向一般不成立。

這是 GPC-CS 驗證可大幅簡化的重要入口。

11. 時間窗觀測

設 deterministic dynamics：

x_{t+1} = F(x_t).

定義：

\boxed{ \mathcal O_T(x_0) = \left( H(x_0), H(F(x_0)), \ldots, H(F^T(x_0)) \right). }

若：

\mathcal O_T(x) = \mathcal O_T(x'),

則兩個初始狀態在長度 $T$ 的 observation window 中不可區分。

12. 有限時間 Observational Equivalence

定義：

x \sim_{H,T} x'

當且僅當：

\mathcal O_T(x) = \mathcal O_T(x').

隨：

T

增加，等價類通常可以變細。

但不保證有限 $T$ 必然足以完全識別所有系統。

13. Linear Observability

對離散線性系統：

x_{t+1} = Ax_t,

y_t = Cx_t,

有：

y_t = CA^tx_0.

堆疊前 $n$ 個輸出：

\begin{pmatrix} y_0\\ y_1\\ \vdots\\ y_{n-1} \end{pmatrix} = \boxed{ \mathscr O_n } x_0,

其中：

\boxed{ \mathscr O_n = \begin{pmatrix} C\\ CA\\ \vdots\\ CA^{n-1} \end{pmatrix}. }

14. Kalman Rank Criterion

定理 14.1

對 $n$ 維離散 LTI 系統，初始狀態可由長度 $n$ 的無雜訊輸出序列唯一辨識，當且僅當：

\boxed{ \operatorname{rank} ( \mathscr O_n ) = n. }

證明

若：

\operatorname{rank} ( \mathscr O_n ) = n,

則線性映射：

x_0 \mapsto \mathscr O_nx_0

單射，故輸出唯一決定 $x_0$ 。

若 rank 小於 $n$ ，存在非零：

v \in \ker\mathscr O_n.

則：

x_0

與：

x_0+v

產生相同前 $n$ 步輸出。

故不可唯一辨識。

證畢。

15. Nonlinear Observability

對：

\dot x=f(x),

y=h(x),

Hermann–Krener 1977 的 nonlinear observability theory 使用由：

h, L_fh, L_f^2h, \ldots

生成的 observation codistribution，以及 rank conditions 判定局部弱可觀測性。

本文不重新推導完整 differential-geometric theorem。

其在 GPC-CS 的意義是：

當 carrier dynamics 非線性時，是否能由輸出識別內部狀態本身就是一個結構性數學問題，不是「多記錄一點 log」就自然解決。

16. Delay Coordinates 與 Takens Boundary

Takens 類 delay embedding 使用：

\boxed{ \mathcal D_m(x) = \left( h(x), h(F(x)), \ldots, h(F^{m-1}(x)) \right). }

在適當 smoothness、genericity、compact-manifold / attractor assumptions 下，delay map 可以形成 embedding。

但本文明確不做以下錯誤推論：

\boxed{ \text{Takens theorem} \not\Rightarrow \text{arbitrary hidden carrier state is reconstructible}. }

因為 theorem scope 與 generic assumptions 必須成立。

17. 網路 Observation Map

對 Paper 09 的全域狀態：

\mathbf X = (x_1,\ldots,x_N),

定義：

\boxed{ H_G: \mathcal X_G \rightarrow \mathcal Y_G. }

它可以只觀察：

部分節點輸出；
aggregate statistics；
logs；
external behavior；
relation measurements。

全域 safety property：

P_G(\mathbf X) = \chi_{\mathcal S_G^\star}(\mathbf X).

18. Global Safety Observability

由定理 5.1，存在只依賴全域觀測：

g_G(H_G(\mathbf X))

的 exact global-safety classifier，當且僅當：

\boxed{ H_G(\mathbf X) = H_G(\widetilde{\mathbf X}) \Rightarrow P_G(\mathbf X) = P_G(\widetilde{\mathbf X}). }

因此：

局部 telemetry 很完整，仍不代表全域 relation safety 可觀測。

19. Relation-Blind Observation

如果：

H_G

只輸出每個節點的本地健康值，

卻不觀察：

\mathcal C_G

所需的相位、延遲、同步、共享依賴或 cross-gain，

則可能存在：

\mathbf X, \widetilde{\mathbf X}

本地輸出相同，

但：

\mathbf X\in\mathcal S_G^\star,

\widetilde{\mathbf X}\notin\mathcal S_G^\star.

此時 global safety 不可由該 observation map 完全判定。

20. Verification Object 必須完整寫出

本文定義一個 verification claim：

\boxed{ \mathfrak V = ( M, \varphi, K, H, A ). }

其中：

$M$ ：被驗證模型；
$\varphi$ ：規格；
$K$ ：驗證域；
$H$ ：觀測／可測映射；
$A$ ：模型假設集合。

因此不能只說：

「系統已證明安全」。

更精確的是：

在假設 $A$ 下，模型 $M$ 對 domain $K$ 滿足 specification $\varphi$ 。

21. Specification Before Verification

形式驗證永遠驗的是：

\varphi.

如果：

\varphi

沒有包含某個真正重要的安全條件，

即使：

M\models\varphi,

也不能推出：

所有未寫進 $\varphi$ 的安全要求都成立。

因此：

\boxed{ \text{verification quality} \le \text{specification quality}. }

這不是數值不等式，而是邏輯依賴原則。

22. 三值 Verifier

定義：

\boxed{ V(M,\varphi) \in \{ \mathrm{PROVED}, \mathrm{REFUTED}, \mathrm{UNKNOWN} \}. }

PROVED 表示 verifier 建立有效證書或完整推導。

REFUTED 表示找到有效 counterexample / proof of violation。

UNKNOWN 表示方法未能決定。

23. Soundness

若 verifier 對 PROVED sound：

\boxed{ V(M,\varphi) = \mathrm{PROVED} \Rightarrow M\models\varphi. }

若對 REFUTED sound：

\boxed{ V(M,\varphi) = \mathrm{REFUTED} \Rightarrow M\not\models\varphi. }

在 counterexample-based verifier 中，REFUTED 通常應附：

c

使：

c\models\neg\varphi.

24. UNKNOWN 是合法答案

如果 solver timeout、

over-approximation 太寬、

state space 太大、

specification 太複雜，

得到：

\mathrm{UNKNOWN}

不等於：

\mathrm{SAFE}.

也不等於：

\mathrm{UNSAFE}.

因此：

\boxed{ \text{inconclusive} \neq \text{negative result} \neq \text{positive result}. }

25. Barrier Certificate 的位置

Prajna–Jadbabaie–Pappas 類 barrier certificate 研究：

若找到一個函數：

B(x)

滿足適當：

initial-set；
unsafe-set；
dynamics；

條件，

就可以證明某些軌跡不會從 initial region 到達 unsafe region。

在 GPC-CS 中，barrier certificate 是 Paper 01 safe-domain verification 的證書工具之一。

它不是安全規格本身。

26. Verification Certificate 不是 Reality Certificate

如果 verifier 證明：

\widehat M\models\varphi,

它首先只是一個：

\boxed{ \text{model-level theorem}. }

要移到 deployed system：

M^\star,

還需要：

\boxed{ \widehat M \approx M^\star }

的 conformance / model-error 證據。

27. Model Discrepancy

設 nominal model trajectory：

\hat x_t,

actual trajectory：

x_t^\star.

定義：

\boxed{ \varepsilon_t = d ( x_t^\star, \hat x_t ). }

若：

\varepsilon_t

沒有已知上界，

則 model proof 一般不能直接變成 runtime state proof。

28. Safety Margin Function

設：

h: \mathcal X \rightarrow \mathbb R

定義：

\mathcal S = \{ x: h(x)\ge0 \}.

假設：

h

為 $L_h$ -Lipschitz：

| h(x)-h(y) | \le L_hd(x,y).

若 nominal model 證明：

h(\hat x_t) \ge m_t>0,

則 model trajectory 距離安全邊界至少具有 certificate margin。

29. Robust Verification Transfer Theorem

定理 29.1

若：

h(\hat x_t) \ge m_t>0,

d(x_t^\star,\hat x_t) \le \varepsilon_t,

且：

\boxed{ L_h\varepsilon_t < m_t, }

則：

\boxed{ h(x_t^\star)>0. }

因此：

x_t^\star \in \operatorname{Int}(\mathcal S).

證明

由 Lipschitz：

h(x_t^\star) \ge h(\hat x_t) - L_h d(x_t^\star,\hat x_t).

故：

h(x_t^\star) \ge m_t - L_h\varepsilon_t > 0.

證畢。

30. Verification Margin 會被 Model Gap 消耗

定理 29.1 可以改寫為：

\boxed{ m_t^{\mathrm{runtime}} \ge m_t^{\mathrm{model}} - L_h\varepsilon_t. }

因此模型證書離 boundary 越遠，

越有空間吸收：

discretization；
floating-point；
calibration；
deployment；
unmodeled-dynamics error。

31. Practical Soundness

2025 年 deployed neural-network verification 研究明確指出：

theoretical soundness under an abstract/full-precision model does not automatically imply practical soundness under actual floating-point and potentially stochastic execution environments.

GPC-CS 對此採用一般原則：

\boxed{ \text{proof soundness} + \text{model conformance} = \text{runtime guarantee bridge}. }

沒有第二項，

不能只靠第一項。

32. Temporal Logic Robustness

對時間訊號：

y(t),

以及 temporal-logic specification：

\varphi,

Fainekos–Pappas、Donzé–Maler 類 robustness semantics 不只給出：

y\models\varphi

或否，

而定義一個 robustness value：

\rho_\varphi(y).

正 robustness 可以被理解為距離 violation boundary 的某種規格 margin。

33. Robust Satisfaction Transfer

如果某 specification robustness metric 對 signal distance 具有相應 Lipschitz / robustness guarantee：

| \rho_\varphi(y) - \rho_\varphi(\tilde y) | \le L_\rho d_Y(y,\tilde y),

且：

\rho_\varphi(\hat y) > L_\rho\varepsilon,

則任何：

d_Y(y^\star,\hat y)\le\varepsilon

的 actual signal 仍滿足：

\rho_\varphi(y^\star)>0.

這與定理 29.1 同一結構。

34. 有限測試集

令測試集：

D = \{ x_1,\ldots,x_n \} \subset K.

測試結果：

P(x_i)=1

對所有：

i.

如果：

K

尚未完全枚舉，

是否能推出：

\forall x\in K, \quad P(x)=1?

一般不能。

35. Finite-Test Non-Universality Theorem

定理 35.1

設：

D \subsetneq K

為有限測試集合，

且候選 property class 允許所有：

K\rightarrow\{0,1\}

函數。

則對任意未測：

x^\star \in K\setminus D,

存在兩個 predicates：

P_1, P_2

使：

P_1(x) = P_2(x) = 1

對所有：

x\in D,

但：

P_1(x^\star)=1,

P_2(x^\star)=0.

證明

令：

P_1(x)=1

對所有：

x\in K.

令：

P_2(x) = \begin{cases} 0, & x=x^\star,\\ 1, & \text{otherwise}. \end{cases}

則兩者在所有測試點完全一致，但全域命題不同。

證畢。

36. 定理 35.1 的正確解讀

這不是說：

testing 沒有價值。

它說：

testing 之所以能 generalize，必須依賴額外結構。

例如：

smoothness；
Lipschitz bound；
coverage；
finite-state exhaustiveness；
probabilistic sampling assumption；
symbolic model；
inductive invariant。

沒有這些，

「沒測到失敗」不能被提升成 universal theorem。

37. Counterexample Asymmetry

考慮 universal claim：

\boxed{ \forall x\in K, \quad P(x). }

只要存在：

x^\star\in K

使：

\neg P(x^\star),

全稱命題立即為假。

38. Falsification Asymmetry Theorem

定理 38.1

一個合法 counterexample：

x^\star\in K

且：

P(x^\star)=0

足以 refute：

\forall x\in K,\;P(x).

但當 $K$ 未被完全枚舉且沒有額外結構定理時，任意有限數量：

P(x_i)=1

不構成該全稱命題的邏輯證明。

證明

第一部分由 universal quantifier 的語義直接成立。

第二部分由定理 35.1。

證畢。

39. Falsification 不是 Verification 的弱版本

Falsification 的目標是：

\exists x\in K: \neg P(x).

Verification 的 universal safety 目標是：

\forall x\in K: P(x).

兩者量詞方向相反。

因此：

\boxed{ \text{failure to falsify} \neq \text{verification}. }

40. Temporal-Logic Falsification

S-TaLiRo 與 robustness-guided falsification 等方法正是搜尋：

\rho_\varphi(y)<0

的輸入／軌跡。

若找到有效軌跡，

即可反證：

\varphi

在指定模型與 domain 下的 universal satisfaction。

若沒有找到，

只表示：

在該搜尋預算與方法下未找到反例。

不自動變成：

M\models\varphi.

41. Zero-Failure Testing 仍只能給機率上界

假設每次測試獨立同分布，

失敗機率為：

p.

做：

n

次測試都沒有觀察到失敗。

則：

P ( \text{zero failures} \mid p ) = (1-p)^n.

若希望構造 confidence level：

1-\delta,

令：

(1-p_U)^n = \delta.

得到：

\boxed{ p_U = 1-\delta^{1/n}. }

42. Zero-Failure Confidence Bound

定理 42.1

在 iid Bernoulli testing 假設下，

若 $n$ 次測試觀察到零失敗，

則 one-sided exact frequentist upper-confidence construction 可寫成：

\boxed{ p \le 1-\delta^{1/n} }

於 confidence level：

1-\delta.

此式等價於 zero-failure Clopper–Pearson upper bound。

解釋

它不是：

p=0.

而是：

在 iid sampling model 與指定 confidence interpretation 下，資料支持一個 failure-probability upper bound。

因此：

\boxed{ \text{zero observed failures} \neq \text{zero failure probability}. }

43. Statistical Certification 的 Scope

若測試分布：

X\sim\mathcal D

則統計結論通常是：

P_{X\sim\mathcal D} [ \text{failure} ] \le \varepsilon

with some confidence。

它不自動推出：

\forall x\in K, \quad \text{safe}.

因為 distributional safety 與 worst-case safety 是不同命題。

44. Probabilistic Guarantee 與 Worst-Case Guarantee

因此至少要分開：

\boxed{ P_{\mathcal D} ( \text{unsafe} ) \le \varepsilon }

與：

\boxed{ \operatorname{Reach}(K) \cap \mathcal U = \varnothing. }

前者允許低機率 unsafe states。

後者要求指定域中完全不可達。

兩者都可能有價值，

但不能互相改寫。

45. Probably-Approximately-Global 類保證的位置

近年的 neural robustness verification 研究開始建立：

local formal oracle；
sampling；
coverage；
probabilistic relaxation；

之間的中間層。

這說明 verification 並非只有：

\text{formal global proof}

與：

\text{ordinary empirical testing}

兩個極端。

GPC-CS 因此允許：

\boxed{ \text{probabilistic certificate} }

成為明確證據類型。

但它必須寫清：

probability space；
confidence；
approximation scope；
local verifier assumptions。

46. 證據強度階梯

本文定義一個命題相對的 evidence ladder，而不是普遍排名所有研究方法。

對 universal property：

\forall x\in K,\;P(x),

可區分：

E0 — Anecdotal Observation

觀察少數案例。

E1 — Systematic Testing

依明確 test plan 掃描大量案例。

E2 — Statistical Guarantee

在明確抽樣模型下給 probabilistic bound。

E3 — Falsification / Counterexample

找到一個有效違反例即可否證 universal claim。

E4 — Bounded Exhaustive Verification

對有限／明確 bounded domain 完整枚舉或 solver-complete 驗證。

E5 — Formal Certificate / Proof

在模型與假設下建立 universal theorem。

E6 — Runtime-Transferred Guarantee

除了 E5，還有可證 model-to-runtime conformance margin。

這些層不是所有研究問題中的絕對線性排名。

例如 E3 對反證全稱命題具有決定性，但不能證明其相反全稱命題。

47. Evidence Type 必須對應 Claim Type

若 claim 是：

\exists x: \neg P(x),

一個 counterexample 已經是完整證明。

若 claim 是：

P_{\mathcal D}(\neg P)\le\varepsilon,

需要統計／機率證明。

若 claim 是：

\forall x\in K: P(x),

通常需要 exhaustive argument、formal proof 或足以覆蓋 $K$ 的結構性證書。

因此：

\boxed{ \text{evidence strength is quantifier-relative}. }

48. Verification Coverage

定義被真正驗證的集合：

K_{\mathrm{ver}} \subseteq K_{\mathrm{claim}}.

若：

K_{\mathrm{ver}} \neq K_{\mathrm{claim}},

就存在 coverage gap：

\boxed{ \mathcal G_{\mathrm{cov}} = K_{\mathrm{claim}} \setminus K_{\mathrm{ver}}. }

任何 proof / test report 都應明確標出：

K_{\mathrm{ver}}.

49. Scope Inflation Error

如果只證明：

\forall x\in K_{\mathrm{ver}}, \quad P(x),

卻寫成：

\forall x\in K_{\mathrm{claim}}, \quad P(x),

且：

K_{\mathrm{ver}} \subsetneq K_{\mathrm{claim}},

本文稱為：

\boxed{ \text{scope inflation}. }

這不是數學反例本身，

而是證據陳述錯誤。

50. Assumption Ledger

令模型依賴假設：

A = \{ a_1,\ldots,a_m \}.

例如：

dynamics class；
bounded noise；
observation calibration；
independent sampling；
fixed topology；
Lipschitz constant；
no hidden mode；
arithmetic semantics。

本文要求 proof statement 寫成：

\boxed{ A \Rightarrow (M\models\varphi). }

而不是隱去 $A$ 。

51. Assumption Failure

如果 runtime：

M^\star

不滿足：

A,

則原 theorem 可能完全仍然正確，

只是：

M^\star

不在 theorem scope。

因此：

\boxed{ \text{assumption violation} \neq \text{proof error}. }

但對部署安全而言，

兩者同樣可能讓保證失效。

52. Model Error 與 Specification Error

至少需要分開：

Model Error

\widehat M \neq M^\star.

Specification Error

\varphi

沒有捕捉真正需要的 property。

即使模型完美，

錯規格仍可：

\widehat M\models\varphi

但實際需求失敗。

即使規格完美，

錯模型也可讓 proof 無法轉移。

53. Observation Error

第三種是：

H_{\mathrm{model}} \neq H_{\mathrm{runtime}}.

例如：

sensor drift；
telemetry omission；
hidden state；
quantization；
aggregation。

因此 verification stack 至少包含：

\boxed{ \text{model correctness} + \text{specification adequacy} + \text{observation adequacy}. }

54. Deployment Arithmetic 也是模型的一部分

如果 verification 假設 real arithmetic / exact floating-point abstraction，

而部署系統使用不同：

precision；
ordering；
hardware kernels；
stochastic implementation；

則 runtime semantics 已經改變。

2025 年 neural verification 的 practical-soundness work 正是對這條 gap 提出直接警告。

GPC-CS 因此把 execution semantics 納入：

A.

55. 可觀測安全證書

除了 state-level certificate：

B(x),

有時希望從：

y=H(x)

直接建立：

\widetilde B(y).

若：

B = \widetilde B\circ H,

則 certificate 是 observation-factorizable。

由定理 5.1，

這要求 $B$ 在 $H$ fibers 上保持相同值。

56. Certificate Observability

定義 certificate $C(x)$ 對 $H$ 可觀測，若存在：

\tilde C

使：

C=\tilde C\circ H.

因此：

\boxed{ \text{property observable} }

與：

\boxed{ \text{certificate observable} }

不是同一件事。

安全 property 可以可觀測，

但某個特定 proof certificate 仍不可從 telemetry 重建。

57. Runtime Monitoring

若完整 universal proof 不可得，

可以使用 runtime monitor：

M_t = \mathcal M ( y_{0:t} ).

monitor 可以判斷：

observed property；
margin；
anomaly；
specification violation。

但若：

\mathcal A_{H,T}^{\mathcal S} \neq\varnothing,

即時間窗 observation fiber 仍跨越 safe/unsafe states，

runtime monitor 也無法對 hidden safety truth 完全正確。

58. Runtime Monitoring 不等於 Offline Verification

Offline verification 問：

\forall \text{ admissible trajectories}, \quad \varphi?

Runtime monitoring 問：

\text{目前已觀察軌跡前綴是否符合／接近違反 }\varphi?

因此：

\boxed{ \text{monitoring} \neq \text{verification}. }

但 monitoring 可以提供：

conformance evidence；
assumption checks；
runtime falsification。

59. GPC-CS Claim Record

本文建議未來每一個 GPC-CS 可實驗命題都存成：

\boxed{ \mathfrak R_{\mathrm{claim}} = ( C, K, A, H, M, E, R ). }

其中：

$C$ ：claim；
$K$ ：scope；
$A$ ：assumptions；
$H$ ：observation map；
$M$ ：model；
$E$ ：supporting evidence；
$R$ ：refutation / countercondition。

這是理論資料庫最小 provenance schema。

60. Paper 00 的可反證接口

Paper 00 的核心條件命題：

若 GPC-like technologies emerge，carrier-state safety becomes relevant.

其反證／收縮方向包括：

communication never causes persistent carrier-state update；
carrier-relative safety effects negligible；
symbol layer remains cleanly separated from persistent state dynamics。

因此 Paper 00 本身不是：

\boxed{ \text{future must become GPC}. }

而是 conditional research program。

61. Paper 01 的可反證接口

Paper 01 主張：

\mathcal S_G^\star = \left( \prod_i \mathcal S_i \right) \cap \mathcal C_G

在存在 relation constraints 時比單純 product 更完整。

若所有實際重要系統都發現：

\mathcal C_G = \mathcal X_G,

則 relational-safety extension 收縮。

可觀測需求：

H_G

必須足以辨識：

\mathcal C_G

是否成立。

62. Paper 02 的可反證接口

Paper 02 的核心是：

T, D, \text{fibers}, \text{side information}.

可測對象包括：

task observable fidelity；
representation / function mismatch；
reconstruction dependence on receiver state。

若：

D(u,x_1) \approx D(u,x_2)

對所有相關 states 都成立，

state-dependent reconstruction importance 下降。

63. Paper 03 的可反證接口

Paper 03 定義：

\mathfrak C(x).

可驗證問題：

throughput；
active-memory limit；
temporal resolution；
service/backlog；
capacity–fidelity envelope。

若單一資源即可預測全部 behavior，

多維容量模型可簡化。

64. Paper 04 的可反證接口

Paper 04 的核心：

O_\alpha

與：

\langle\mathfrak O\rangle.

可觀測：

repeated-update trajectory；
fixed points；
order defect；
switching behavior。

如果所有 relevant operators 幾乎 idempotent / commuting，

recursive and order-sensitive risk importance 收縮。

65. Paper 05 的可反證接口

Paper 05 定義 cross-gains：

\gamma_{AB}, \qquad \gamma_{BA}.

如果成熟系統：

\gamma_{BA}\approx0

或：

\gamma_{AB}\approx0,

bidirectional-loop analysis 退化成單向。

generalized synchronization：

\mathcal M_h

也必須有可測 $h$ 與 transverse error。

66. Paper 06 的可反證接口

Paper 06 的核心是：

noninjective update；
history dependence；
recovery language；
safe recovery path。

若：

\Phi|_K

普遍穩定可逆，

且 recovery path 始終安全，

irreversibility layer importance 下降。

67. Paper 07 的可反證接口

Paper 07 的 observable claims：

\Psi, \mathbf C, B_\tau.

可測：

representation drift；
information recoverability；
functional continuity；
lineage branching。

但：

\mathfrak F

first-person continuity 目前不在 identified observable model 中。

因此它不能被 Paper 07 的外部資料直接證成或證偽。

68. Paper 08 的可反證接口

Paper 08 可測：

p_i, \Sigma_F, \Omega_{ij}, D_i, \text{higher-order joint failures}.

若實證顯示 failure dependence 可忽略，

common-mode layer 可弱化。

若 structural heterogeneity 與 failure independence 有穩定關係，

依賴模型可簡化。

69. Paper 09 的可反證接口

Paper 09 可測／估計：

G_t, A_H, S_t, G(S_t).

核心反證條件包括：

influence truly local；
no state-dependent network reconfiguration；
no meaningful transient amplification；
cascade map nonmonotone under claimed theorem scope。

因此：

\boxed{ \text{cascade theory must be tested as dynamics, not inferred from correlation alone}. }

70. 系列統一 Verification Matrix

整個 GPC-CS 可壓成：

理論層	Latent object	可觀測／證據接口
Carrier safety	$x,\mathcal S$	state proxy, barrier/reachability, violation
Transduction	$T,D$	task fidelity, side-information dependence
Capacity	$\mathfrak C$	rate, memory, latency, backlog
Operator	$O_\alpha$	repeated-update trajectories
Coupling	$\Gamma_{AB}$	cross-response, synchronization error
History	$h,\Phi_w$	path dependence, recovery residual
Continuity	$\Psi,\mathbf C$	observable/function/lineage measures
Common mode	$\Sigma_F,D_i$	joint failures, dependency structure
Cascade	$G(S),\mathcal C$	transient response, mode changes, closure
Verification	$H,M,\varphi$	proofs, counterexamples, conformance

此表不是說每個 latent object 都必然能被完全識別。

它只是要求每個 claim 說清楚：

你到底打算用什麼 evidence 連到它？

71. Verification Dependency Graph

驗證結論本身也有依賴鏈：

\boxed{ \text{observation} \rightarrow \text{identification} \rightarrow \text{model} \rightarrow \text{specification} \rightarrow \text{certificate} \rightarrow \text{deployment transfer}. }

任一層失效，

都可能讓最終 runtime claim 需要降級。

72. Claim Strength Degradation

因此可以定義：

Strongest

M^\star\models\varphi

有 runtime-transfer proof。

Model-level

\widehat M\models\varphi.

Probabilistic

P(\neg\varphi)\le\varepsilon

在明確 distribution 下。

Tested

在有限 test set 未見 violation。

Anecdotal

少數觀察支持。

本文要求語言與 evidence level 對齊。

73. 可重現性不是 Validity 的同義詞

即使一個實驗可以 bit-for-bit 重現，

它仍可能：

規格錯；
模型錯；
scope 太小；
observation map 不足。

因此：

\boxed{ \text{reproducible} \neq \text{valid for claimed theorem}. }

但 reproducibility 是 evidence auditing 的重要必要層。

74. 驗證包應保存什麼

對未來 GPC-CS 實驗／形式驗證，

至少應保存：

model version；
specification；
scope；
assumptions；
solver / proof artifact；
observation schema；
dataset / trace provenance；
random seeds if relevant；
numerical precision；
runtime environment；
counterexamples；
unresolved cases。

本文不規定具體儲存格式。

75. UNKNOWN 的透明度

若：

V(M,\varphi) = \mathrm{UNKNOWN},

應保存原因：

timeout；
unsupported operator；
numerical uncertainty；
overapproximation；
state explosion；
incomplete observation。

這能避免「沒有結果」在後續 handoff 中被誤傳成 positive result。

76. Falsification Record

若找到 counterexample：

c,

應區分：

Model Counterexample

c

違反：

\widehat M\models\varphi.

Runtime Counterexample

真實部署 trace 違反：

\varphi.

Specification Counterexample

事件顯示：

\varphi

即使成立也沒有捕捉真正安全需求。

三者修正方向不同。

77. Model Refutation 不等於 Theory Refutation

如果某個具體：

\widehat M

被反例推翻，

只代表：

\widehat M

不足。

GPC-CS 的更高層 framework 只有在其 structural claims 也被系統性否定時才需要收縮。

因此必須分開：

\boxed{ \text{instance falsification} }

與：

\boxed{ \text{framework falsification}. }

78. Framework Falsification

例如若大量成熟跨載體系統都顯示：

carrier state 幾乎不影響 reconstruction；
cross-gains negligible；
history irrelevant；
failure independence high；
network reconfiguration absent；

那麼 GPC-CS 的廣義強版本就被實證壓縮成較接近傳統通信安全的窄版本。

這就是一個真正可被世界修正的理論。

79. 理論成功也不要求所有風險都出現

反過來，

如果只觀察到：

carrier-relative reconstruction；
capacity dependence；

但沒有：

identity-related drift；
cascades；

也不表示前兩層失效。

GPC-CS 是模組化條件理論。

不是：

\boxed{ R_C,R_T,R_K,R_O,R_B,R_I,R_U,R_M,R_G \text{ 必須全部同時存在}. }

80. 科學性來自可收縮性

一個好的前瞻安全理論不應只能：

無論發生什麼都說自己對。

因此本文要求每個強主張都具有：

\boxed{ \text{conditions under which it becomes unnecessary}. }

也就是：

未來資料若顯示某風險機制沒有實質作用，理論應縮小，而不是重新解釋到永遠無法被反駁。

81. Paper 10 的十二個主命題

命題 A：Property observability 是 fiber constancy

\boxed{ P=g\circ H \iff P \text{ 在 }H\text{ fibers 上為常數}. }

命題 B：Safety ambiguity fiber 使 observation-only exact safety classification 不可能

\mathcal A_H^{\mathcal S}\neq\varnothing.

命題 C：完整 state observability 比 property observability 強

安全驗證不一定需要完整重建所有 latent state。

命題 D：Linear observability 可由 Kalman rank criterion 精確判定

\operatorname{rank}(\mathscr O_n)=n.

命題 E：有限測試在沒有額外結構時不推出 universal safety

由定理 35.1。

命題 F：一個 counterexample 足以反證 universal safety，而 failure-to-falsify 不等於 verification

由量詞不對稱。

命題 G：Formal verification 必須明確綁定 model、specification、scope 與 assumptions

\mathfrak V=(M,\varphi,K,H,A).

命題 H：UNKNOWN 必須保留為第三種合法驗證結果

不能靜默升級。

命題 I：Model-level proof 不自動轉移到 runtime

需要 model discrepancy / conformance bound。

命題 J：足夠 specification margin 可以吸收 bounded model error

\boxed{ L_h\varepsilon_t<m_t \Rightarrow h(x_t^\star)>0. }

命題 K：零失敗測試提供 statistical upper bound，而非 $p=0$

\boxed{ p_U=1-\delta^{1/n}. }

命題 L：GPC-CS 必須是可反證、可收縮的條件理論

沒有反證條件的強主張不屬於本系列最終公共版本。

82. 可證偽性

Paper 10 本身也可以被修正。

82.1 所有重要 GPC properties 都由簡單 telemetry 完全決定

若：

\mathcal A_H^P=\varnothing

對所有重要 properties 與成熟系統都成立，

hidden-state observability problem 的實際重要性下降。

82.2 Runtime 與 verified model 幾乎完全一致

若可證：

\varepsilon_t\approx0

且 arithmetic/runtime semantics 完全等價，

model-to-deployment gap 可以忽略。

82.3 有限測試域本身就是完整有限 domain

若：

D=K

且已完全枚舉，

定理 35.1 的未測點限制不適用。

82.4 形式驗證取得完整 scalability

若未來所有 relevant GPC models 都能被 sound-and-complete verifier 在可接受成本內決定，

probabilistic / falsification / incomplete methods 的必要性會下降。

83. Core Series Closure：Paper 00–10

至此核心系列形成十一篇：

Paper 00

廣義相位交流與載體安全總論。

Paper 01

載體狀態空間與安全域。

Paper 02

跨載體轉導與重建錯配。

Paper 03

容量向量、維度錯配與更新速率。

Paper 04

算子誘發風險與遞歸動力學。

Paper 05

雙向相位耦合與反向影響。

Paper 06

不可逆更新與路徑依賴安全。

Paper 07

身份漂移與跨載體連續性。

Paper 08

共模失效與異質載體韌性。

Paper 09

全域相位網路與級聯動力學。

Paper 10

可觀測性、可驗證性與反證框架。

這十一篇構成 GPC-CS 第一個完整理論閉環。

84. 整體數學骨架

整個核心系列可壓縮成：

\boxed{ x \xrightarrow{E} z \xrightarrow{T} u \xrightarrow{D(\cdot,x)} r \xrightarrow{F} x^+ }

單載體安全：

\boxed{ x\in\mathcal S. }

容量：

\boxed{ q\in\mathfrak C(x). }

算子：

\boxed{ x^+=O_\alpha(x). }

雙向：

\boxed{ (x_A^+,x_B^+) = \Gamma_{AB}(x_A,x_B). }

歷史：

\boxed{ x_w=\Phi_w(x_0). }

群體：

\boxed{ \mathbf X_{t+1} = \Gamma_G(\mathbf X_t). }

全域安全：

\boxed{ \Gamma_G ( \mathcal S_G^\star ) \subseteq \mathcal S_G^\star. }

觀測：

\boxed{ y=H(x). }

驗證：

\boxed{ V(M,\varphi) \in \{ \mathrm{PROVED}, \mathrm{REFUTED}, \mathrm{UNKNOWN} \}. }

85. 核心系列的最終問題

Paper 00 一開始問：

如果未來交流不再只是訊息，而是狀態耦合，安全問題會變成什麼？

Paper 10 現在可以給出完整答案。

我們至少必須知道：

狀態是什麼？
什麼狀態叫安全？
轉導保留了什麼？
載體能承受多少？
輸入誘發了什麼更新算子？
雙方是否形成閉環？
歷史是否可逆、可恢復？
哪些 identity-related quantities 持續？
多個載體是否共享失效模式？
局部擾動是否變成網路動力學？
以上這些東西，我們到底觀察得到、驗證得到、反駁得到嗎？

第十一問是前十問成為科學研究，而不只是形式敘事的條件。

86. 最終結論

一套安全理論可以在紙上定義非常漂亮的：

\mathcal X, \quad \mathcal S, \quad T, \quad D, \quad O, \quad \Gamma, \quad G.

但如果真實系統只輸出：

y=H(x),

而：

H

把安全與不安全狀態壓在同一 fiber 中，

那麼外部觀察者根本不能從 $y$ 完整判斷 safety truth。

因此 Paper 10 的第一個根本結果是：

\boxed{ P=g\circ H \iff P \text{ is constant on observation fibers}. }

第二個根本限制是：

\boxed{ \text{finite successful testing} \not\Rightarrow \text{universal safety}. }

第三個則是量詞不對稱：

\boxed{ \text{one valid counterexample} \Rightarrow \text{universal claim refuted}, }

但：

\boxed{ \text{failure to find a counterexample} \not\Rightarrow \text{universal claim proved}. }

第四個是 deployment boundary：

\boxed{ \widehat M\models\varphi \not\Rightarrow M^\star\models\varphi }

除非我們另外控制 model gap。

若：

h(\hat x)\ge m,

d(x^\star,\hat x)\le\varepsilon,

以及：

L_h\varepsilon<m,

才得到一個最簡潔的 robust transfer：

\boxed{ h(x^\star)>0. }

因此，GPC-CS 第一個核心系列的最終原則不是：

我們已經知道未來一定會出現這些危險。

而是：

\boxed{ \text{If such coupling structures emerge, define them clearly enough that they can be observed, verified, or refuted before they become invisible assumptions.} }

這正是本系列最初的目的：

不等技術完成之後才第一次問下一步會發生什麼。

但同樣重要的是：

也不因為我們提前提出了數學框架，就把未來尚未觀測到的機制寫成既成事實。

所以 GPC-CS 的公共理論應永久保留三個出口：

\boxed{ \text{PROVE}, \qquad \text{REFUTE}, \qquad \text{REVISE}. }

若未來資料支持某一層，就把它提升為更強的實證理論。

若資料反對某一層，就收縮它。

若觀測能力不足，就標記 unknown。

這不是理論的退讓。

這是它能夠真正活到未來技術出現時，仍然具有科學價值的必要條件。

參考文獻

Kalman, R. E. (1960). Contributions to the Theory of Optimal Control. Boletín de la Sociedad Matemática Mexicana, 5, 102–119.
Hermann, R., & Krener, A. J. (1977). Nonlinear Controllability and Observability. IEEE Transactions on Automatic Control, 22(5), 728–740. DOI: 10.1109/TAC.1977.1101601.
Takens, F. (1981). Detecting Strange Attractors in Turbulence. In Dynamical Systems and Turbulence, Warwick 1980, Lecture Notes in Mathematics 898, 366–381. DOI: 10.1007/BFb0091924.
Prajna, S., Jadbabaie, A., & Pappas, G. J. (2007). A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates. IEEE Transactions on Automatic Control, 52(8), 1415–1428. DOI: 10.1109/TAC.2007.902736.
Fainekos, G. E., & Pappas, G. J. (2009). Robustness of Temporal Logic Specifications for Continuous-Time Signals. Theoretical Computer Science, 410(42), 4262–4291. DOI: 10.1016/j.tcs.2009.06.021.
Donzé, A., & Maler, O. (2010). Robust Satisfaction of Temporal Logic over Real-Valued Signals. In FORMATS 2010, LNCS 6246, 92–106. DOI: 10.1007/978-3-642-15297-9_9.
Annpureddy, Y., Liu, C., Fainekos, G. E., & Sankaranarayanan, S. (2011). S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems. In TACAS 2011, LNCS 6605.
Katz, G., Barrett, C., Dill, D., Julian, K., & Kochenderfer, M. (2017). Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. arXiv:1702.01135; CAV 2017.
Xiang, W., Tran, H.-D., & Johnson, T. T. (2017/2018). Reachable Set Computation and Safety Verification for Neural Networks with ReLU Activations. arXiv:1712.08163.
Szász, A., Bánhelyi, B., & Jelasity, M. (2025). No Soundness in the Real World: On the Challenges of the Verification of Deployed Neural Networks. Proceedings of ICML 2025, PMLR 267, 58088–58105.
Blohm, P., Indri, P., Gärtner, T., & Malhotra, S. (2025). Probably Approximately Global Robustness Certification. Proceedings of ICML 2025, PMLR 267, 4570–4587.
Boetius, D., Leue, S., & Sutter, T. (2025). Solving Probabilistic Verification Problems of Neural Networks using Branch and Bound. Proceedings of ICML 2025, PMLR 267, 4660–4699.
Kresse, F., Yu, E., Lampert, C. H., & Henzinger, T. A. (2025). Logic Gate Neural Networks are Good for Verification. Proceedings of the International Conference on Neuro-symbolic Systems, PMLR 288, 90–103.
Chehade, M. F. E. H., Li, W., Bell, B. W., Bent, R., Kazi, S. R., & Zhu, H. (2025). LEVIS: Large Exact Verifiable Input Spaces for Neural Networks. Proceedings of ICML 2025, PMLR 267, 7634–7647.

系列狀態

Series: Generalized Phase Communication and Carrier Safety
Paper: 10
Version: v1.0
Canonical source encoding: UTF-8
Canonical mathematics delimiters: $...$ and $$...$$ only
Operational high-risk experiment details: Excluded
Governance/deployment prescriptions: Out of scope
Depends on: Paper 00–09
Core Series Status: CLOSED — Foundation Cycle 00–10 complete