💻 computer science

Verification of Neural Networks (Lecture Notes)

本文提供了一份讲座笔记，对神经网络验证进行了理论性介绍，涵盖了前馈网络、循环神经网络和 Transformer 等架构，以及规范语言和算法技术。

原作者： Benedikt Bollig

发布于 2026-04-29

📖 1 分钟阅读☕ 轻松阅读

原作者： Benedikt Bollig

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你建造了一台极其复杂、如同黑盒般的机器，它能识别照片中的猫、翻译语言，甚至驾驶汽车。你知道它大多数时候运作良好，但你不知道它为何会做出这些决策，而且你担心它可能会因为相机前飞过一只鸟，就突然把“停车标志”判定为“限速标志”。

本系列讲座由 Benedikt Bollig 主讲，它就像一本指南，供数学侦探们试图查明这些“黑盒”机器（神经网络）是否安全可靠。作者并非仅仅用一百万张图片来测试它们，而是提出：我们能否从数学上证明这台机器绝不会犯某种特定的错误？

以下是该论文旅程的拆解，辅以简单的类比：

1. 目标：证明机器是“好”的

论文开篇指出，虽然我们可以训练这些机器，但我们仍需要形式化保证。这就像建造一座桥梁：你不会仅仅让几辆车开过去看看它是否承重，而是会计算物理原理以证明它不会坍塌。

挑战：神经网络是“不透明”的。它们由难以解读的数学层构成。
解决方案：作者提出了一种“规范语言”。将其想象为用机器能理解的语言编写一本严格的规则手册。例如：“如果你看到一只狗，即使我在图片中加入极微小的噪声，你也必须回答‘狗’。”

2. 简单机器：前馈网络

首先，论文考察了最简单的网络类型（前馈网络）。想象一条工厂流水线，包裹从一个站点移动到下一个站点，在每个站点进行处理，但绝不会倒退。

好消息：对于这类简单网络，作者证明了可以解决验证问题。
魔法技巧：作者表明，我们可以将整个网络的行为转化为一个巨大的数学谜题（线性实数算术）。如果我们能解开这个谜题，就知道该网络是安全的。
局限：虽然可以求解，但如果网络非常庞大，这可能需要极长的时间（就像试图解一个拥有十亿个格子的数独）。不过，对于许多实际规则，存在一些捷径，足以使其速度快到具有实用价值。

3. 循环机器：循环神经网络（RNN）

接下来，论文考察了处理序列的网络，例如逐字阅读句子。这就像是一个机器人，它会记住刚才读到的内容，以便理解下一个词。

坏消息：作者证明，对于这类循环机器，在一般情况下验证是不可能的。
类比：这就像问：“这个机器人会陷入无限循环吗？”数学表明，对于这类特定机器，不存在一种算法能为每一种可能的场景给出“是”或“否”的答案。这是逻辑的根本局限，而不仅仅是计算能力的不足。
原因：作者指出，这些机器足够强大，可以模拟“概率有限自动机”，而众所周知，概率有限自动机是无法被完全验证的。

4. 现代巨人：Transformer 与注意力机制

最后，论文考察了驱动现代 AI（例如正在与你对话的这个）的"Transformer"。这些模型使用一种称为**注意力（Attention）**的机制。

类比：想象一名学生在阅读一篇长文章。普通读者是逐字阅读的。而“注意力”机制则像一名学生，可以瞬间跳转到文章的任意部分，查看其与当前句子的关联。他们可以纵观整页内容，以决定下一个词是什么。
现状：论文解释了这些机器是如何构建的（由多层“注意力头”和“前馈”层组成）。
谜团：作者承认，虽然我们要理解它们的工作原理，但我们尚不知道能否验证它们。
- 这些机器的一些简单版本（仅编码器）可以执行诸如在列表中查找最大数字或检查句子是否已排序等操作。
- 然而，由于完整架构极其强大（理论上它可以模拟图灵机——最强大的计算机模型），核心问题依然是：是否有办法从数学上证明这些复杂机器是安全的？ 论文指出，这是一个开放的研究问题。

“侦探工作”总结

简单网络：我们拥有地图和指南针。我们可以证明它们是安全的，尽管旅程可能漫长。
循环网络：我们撞上了墙壁。数学表明，我们无法在所有情况下证明它们是安全的。
Transformer：我们正站在一个新大陆的边缘。我们知道它们很强大，但尚未绘制出地图。论文建议，找到验证它们的方法将是科学家们面临的下一个重大挑战。

这篇论文并不承诺修复这些机器，也不告诉你今天如何在医院或自动驾驶汽车中使用它们。相反，它在沙地上划出了一条清晰的界线：“这是我们可以从数学上证明的，这是不可能的，而这里是我们需要发明新数学的地方。”

基于 Benedikt Bollig 的讲义，以下是论文《神经网络的验证》的详细技术总结。

1. 问题陈述

本文探讨了为神经网络（NN）提供形式化保证的挑战，这些网络正日益部署于安全关键系统（例如自动驾驶汽车、医疗诊断）中。与传统软件不同，神经网络是基于数据训练的“黑盒”模型，其行为不透明，难以使用标准测试方法进行验证。

核心问题是验证：确定一个神经网络是否对定义域内的所有可能输入都满足特定的数学规范（例如鲁棒性、公平性、功能正确性）。本文探讨了该验证的理论极限，具体聚焦于：

可判定性：我们能否通过算法确定某个规范是否成立？
复杂性：验证的计算成本是多少？
表达能力：不同的架构（前馈、循环、Transformer）和激活函数如何影响这些属性？

2. 方法论

作者采用理论计算机科学方法，结合了：

形式逻辑：使用**线性实数算术（LRA）并将其扩展为神经网络逻辑（NNL）**以定义规范。
自动机理论：利用Büchi 自动机（在无限词上运行）来建模实数并判定算术理论。
归约：通过将已知的不可判定问题（如概率有限自动机的空性问题或修改后的后对应问题）归约到神经网络验证问题，来证明不可判定性或困难性。
架构分析：系统性地分析前馈神经网络（FFNN）、循环神经网络（RNN）和 Transformer（注意力机制）。

3. 主要贡献与结果

A. 前馈神经网络（FFNNs）

规范语言（NNL）：作者定义了神经网络逻辑（NNL），这是 LRA 的一个扩展，包含谓词 $N(x) = y$ ，表示网络的输入 - 输出关系。
ReLU 的可判定性：
- 定理：带有ReLU激活函数的 NNL 的可满足性问题（ $\text{SAT}(\text{NNL}[\text{ReLU}])$ ）是可判定的。
- 方法：该证明将神经网络转换为等价的 LRA 公式。由于 LRA 是可判定的（通过自动机理论技术），因此 ReLU 网络的神经网络验证也是可判定的。
复杂性：
- 带有 ReLU 的 NNL 的存在片段（ $\exists\text{NNL}[\text{ReLU}]$ ）是NP 完全的。
- 全称片段是coNP 完全的。
- 困难性：即使是受限的“可达性”问题（检查网络是否能从特定输入到达特定状态）也是 NP 难的，这是通过从 3SAT 归约证明的。
超越 ReLU：
- 对于使用sigmoid ( $\sigma$ )、tanh或NLReLU等激活函数的网络，验证问题等价于实指数域的一阶理论（REF）。
- 状态：REF 的可判定性（Tarski 指数函数问题）目前未知，这意味着这些通用网络的验证是一个开放问题。

B. 循环神经网络（RNNs）

不可判定性：
- 定理：RNN 的空性问题（确定是否存在任何被网络分类为正的输入序列）是不可判定的。
- 证明策略：
  1. 证明 (ReLU, sigmoid)-RNN 可以模拟概率有限自动机（PFAs）。
  2. 依赖已知结果：PFAs 的空性问题（特别是检查接受概率是否等于或超过某个阈值）是不可判定的（从修改后的后对应问题归约而来）。
- 推论：由于基本空性问题不可判定，RNN 的大部分非平凡验证任务也是不可判定的。

C. 注意力机制与 Transformer

架构：本文形式化了Transformer架构，包括注意力头、多头层、编码器和解码器。
表达能力：
- 研究表明，仅使用**仅编码器（Encoder-Only）**架构，Transformer 能够计算复杂函数（例如在序列中查找最大值、识别排序序列、识别格式正确的括号字符串）。
- 本文展示了如何利用注意力机制（例如 avg-argmax 注意力）和前馈层构建特定的 Transformer 来执行这些任务。
验证状态：
- 由于通用 Transformer 架构具有图灵完备性（它们可以模拟图灵机），通用验证很可能不可判定。
- 本文强调，虽然特定的受限片段可能是可判定的，但针对 Transformer 的通用正可判定性结果仍是一个开放的研究领域。

4. 意义与影响

理论边界：这项工作清晰地划定了理论上可验证与不可验证之间的界限。它确立了虽然简单的 ReLU 网络是可判定的（尽管是 NP 难的），但引入循环（RNN）或复杂的非线性（指数/超越函数）会将问题推向不可判定性或未知可判定性的领域。
形式化规范：它提供了一个严谨的逻辑框架（NNL）来表达诸如鲁棒性（微小输入变化不改变输出）、公平性（忽略敏感特征）和功能等价性等属性，超越了临时性的测试。
对从业者的指导：
- 对于FFNN，验证是可能的，但计算成本高昂；从业者应关注存在片段或使用 SMT 求解器。
- 对于RNN 和 Transformer，在一般情况下精确验证在理论上是不可能的。这表明这些模型的验证必须依赖抽象、近似或架构的受限子类。
未来研究方向：本文指出 Transformer 的验证和实指数域的可判定性是关键的开放问题。它建议未来的工作应集中在识别特定的架构约束，以在保持实用性的同时恢复可判定性。

总结结论

Bollig 的讲义提供了神经网络验证的基础理论分析。核心结论是：带有 ReLU 激活的前馈网络的验证是可判定的（可归约到线性实数算术），但循环网络的验证是不可判定的，而带有超越激活函数的网络或通用 Transformer 的验证状态仍为开放问题。这强调了为现代深度学习架构开发专用的、近似的验证工具的必要性，而不是依赖通用的精确验证。