🤖 machine learning

Branch and Bound for Relational Verification of Neural Networks

本文介绍了 SaBRe，这是一个用于关系神经网络验证的分支定界框架，它通过基于对偶形式化选择策略来拆分关系神经元，从而提高了效率和可扩展性，并在多个基准测试中优于现有的基准方法。

原作者： Kota Fukuda, Zhenya Zhang, Guanqin Zhang, Jianjun Zhao

发布于 2026-08-14

📖 1 分钟阅读☕ 轻松阅读

原作者： Kota Fukuda, Zhenya Zhang, Guanqin Zhang, Jianjun Zhao

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

想象一下，你是车队安全检查员，负责监管一群自动驾驶汽车。这些汽车由“神经网络”驱动，本质上是超级聪明的计算机大脑，通过观察数百万个示例来学习识别停止标志或行人等物体。但问题在于，这些大脑可能会过于敏感。如果停止标志上贴了一个微小的贴纸，或者光照发生了细微变化，汽车可能会突然认为那是限速标志，然后直接加速冲过去。为了保障大家的生命安全，我们需要证明汽车的大脑不会被微小的变化所迷惑。这被称为“验证”（verification）。

长期以来，安全检查员只检查汽车是否能处理一个特定的变化，比如“如果我在图像上加一个小点，汽车还能识别出停止标志吗？”但在现实世界中，我们需要检查更广泛的情况：“无论天气如何，或者路面是否稍微有些湿滑，汽车的表现是否都能保持一致？”这被称为“关系验证”（relational verification）。这就像是在问：“如果我在两个略微不同的场景下驾驶汽车，它是否会做出同样安全的决策？”问题在于，同时检查两个场景在数学上要难得多。这就像是尝试同时平衡两个旋转的盘子，而不是一个；旧有的工具往往会变得混乱，在其实并不危险的情况下大喊“危险！”，或者完全漏掉真正的危险。

这篇论文介绍了一种名为 SABRE（用于关系验证的分裂近似界限，Splitting Approximated Bounds for RElational verification）的新工具，用以解决这个棘手的平衡难题。把检查这些汽车的旧方法想象成通过一次捡起一只袜子来整理乱糟糟的房间。如果房间很大，且袜子到处都是，你可能会花上一辈子去捡袜子，却依然漏掉了角落里那堆大衣服。作者意识到，在“关系型”问题的世界里（即同时检查两个场景），真正的混乱不在于单个数据点（即每一只袜子），而在于两堆衣服之间的差异。

因此，SABRE 改变了策略。它不再是一次捡起一只袜子，而是抓取两堆衣服之间的差异并将其拆解。想象你有两张几乎完全相同的城市地图。旧方法会分别检查两张地图上的每一条街道。然而，SABRE 会观察两张地图之间微小的差异，并基于这些差异来拆解问题。如果两张地图对某个转弯处的判断不一致，SABRE 会立即聚焦于那个分歧点。

研究人员在使用了 ACAS Xu（用于空中交通管制）、MNIST、CIFAR 和 GTSRB（用于图像识别）等标准数据集的 817 个不同安全问题上测试了这种新方法。他们发现，在解决这些问题时，SABRE 比之前的最优方法表现得好得多。事实上，它解决的问题数量更多，速度也更快。例如，在 ACAS Xu 数据集上，SABRE 解决了 67 个问题，而旧方法仅解决了 42 个。在 GTSRB 数据集上，它解决了 33 个问题，而旧方法仅解决了 9 个。

至关重要的是，论文指出，旧有的拆解问题的方法——即专注于神经网络的单个部分——对于这些“同时处理两个场景”的检查来说往往是错误的策略。通过专注于两个场景之间的关系，SABRE 能更高效地穿透混乱。作者还设计了一个聪明的“选择器”（selector），帮助 SABRE 决定下一步应该拆解哪一个差异，就像一位知道该追踪哪个线索才能最快破案的侦探一样。当他们将这个智能选择器与随机猜测者进行对比测试时，智能选择器解决了更多的题目，这证明了知道“拆解什么”与“如何拆解”同样重要。

简而言之，这篇论文表明，通过改变我们拆解问题的方式——即专注于两个场景之间的关系，而非场景本身——我们可以让自动驾驶汽车和其他人工智能系统变得更加安全且易于验证。它目前还没有解决世界上所有的难题，但它展示了一条比我们以前所拥有的路径要先进得多的清晰路径。

技术摘要：用于神经网络关系验证的分支定界法 (SABRE)

问题陈述
本文解决了针对关系规范（特别是全局鲁棒性）进行神经网络验证的挑战。与关注单个输入在微小扰动下输出保持稳定的局部鲁棒性不同，全局鲁棒性要求推理关于多个输入之间的关系进行推理。形式上，如果对于任何在限定距离 $\epsilon$ 内的两个输入，其输出之差都受到 $\delta$ 的限制，则称该网络是全局鲁棒的。

现有的关系验证方法主要依赖于可靠过近似（sound over-approximation）技术（例如 RaVeN），利用凸域来限制网络输出之间的差异。虽然这些方法效率很高，但它们本质上是不完备的，并且由于近似过于宽松，容易产生假警报（虚假反例）。虽然分支定界（Branch and Bound, BaB）是局部鲁棒性验证中通过拆分单个神经元来细化近似的标准技术，但将其应用于关系验证的尝试却非常有限。先前的尝试（例如 RABBit）通过拆分单个神经元将 BaB 应用于关系问题，作者认为这种做法未能利用关系约束的特定结构，并可能导致次优的细化效果。

方法论：SABRE 框架
作者提出了 SABRE（用于关系验证的近似界限拆分框架），这是一个专门为关系验证设计的分支定界框架。其核心创新在于将拆分策略从单个神经元转向关系神经元（relational neurons）。

关系神经元与问题拆分：
- 该框架使用关系神经元（ $\Delta y^{(i)}_j = y^{(i)}_j - \hat{y}^{(i)}_j$ ）来建模两个网络推理之间的差异，这些神经元代表了两个并行网络副本中对应神经元的差值。
- SABRE 不是基于单个神经元的激活状态（例如 $x > 0$ 与 $x < 0$ ）进行拆分，而是基于关系神经元输入的正负号（ $\Delta x^{(i)}_j \geq 0$ 与 $\Delta x^{(i)}_j \leq 0$ ）进行拆分。
- 这种方法直接针对输出差异中的不确定性，旨在比拆分单个组件更有效地收紧关系差异的界限。
基于对偶的神经元选择策略：
- 决定 BaB 效率的一个关键因素是在每一步中选择拆分哪个神经元。为了避免通过求解子问题来估计影响所带来的计算开销，SABRE 采用了验证问题的拉格朗日对偶形式。
- 作者推导出了一个对偶问题，其目标函数是神经元项的求和。这些项捕捉了在线性松弛下特定神经元对最终输出界限的贡献。
- 通过分析拆分特定关系神经元如何影响对偶目标函数中的系数，SABRE 可以在不求解子问题的情况下，高效地估计潜在的细化程度（即界限的收紧程度）。算法会选择能使估计改进量最大化的关系神经元。
工作流程：
- 过程始于一个近似验证器（如 RaVeN）来检查全局鲁棒性属性。
- 如果检测到假警报，算法会使用基于对偶的选择策略选择一个关系神经元。
- 通过对选定的关系神经元添加约束，将问题拆分为两个子问题。
- 这个递归过程持续进行，直到所有子问题都被验证或找到了真实的反例。

核心贡献

新颖的拆分策略： 本文引入了一个分支定界框架，该框架优先拆分关系神经元而非单个神经元，作者认为这直接解决了关系规范中近似误差的来源。
基于对偶的选择启发式算法： 作者将对偶形式化方法（此前用于局部鲁棒性）扩展到了关系场景，实现了高效、数据驱动的选择，以确定最具影响力的关系神经元进行拆分。
SABRE 实现： 一个集成了这些策略的完整验证框架，能够处理各种网络架构下的全局鲁棒性属性。

实验结果
作者在五个数据集（ACAS Xu, MNIST-F, MNIST-C, CIFAR, GTSRB）的 817 个验证实例上对 SABRE 进行了评估。评估对象包括：

RaVeN： 一种不具备细化能力的先进近似验证器。
ClasIS & DualIS： 拆分单个神经元的 BaB 变体（ClasIS 使用标准选择；DualIS 使用提出的对偶形式但应用于单个神经元）。
RandRS： 使用随机神经元选择的 SABRE 变体。

主要发现：

相对于 RaVeN 的性能： SABRE 表现显著优于 RaVeN，通过有效地细化 RaVeN 无法验证的近似，解决了更多的实例。
关系拆分与个体拆分： 在大多数基准测试（ACAS Xu, MNIST-F, MNIST-C, GTSRB）中，SABRE（关系拆分）解决的实例更多，探索的子问题更少，且所需时间比个体拆分方法（ClasIS, DualIS）更短。
- 注：关于 CIFAR 数据集： 在 CIFAR 数据集且扰动半径 $\epsilon$ 较小时，个体拆分方法最初优于 SABRE。作者将其归因于 CIFAR 模型中存在大量不稳定的 ReLU，这稀释了关系拆分的局部影响。然而，随着 $\epsilon$ 的增加，关系拆分变得更加有效。
选择策略： 基于对偶的选择策略（SABRE）在所有数据集上都显著优于随机选择（RandRS），在许多情况下将子问题数量和验证时间减少了约 50%。
最大可验证扰动： SABRE 始终能比基准方法认证更大的扰动区域 ( $\epsilon^*$ )，特别是在 ACAS Xu 和 MNIST-F 上，它经常能在其他方法无法认证任何内容时成功找到非平凡界限。

意义与主张
本文声称，SABRE 通过证明拆分关系神经元在全局鲁棒性验证中是比拆分单个神经元更有效的近似细化策略，标志着关系验证迈出了重要一步。作者强调，其基于对偶的选择策略为优先处理拆分提供了可靠指导，从而提高了验证的效率和可扩展性。

该研究指出，尽管由于近似的性质，该方法仍是不完备的，但所提出的技术最大化了每次拆分的细化程度，使得关系属性的形式化验证在安全至上的信息物理系统中变得更加实用。作者谦虚地提到，未来的工作可以探索在个体拆分与关系拆分之间动态切换的混合策略，但他们断言，目前仅专注于关系神经元的方法在大多数测试基准上已经取得了优异的表现。

类似论文