🤖 machine learning

Mining Verdict Boundaries for Neural Network Verification

本文提出了一种用于神经网络验证的高效分支定界方法，该方法利用路径单调性和指数搜索来同时拆分多个激活函数，从而跳过无关的子问题并精确地定位判定边界，避免了现有方法中代价高昂的顺序边界传播。

原作者： Jiawei Ren, Guanqin Zhang, Zhenya Zhang, Yulei Sui

发布于 2026-08-03

📖 1 分钟阅读☕ 轻松阅读

原作者： Jiawei Ren, Guanqin Zhang, Zhenya Zhang, Yulei Sui

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

想象一下，你正试图教会一个机器人开车。你希望能够绝对确保无论路上发生什么，机器人都不会发生碰撞。这就是**神经网络验证（neural network verification）**的世界。把神经网络想象成一个由开关和杠杆组成的巨大且复杂的迷宫。为了证明机器人的安全性，我们需要检查迷宫中的每一条路径，以确保没有任何一条会导致碰撞。

问题在于，这些迷宫规模巨大。逐一检查每一条路径就像试图用吸管喝干大海一样——这太耗时了。因此，科学家们使用了一种被称为**分支定界法（Branch and Bound）**的巧妙技巧。想象一下，你正在一片巨大的森林中寻找隐藏的宝藏。你不需要走遍每一棵树，而是将森林分成较小的区块。你从远处快速观察一个区块；如果看起来是安全的，你就跳过该区域剩余的部分。如果看起来有危险，你就将该部分进一步细分为更小的碎片并进行检查。这种“分而治之”的方法很棒，但仍然涉及大量的行走和检查。核心问题在于：我们如何在确定一个区域是安全的时候就停止检查，而不浪费时间去走遍那个区域里的每一棵树呢？

这正是这篇论文的研究人员试图解决的问题。他们注意到，当你深入探索这些森林区块时，“安全性得分”通常会以一种可预测的方式变得越来越好。这就像爬山：一旦你开始向上攀登，你就会一直向上，直到到达顶峰。旧的检查方式就像是一小步一小步地挪动，每走一步都要检查一下地面，看是否已经到达了顶峰。这种方式很周全，但速度慢得令人痛苦。

作者贾威雷（Jiawei Ren）及其团队意识到他们可以跳过这些步骤。他们提出了一种名为 BMiner 的新方法。与其迈出微小的步伐，不如使用两个聪明的技巧来向前跨越。第一个技巧类似于指数搜索（exponential search）：你先迈出一大步，然后是两倍大的步子，接着是三倍大的步子，直到你越过了顶峰。一旦你知道自己已经跳过了顶点，你只需往回走几步就能找到准确的位置。第二个技巧甚至更聪明：基于梯度的搜索（gradient-based search）。这就像观察山的坡度。如果地面上升得很快，你就知道自己离顶峰很近，因此可以进行一次巨大且自信的跳跃。如果坡度很平缓，你就迈出一小步。

通过使用这些“跳跃式前进”的策略，该团队发现他们可以更快地验证神经网络。在对标准计算机视觉模型（使用 MNIST 和 CIFAR-10 等数据集）进行的测试中，他们的方法将证明安全性所需的时间平均减少了 17% 到 30%。在最好的情况下，他们节省了近 45% 的时间。他们并非仅仅靠猜测；他们在 500 个不同的验证问题上运行了这些模拟，并将结果与目前的最佳工具进行了对比。结果表明，通过挖掘“判定边界”（verdict boundary）——即问题从“不安全”转变为“安全”的精确点——他们可以跳过大量的冗余检查。

论文还解决了一个担忧：如果这座山并不完全平滑怎么办？如果山坡上有一个微小的凸起，导致安全性得分在再次上升前略有下降怎么办？研究人员对此进行了检查，发现虽然这些凸起确实存在，但它们很罕见且通常很小。他们的方法足够鲁棒，能够处理这些情况而不会产生混乱。简而言之，他们不仅造出了一个更快的步行者，还为验证过程安装了一对喷气背包，让我们能以更少的努力、更快的速度得出“安全”的结论。

技术摘要：神经元网络验证中的判定边界挖掘

问题陈述

神经元网络验证对于确保自动驾驶等领域（特别是针对对抗性扰动）的安全性至关重要。虽然分枝定界法（Branch and Bound, BaB）已成为一种完整的验证手段，但其效率问题显著。BaB 通过将验证问题自适应地划分为子问题（表示为一棵树），并对每个子问题应用现成的近似验证器，从而进行操作。

本研究识别出的核心低效之处在于现有 BaB 方法如何定位判定边界（verdict boundary）。判定边界是树路径上验证状态发生转变的点：从“未验证”（近似误差 $\hat{p} < 0$ ）转变为“已验证”（近似误差 $\hat{p} > 0$ ）。由于沿路径 $\hat{p}$ 具有近乎单调的特性（随着问题拆分，近似误差逐渐减小），边界之前的节点为未验证状态，而边界之后的节点为已验证状态。

现有方法（如 $\alpha\beta$ -Crown）沿着每条路径执行线性搜索，即逐个访问节点以寻找该边界。这需要在每个被访问的节点上进行代价高昂的边界传播，即使这些节点显然是未验证或已验证的，也会导致冗余的计算开销。

方法论

作者提出了 BMiner，这是一个全新的验证框架，它将寻找判定边界的任务重新表述为在近乎有序数组中的搜索问题。BMiner 不再逐个访问节点，而是利用 $\hat{p}$ 的单调性来跳过不必要的子问题。该框架引入了两种不同的搜索策略：

1. 指数搜索 (BMinerE)

BMinerE 借鉴经典的指数搜索算法，通过两个阶段来定位判定边界：

范围识别： 从当前节点开始，算法通过指数级增加规模的方式滑动并扩展搜索范围，以快速识别出一个包含边界点的区间 $[i_l, i_r]$ 。
二分搜索： 一旦确定了范围，就在 $[i_l, i_r]$ 内进行二分搜索，以精确锁定边界位置。
与线性搜索相比，这种方法显著减少了节点访问次数，尤其是在边界并未位于长路径末端的情况下。

2. 基于梯度的搜索 (BMinerG)

BMinerG 通过利用来自验证器评估（ $\hat{p}$ ）的定量信息，更精确地估计边界位置，从而进一步优化过程。

梯度估计： 算法将绝对值 $|\hat{p}|$ 视为目标函数，并利用先前访问过的节点来估计沿路径的“梯度”（变化率）。
位置估计： 基于估计的梯度，算法估算 $\hat{p}$ 穿过零点的可能位置。它会检查该估计节点，并迭代地更新梯度信息。
精炼： 该过程比指数搜索更积极地缩小搜索范围 $[i_l, i_r]$ ，然后再应用最终的二分搜索。该方法旨在通过基于近似改进速率来估计边界位置，从而最大限度地减少节点访问。

两种方法都采用了并扩展了最先进的 ReLU 选择策略（例如 FSB），以便与现有框架集成。具体而言，选择启发式算法被扩展为同时选择用于拆分的 Top- $k$ 个神经元，其中 $k$ 对应于搜索方法跳过的神经元数量。然而，搜索过程本身是通过沿着路径顺序检查节点来识别边界，而不是在单个步骤中同时拆分多个激活函数。

核心贡献

判定边界形式化： 本文将 BaB 验证过程形式化为在近乎单调的树路径中寻找判定边界的过程，指出现有的线性搜索策略是次优的。
BMiner 框架： 引入了两种新型搜索算法（指数搜索和基于梯度的搜索），能够跳过与边界无关的子问题，从而减少对高代价近似验证器的调用。
处理非单调性： 作者通过实验证明，尽管最近的 BaB 实现（如 $\alpha\beta$ -Crown）可能会表现出 $\hat{p}$ 的局部非单调性，但这些违反情况很少见，且不会显著影响所提搜索策略的整体有效性。
集成性： 该方法采用了并扩展了最先进的 ReLU 选择策略，使其能够与当前的尖端工具集成。

实验结果

作者在五个神经网络模型（MNISTL2, MNISTL4, OVAL21BASE, OVAL21WIDE, OVAL21DEEP）以及 MNIST 和 CIFAR-10 数据集上，对 500 个验证实例进行了 BMiner 的评估。他们将 BMinerE 和 BMinerG 与 $\alpha\beta$ -Crown（VNN-COMP 的获胜者）以及 Oliva 进行了对比。

验证能力： BMinerE 和 BMinerG 在认证实例数量上与 $\alpha\beta$ -Crown 持平或略有超越，同时在认证能力上始终优于 Oliva（尽管 Oliva 在证伪方面仍然更强）。
时间效率：
- BMinerG 取得了最显著的改进，在所有模型中将平均验证时间降低了 17.0% 至 29.2%，在五个神经网络中的最大降幅达到 44.7%。
- BMinerE 提供了约 4% 的稳定平均改进。
- 在最坏情况下，由于初始估计过度越过边界导致的溯回（backtracking），激进的搜索策略偶尔会引入额外开销（最高约 16.7%）。
非单调性的影响： 分析表明，即使在非单调路径上，BMinerE 和 BMinerG 的性能也保持稳定一致，证实了单调性的局部违反不会阻碍该方法的有效性。
机制分析： 性能提升归功于这些方法高效处理长路径的能力。尤其是 BMinerG，在处理长路径（长度 16–40）时表现出卓越的效率，其节点访问次数显著少于 BMinerE 和基准方法（例如 6.3 次对比 11.2 次）。

重要性与主张

本文声称，通过将验证过程重新定义为边界挖掘问题，可以在不牺牲完整性的情况下大幅降低基于 BaB 验证的计算成本。作者强调，其方法并非要取代近似验证器，而是对围绕它们的搜索策略进行的优化。

其重要性在于实现了 17%–30% 的平均验证时间缩减，这解决了神经网络形式化验证中的主要瓶颈。作者谦虚地指出，虽然目前的实现使用的是基于 CPU 的执行，但未来的工作可以通过 GPU 并行化和元启发式证伪来进一步提高效率。他们也承认，目前的 ReLU 选择策略是现有方法的扩展，将设计具备预测能力的全新选择启发式算法作为未来的研究方向。