Verification of Neural Networks：神經網絡形式驗證的入門地圖

5月1日
讀畢需時 6 分鐘

已更新：5月2日

神經網絡愈來愈多出現在自動駕駛、醫療診斷、金融風控、異常偵測等高風險場景。問題是，模型準確率高，不等於我們知道它在所有重要情況下都會安全運作。當輸入稍微變動、資料包含敏感特徵，或者模型被放進一個反覆互動的系統入面，我們可否給出真正的 formal guarantee？

Benedikt Bollig 的 Verification of Neural Networks: Lecture Notes（arXiv:2604.25733v1）不是一篇提出新 benchmark 的 paper，而是一份從理論角度整理 neural network verification 的講義。它涵蓋 feed-forward neural networks、recurrent neural networks、attention mechanisms、transformers、specification languages 與 algorithmic verification techniques。

這份筆記特別適合想把「AI safety / robustness」講得更精確的人：不是只說模型要可靠，而是問可靠性如何寫成數學規格，哪些模型類別可以判定，哪些問題一開始就可能是 undecidable。

本文重點

這篇講義最有價值之處，是把 neural network verification 放回 formal methods 的語境。神經網絡雖然不是人手寫出的傳統程式，但它仍然是一串明確的數學運算；只要我們能把「正確性」寫成邏輯公式，就可以問這個公式是否對模型成立。

講義的主線可以簡化成三步：先為 feed-forward ReLU networks 建立規格語言，再把這些規格翻譯到可判定的 linear real arithmetic；然後轉向 RNN，展示序列模型的 emptiness problem 可以變成 undecidable；最後介紹 attention 與 transformer，指出 transformer verification 仍有大量開放問題。

一、神經網絡要驗證甚麼？

對傳統程式來說，termination、deadlock freedom、memory safety 這些規格相對自然。但對神經網絡，甚麼叫「正確」並不總是清楚。若是一個動物圖片分類器，我們很難完整形式化「這張圖是狗」的所有條件；如果能形式化，也許根本不需要學習模型。

因此，verification 通常會處理較可形式化的性質。例如：

Robustness： 對某個輸入作小幅 perturbation，分類結果不應突然改變。這對交通標誌辨識、醫療影像等任務尤其重要。

Fairness： 當某些敏感特徵改變，而其他相關特徵保持一致時，模型決策不應改變。

Equivalence： 若一個小模型要取代大模型，是否能證明它們在某個輸入區域內輸出同一類別？

Permutation invariance / equivariance： 當輸入是一組無序個體或多個 agent 的特徵時，改變排列順序不應改變整體預測，或者輸出應按同樣方式排列。

這些例子說明，verification 的第一步不是選 solver，而是把想要的行為寫成可以被機器檢查的 specification。

二、NNL：把模型行為寫成邏輯

講義為神經網絡引入一個簡潔的 specification language，稱為 Neural Network Logic（NNL）。它本質上是 linear real arithmetic（LRA） 加上一個可以描述網絡 input-output relation 的 predicate。

直觀地說，NNL 允許我們寫出這類句子：

「對所有輸入 x，如果 x 在某個安全區域 R 內，並且 x 與 x' 的 Manhattan distance 不超過 epsilon，那麼 N(x) 與 N(x') 的 argmax 應相同。」

這就是 robustness specification。Fairness、equivalence、surjectivity、injectivity、XOR correctness 等性質，也可以用同一套語言表達。

這個觀點很重要：一旦模型與規格都能放進同一個邏輯框架，verification 就可以轉化成 satisfiability problem。換句話說，我們不是只憑抽樣測試模型，而是問「是否存在一個反例輸入，令規格失敗？」

三、為甚麼 ReLU feed-forward networks 可以處理？

對 feed-forward ReLU networks，講義給出一條清晰路線：把 NNL[ReLU] 公式多項式時間翻譯成 LRA 公式，而 SAT(LRA) 是 decidable。

關鍵在於 ReLU 本身可以用線性不等式與邏輯分支表示：

若 z <= 0，輸出 y = 0；若 z > 0，輸出 y = z。

每一層的線性變換與 ReLU activation 都能被展開成 LRA constraints。多層網絡則透過 existential variables 表示中間層輸出，把每一層的約束串起來。如此一來，驗證 ReLU network 的某個 NNL specification，就可以轉成檢查一個 LRA sentence。

講義還用 Buechi automata 給出 LRA 可判定性的證明思路：把實數編碼成無限二進位字串，為公式構造 automaton，再把 satisfiability 轉成 Buechi automaton 的 non-emptiness。這部分比較理論，但它說明一件事：神經網絡驗證不是單純工程 heuristic，而可以建立在嚴格的邏輯與自動機理論之上。

四、有效可解片段：理論可判定不等於實務可擴展

講義也提醒讀者：decidable 並不代表容易。神經網絡可以有數百萬甚至更多參數，直接把所有層展開成邏輯公式，實務上很快會遇到 scalability 問題。

因此，後續章節討論了更容易求解的片段，例如限制公式形態、輸入區域、網絡結構或 activation function。這對工程實踐很重要：formal verification 的價值不只是「理論上可判定」，而是能否找到足夠有用、又可被 solver 處理的規格子集。

對做安全審計的人來說，這是一個很實際的取捨。完整驗證可能太貴，但針對某些輸入區域、某些安全邊界、某些替代模型 equivalence，仍然可以提供比隨機測試強得多的保證。

五、超越 ReLU：sigmoid、tanh、softmax 會帶來甚麼？

講義亦討論「Beyond ReLU Neural Networks」。實務模型常用 sigmoid、tanh、softmax 等 activation；一旦加入指數、對數、乘法等非線性結構，規格語言與可判定性分析會變得更複雜。

作者展示如何透過擴充語言處理部分非線性函數，例如把 exponentiation、logarithm、multiplication 等關係重新表達。這一章的訊息不是說所有網絡都突然變得簡單，而是說 activation function 的數學性質會直接影響 verification problem 的邊界。

這點對今日的深度模型尤其重要。模型架構不是黑箱符號；它用甚麼 activation、normalization、attention weighting，都會改變我們能否形式化與求解相關性質。

六、RNN：序列模型把問題推向 undecidability

講義到 RNN 章節時，風景突然改變。Feed-forward network 處理固定維度輸入；RNN 處理任意長度序列，並透過 hidden state 在時間上反覆更新。這讓它更接近 automaton 或 dynamical system。

作者考慮簡化的 Elman RNN，並把它視作 sequence-to-sequence 或 sequence-to-vector transducer。對 finite alphabet，可以透過 one-hot encoding 把字母轉成向量，再由 RNN 定義某個 language。

核心結果是：某些 RNN emptiness problem 是 undecidable。直觀上，問題問的是：是否存在某個輸入序列，令 RNN 的最後輸出超過、等於或達到某個閾值？講義透過 probabilistic finite automata 的 emptiness problem 做 reduction，說明即使看似簡單的 RNN 類別，也可能已經落入不可判定範圍。

這個結論對 AI verification 很重要。它提醒我們，序列模型與循環狀態一旦加入，不能期望所有自然規格都有完整決策程序。工程上可能需要 bounded verification、抽象化、over-approximation，或者限制架構與輸入語言。

七、Transformer：定義清楚，但 verification 還在早期

最後一章介紹 attention 與 transformer。講義先定義 attention head：query、key、value matrices 將某個位置的向量放入整個序列上下文中，再用 softmax 或 hard-attention 變體計算加權和。

之後它建立 multi-head attention layer、encoder layer、decoder layer、machine-translation transformer，以及 encoder-only transformer。這些定義讓 transformer 可以像 RNN 一樣，被視為處理任意長度序列的 transducer 或 language recognizer。

有趣的是，作者不只是描述標準架構，還用簡單例子展示 transformer 可以實作 argmax、辨認 sorted sequences、甚至識別 well-formed bracket strings。這些例子幫助讀者理解 attention 的計算能力，而不只是把 transformer 當成大型語言模型的工程元件。

不過，講義也明確指出：transformer verification 的一般正面可判定結果仍有待探索。已有一些工作研究 robustness verification，也有研究從 logic 與 circuit complexity 角度分析 transformer 可識別的 language classes；但對一般 transformer 架構，由於 Turing completeness 等結果，真正有用的 verification fragment 仍是未解問題。

八、為甚麼這份講義值得讀？

這份 lecture notes 的價值，不在於提供一個最新 SOTA solver，而在於給出一張理論地圖。

第一，它把神經網絡驗證拆成三件事：模型語義、規格語言、決策程序。很多 AI safety 討論停留在「模型可靠嗎」，但這份講義迫使我們問：可靠性到底是甚麼公式？反例長甚麼樣？哪類模型可判定？

第二，它展示不同架構有不同理論邊界。ReLU feed-forward networks 可以透過 LRA 處理；RNN 的某些自然問題是 undecidable；transformer 則仍需要找出有用又可判定的片段。

第三，它連接了 formal methods 與 modern ML。Buechi automata、linear real arithmetic、language recognition、attention heads 這些看似分散的概念，在神經網絡驗證問題上其實互相扣連。

九、小結

Verification of Neural Networks 是一份適合研究者與工程師重建基本功的筆記。它不會告訴你「把這個 package 跑一次就完成驗證」，反而更有價值：它說明神經網絡驗證到底在問甚麼、哪些保證有數學意義、哪些模型類別仍然困難。

如果 AI 系統要進入安全關鍵場景，測試集分數與 benchmark leaderboard 不足以承擔全部信任。formal verification 也許不能解決所有問題，但它提供了一套更嚴格的語言，讓我們可以清楚區分「我們測過很多例子」與「不存在某類反例」。

這正是這份講義的核心提醒：要讓神經網絡變得可被信任，第一步不是把模型說得更神秘，而是把它重新看成一個可以被定義、被規格化、被分析的數學物件。

Reference

Benedikt Bollig. Verification of Neural Networks: Lecture Notes. arXiv:2604.25733v1 [cs.LO], 28 Apr 2026. https://arxiv.org/abs/2604.25733
Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. CAV 2017.
Ashish Vaswani et al. Attention Is All You Need. NeurIPS 2017.
Buechi automata、linear real arithmetic、RNN emptiness 與 transformer language recognition 的詳細引文，見原講義各章 references。