💻 computer science

Differential Zonotopes for Verifying Global Robustness of DNNs

本文介绍了 TwoSafe，一种利用微分光晕带状区域（differential halo zonotopes）来高效验证深度神经网络全局鲁棒性的新型静态分析工具，其在精度和可扩展性方面均显著优于现有的最先进技术。

原作者： Anagha Athavale, Samuel Teuber, Matteo Maffei, Ezio Bartocci, Dejan Nickovic, Georg Weissenbacher

发布于 2026-06-23

📖 1 分钟阅读☕ 轻松阅读

原作者： Anagha Athavale, Samuel Teuber, Matteo Maffei, Ezio Bartocci, Dejan Nickovic, Georg Weissenbacher

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

想象一下，你构建了一个非常聪明的机器人（深度神经网络），它负责做出重要的决策，比如识别物理实验中的粒子，或者根据传感器数据识别一个人是在走路还是在站立。你希望能够绝对确定，如果输入的数据带有轻微的“噪声”或不完美（比如传感器的故障或相机镜头的污渍），这个机器人不会产生混乱。

这篇论文介绍了一种全新的、超高效的方法，用来测试这些机器人是否足够“强韧”，能够应对这种噪声而不出错。

以下是他们工作的详细拆解，使用了简单的类比：

1. 问题所在：检查每一种可能的情景

通常，当我们测试一个机器人时，我们会检查它在特定图像下的表现，然后检查在同一张图像加入微量噪声后的表现。这被称为局部鲁棒性（Local Robustness）。这就像是检查一座桥在单辆汽车驶过时是否稳固。

但作者想要检查的是全局鲁棒性（Global Robustness）。这要难得多。这就像是在问：“如果两辆车同时驶过这座桥，并且彼此靠得很近，桥面是否依然稳固？”

挑战： 检查每一对可能的输入，就像试图数清沙滩上的每一粒沙子一样。这需要巨大的计算能力，以至于旧有的工具只能处理非常小、非常简单的机器人（神经元数量极少）。

2. 旧方法 vs. 新方法

旧方法（“暴力破解”法）：
以前的工具尝试通过分别检查两个机器人并减去它们的结果来解决这个问题。想象一下，通过分别计时两个跑步者，然后再进行数学计算来测量他们的差距。问题在于，这个“数学计算”过程会引入误差，使得结果过于模糊，对于大型机器人来说毫无用处。

新方法（“并肩同步”法）：
作者创建了一个名为 TwoSafe 的新工具。他们不是分别运行两次检查，而是让它们并排运行，保持完美的同步。

类比： 想象两个双胞胎在赛跑。与其分别为他们计时然后再比较时间，不如让他们手拉手（或被绳子连在一起）一起跑。你测量的是他们奔跑过程中双手之间的距离。
创新点： 他们使用了一种被称为带状体（Zonotope）的数学形状（可以理解为一个灵活的多维气球）来追踪这对双胞胎。他们发明了一个特殊版本，称为微分晕带状体（Differential Halo Zonotope）。
- 这个“晕（Halo）”就像是围绕在双胞胎周围的安全气泡。它允许他们稍微分开（模拟噪声/扰动），但又能紧紧控制住他们分离的具体程度。这防止了旧方法中那种“模糊数学”导致的误差。

3. 更聪明的规则：“置信度”漏洞

论文还引入了一个关于什么才算作“失败”的新规则。

严格规则（非对称规则）： 如果机器人看到一张清晰的“狗”的照片（确信度 99%），而微小的噪声让它认为是一只“猫”（即使确信度只有 10%），严格规则会判定：失败。无论机器人对“猫”这个标签有多么不确定，它都改变了判断，所以它是失效的。
更聪明的规则（对称规则）： 作者说：“等等。”如果机器人看到一只“狗”（99% 确信），而噪声让它觉得是“猫”（10% 确信），这其实没关系！机器人实际上是在表达：“我认为它是狗，但如果非要我猜，我对‘猫’这个标签其实很不确定。”
- 类比： 想象一名保安。如果他 99% 确定某人是员工，但一点点雾气让他犹豫并说“也许是个陌生人？”（置信度很低），他不应该被开除。只有当他自信满满地大喊“陌生人！”而实际上对方是员工时，他才算失职。
- 这个新的对称规则允许该工具验证更复杂的机器人，因为它忽略了那些人类自然会发现或忽略的“低置信度”错误。

4. 结果：规模化升级

作者将他们的工具 TwoSafe 应用到了现实世界的机器人任务中，包括：

粒子物理学 (LHC)： 在大型对撞机中对粒子进行分类。
人体活动识别 (HAR)： 通过佩戴式传感器判断一个人是在走路还是在坐着。
空中交通管制 (ACAS)： 防止飞机碰撞。

最终成果：

速度： TwoSafe 比之前的最优工具显著更快。
规模： 旧工具只能处理小型机器人（约 15 个神经元），而 TwoSafe 成功验证了拥有 500 个神经元和 561 维输入的机器人。这就像是从检查一辆自行车升级到了检查一艘巨大的货轮。
准确性： 旧工具经常因为数学计算过于粗糙而发出“假警报”（误以为机器人坏了，其实并没有）。TwoSafe 则精确得多，在他人判定失败的地方证明了安全性。

总结

这篇论文提出了一种新的数学“安全护栏”（微分晕带状体），使我们能够测试复杂的 AI 系统在其整个运行范围内对噪声的鲁棒性。通过同步进行测试并采用更符合现实的“置信度”定义，他们成功验证了以往难以检测的、规模更大且更复杂的 AI 系统。

技术摘要：用于验证深度神经网络全局鲁棒性的微分带状区域（Differential Zonotopes）

1. 问题陈述

深度神经网络（DNN）正越来越多地部署在交通运输和医疗保健等安全关键领域，在这些领域中，其针对输入扰动的鲁棒性至关重要。虽然局部鲁棒性（确保在特定输入周围的小扰动下预测不发生变化）是一个研究充分的安全属性，但全局鲁棒性是一个更强的要求。全局鲁棒性要求对于在一定距离内的所有输入对，模型的预测必须保持一致。

形式上，全局鲁棒性是一个 2-安全性属性（2-safety property），它要求验证两个全称量化的执行轨迹之间的关系，而非单个轨迹。这种复杂性使得全局验证比局部验证要困难得多。现有的基于置信度的全局鲁棒性（将保证限制在以避免决策边界的高置信度预测上）方法依赖于专门的满足性求解器，但在可扩展性方面表现不佳，目前仅限于只有数十个神经元的网络。

2. 方法论

本文提出了一种基于**微分光晕带状区域（differential halo zonotopes）**的新型静态分析框架，以高效地验证全局鲁棒性。

2.1 微分光晕带状区域

核心技术创新是对*带状区域（zonotope）*抽象域的扩展。标准的带状区域通过一个中心和一个生成矩阵来表示点集。为了验证全局鲁棒性，作者必须同时追踪两个具有不同*输入的相同* DNN 的执行过程。

挑战： 微分带状区域（此前用于处理输入完全相同的 DNN 等价性 验证）的朴素适配无法用于全局鲁棒性。将输入初始化为相同或使用完全独立的生成器会导致不完备性（unsoundness）或过度近似（精度损失）。
解决方案： 作者引入了微分光晕仿射形式（differential halo affine forms）。这种编码将扰动界限 $\epsilon$ $ϵ$ 分布到两个生成器中：
1. 一个在两次执行之间共享的主生成器，以保持相关性。
2. 每个执行过程各自独立的次级生成器，用以建模扰动。
机制： 这种“光晕”结构允许系统以稳健且精确的方式对以下条件进行编码：两个输入 $x$ 和 $y$ 位于边界框 $[l, u]$ 内，且满足 $|x - y| \le \epsilon$ 。微分带状区域 $\mathcal{Z}_\Delta$ 以同步方式追踪两次执行之间的差异，从而比直接减去单个带状区域获得更紧凑的散度界限。

2.2 对称置信度全局鲁棒性

论文指出，现有基于置信度的全局鲁棒性定义（非对称变体）存在局限性，该定义要求高置信度输入 $x$ 不能被扰动为不同的类别 $y$ ，无论 $y$ 的置信度如何。作者认为这种要求过于严格，因为导致低置信度、不同预测的扰动在实践中是可以接受的（例如，触发人工审核）。

他们提出了一个对称变体：

定义： 对于任何在距离 $\epsilon$ 内的两个输入 $x, y$ ，如果两者的分类置信度都大于阈值 $\tau$ ，则它们必须属于同一类别。
优势： 这种放宽使得更广泛的类网络可以被视为“鲁棒”的，同时对于那些通过回退机制处理低置信度输出的安全关键应用而言，该定义依然具有意义。

2.3 验证算法

验证过程（在工具 TwoSafe 中实现）遵循以下步骤：

初始化： 构建一个代表输入空间和扰动约束的微分光晕带状区域。
传播： 将带状区域传播通过 DNN 层。对于 ReLU 激活函数，该方法引入新的生成器来过度近似非线性，同时保持微分结构。
属性检查： 在输出端，系统构建一个线性规划（LP）问题，以检查是否存在类别不同且两者均满足置信度阈值 $\tau$ 的输出对。
细化： 如果检查结果是不确定的（由于过度近似），算法会执行生成器分裂（generator splitting）。与标准的输入分裂不同，它通过分裂微分光晕带状区域的生成器来细化近似，同时不丢失对扰动空间的覆盖。

3. 核心贡献

微分光晕带状区域： 一种新的抽象域，它扩展了带状区域，使其能够以同步方式共同传播一对受扰动的输入，从而紧凑地界定它们的散度。这使得验证全局 2-安全性属性时能获得比单独分析更高的精度。
对称置信度全局鲁棒性： 一种新的全局鲁棒性定义，仅要求高置信度预测之间的一致性。该定义在严格度上低于非对称变体，并且可以在所提出的框架内进行高效验证。
完备性证明： 对基于微分带状区域的静态分析的完备性进行了形式化证明，其核心结果已在 Isabelle 中实现。
TwoSafe 工具与评估： 将该方法实现在新工具 TwoSafe 中，该工具在精度和可扩展性方面均显著优于最先进的基准方法（CGR）。

4. 实验结果

作者在四个基准测试上评估了 TwoSafe：Law（小型）、LHC（粒子分类）、ACAS Xu（碰撞规避）和 HAR（人类活动识别）。

可扩展性： TwoSafe 成功验证了拥有高达 500 个 ReLU 神经元和 561 个输入维度（HAR 基准）的网络的全局鲁棒性。相比之下，基准方法（CGR）在处理这些较大的网络时会超时或耗尽内存。
精度： 由于 Softmax 近似过于粗糙（特别是在具有许多输出类别的网络上），基准方法经常报告伪反例（spurious counterexamples）。TwoSafe 避免了这些假阳性。
性能： TwoSafe 展示了显著的加速。例如，在 LHC 基准测试中，它在不到 3 秒内完成了验证，而基准方法在 2 小时后仍处于超时状态。
对称 vs 非对称： 对称属性允许在非对称属性不确定或失败的参数范围内实现成功验证。例如，在 $\epsilon=0.01$ 的 HAR 基准测试中，对称属性是可验证的，而非对称变体则超时了。

5. 重要性与主张

本文声称解决了鲁棒性保证强度与验证工具可扩展性之间的内在矛盾。通过从局部转向全局鲁棒性验证并利用微分光晕带状区域，作者证明了验证规模更大、更深的神经网络是可能的。

对称置信度全局鲁棒性的引入被视为一项实用的进展，它通过承认低置信度预测在现实世界系统中通常会被区别对待，从而提供了一个“有意义的鲁棒性概念”，适用于更广泛的类网络。这项工作确立了微分验证在适配 2-安全性属性后，其规模可以达到处理以往技术所处理网络的数量级，使得全局鲁棒性认证对于实际部署的模型变得可行。