🤖 machine learning

Lookahead Branching for Neural Network Verification

本文介绍了一种用于神经网络验证的通用前瞻分支策略，该策略通过改进分支决策和生成额外的引理来增强现有的分支定界验证器，从而实现了持续的加速，并使解决的实例数量最多增加了 57%。

原作者： Liam Davis, Duo Zhou, Huan Zhang, Guy Katz, Clark Barrett, Haoze Wu

发布于 2026-07-21

📖 1 分钟阅读☕ 轻松阅读

原作者： Liam Davis, Duo Zhou, Huan Zhang, Guy Katz, Clark Barrett, Haoze Wu

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

想象一个这样的世界：我们汽车、医疗设备和安防系统的“大脑”是由被称为神经网络的巨大且复杂的数学网络构成的。这些数字大脑在识别面部或预测天气方面表现得极其出色，但它们也以难以理解而著称。因为它们是通过在数据中寻找模式而非遵循严格的既定规则来学习的，所以很难确定它们在情况变得诡异时是否会犯错。这是一个重大的安全问题：如果一辆自动驾驶汽车的大脑做出了错误的判断，人们可能会受伤。因此，一群科学家一直在研究一种方法，通过数学手段来证明这些网络无论接收到什么输入，都能始终表现正确。你可以把这个过程想象成一名侦探正在试图通过检查每一个可能的线索来破解一个巨大的谜团。这位侦探必须将谜团拆解成越来越小的部分，逐一检查每个部分是会导致矛盾（即“漏洞”）还是会导致安全的结果。挑战在于，由于可能的线索实在太多，如果一个一个地检查，耗费的时间将比宇宙的年龄还要长。侦探需要一种聪明的策略来决定下一步该检查哪个线索，希望其中一个选择能快速解开整个谜题。

这篇论文为那位侦探介绍了一种聪明的策略，叫做“前瞻分支”（Lookahead Branching）。研究人员在使用两种不同类型的验证工具（一种称为 Marabou，另一种称为 α-β-CROWN）进行工作时发现，与其仅仅根据当前的状况来猜测下一步该检查哪个线索，不如停下来模拟未来几步会发生的情况。想象一下你在下国际象棋。一个普通的棋手可能会观察棋盘并选择当前看起来最好的走法。但一位特级大师可能会想：“如果我走这里，我的对手就会走那里，然后我可以走那里……”作者建议，神经网络验证器也应该这样做：在做出决策之前，它们应该简要地“梦见”如果采取不同的路径会发生什么。他们发现，通过花费一点额外的时间来模拟这些未来的步骤，验证器可以做出更好的选择，从而实现更快的求解速度并解决更多的难题。在测试中，这种方法帮助工具多解决了高达 57% 的实例，并且在处理最难的问题时显著提高了速度。

该论文的核心在于如何高效地进行这种“梦境”模拟。研究人员创建了一个通用的配方，可以添加到任何这类验证工具中。这个过程是这样运作的：当工具需要拆分一个问题时，它并不仅仅选择一个选项。相反，它会挑选几个有潜力的候选方案，并模拟对每一个方案进行拆分后的情况。它会向后看几步（即“前瞻深度”），以观察问题会如何变化。如果一次拆分导致许多其他混乱的部分突然变得清晰（例如，一个原本“不稳定”的神经元突然变得“固定”了），那么这次拆分就会获得高分。随后，工具会选择得分最高的那个拆分方案。

作者还发现，这种模拟不仅仅是为了挑选最佳路径；它实际上可以发现新的事实。有时，通过模拟一次拆分，工具会意识到神经网络的某个部分必须处于特定的状态，甚至在它正式进行该拆分之前就已经意识到了这一点。这使得工具能够立即“固定”这些部分的网络，从而省去了大量不必要的重复工作。论文表明，这种方法在两种完全不同类型的验证工具上都表现良好：一种是在标准计算机处理器上运行的（Marabou），另一种是使用强大的图形处理器的（α-β-CROWN）。

在实验中，团队在各种神经网络上测试了这种方法，从识别手写数字的简单网络到用于计算机视觉的复杂网络。在使用 Marabou 工具时，使用前瞻技术有助于解决更多问题，并缩短了处理困难案例所需的时间。例如，在名为 NN4Sys 的特定基准测试集上，使用前瞻技术的工具比不使用时解决了更多的实例。在以速度快著称的 α-β-CROWN 工具上，前瞻策略仍然成功实现了求解时间的加速，并解决了一些标准方法未能处理的额外问题。研究人员指出，虽然前瞻过程在设置时会消耗一点额外的计算时间，但回报是巨大的，因为它防止了工具在稍后阶段浪费时间在错误的路径上。

然而，论文谨慎地指出，这并不是一个能瞬间解决一切的“万灵药”。“前瞻”过程在计算上是昂贵的，这意味着它需要更多的计算能力来思考未来。作者发现，当它被用于搜索的最开始阶段时效果最好，因为那里的决策对未来的影响最大。如果你尝试在每一个步骤都使用它，思考未来的成本可能会超过其带来的收益。他们还测试了不同的前瞻设置方式，例如前瞻多少步以及模拟多少个候选方案，并发现中等深度（向后看两步）在处理最难的问题时效果最好。

论文明确反对了“我们应该只使用快速的局部信息来做决策”这一观点。虽然快速的启发式算法（经验法则）在速度上有优势，但它们往往会忽略大局，并可能导致验证器陷入死胡同。作者展示了通过投入更多的努力来模拟拆分的后果，整个验证过程会变得更加高效。他们还澄清，他们的方法不同于使用人工智能来学习如何进行分支；他们的做法不是利用人工智能模型在过去的数据上进行训练，而是利用数学模拟在实时情况下找出最佳移动。

最终，论文表明，“前瞻分支”是一种强大的通用策略，可以植入不同的验证工具中，使它们变得更聪明、更快速。它并不是要取代现有的工具，而是增强它们，使其能够更有信心地应对更困难的安全关键型问题。研究结果表明，对于最困难的验证任务，花费时间进行前瞻是值得的额外计算成本，这能带来一种更稳健、更可靠的方式，来确保我们的 AI 系统是安全的。

技术摘要：用于神经网络验证的前瞻分支策略

问题陈述

深度神经网络（DNN）正越来越多地部署在安全至关重要的领域，这使得需要可扩展的形式化验证技术来推理其行为。最先进的完备验证工具依赖于**分支定界（Branch-and-Bound, BaB）**框架。这种方法涉及对非线性激活函数（如 ReLU）进行递归拆分，并使用不完备的验证器分析生成的子问题。

BaB 的效率在很大程度上取决于分支启发式算法（branching heuristic），即用于选择下一个待拆分的不稳定神经元的策略。较差的选择，特别是在搜索树顶部的决策，会导致重复的验证工作并增加运行时间。虽然最近的启发式算法如**过滤智能分支（Filtered Smart Branching, FSB）**通过模拟单层分支提高了性能，但它们往往无法捕捉跨越多个搜索树层级的决策级联效应。大多数现有方法通过利用局部信息（如变量边界）来优先考虑速度，而没有评估长期影响，从而增加了无效分支的风险。

方法论

作者提出了一种通用的**前瞻分支（Lookahead Branching）**策略，该策略改编自形式化方法（SAT/SMT）和混合整数线性规划（MILP），旨在系统地改进分支决策。其核心思想是通过模拟潜在的候选神经元拆分，在提交决策之前衡量其下游影响。

前瞻模板

作者提出了一个带有若干可调参数的模板算法（算法 1）：

预选策略（Preselect Strategy）： 为了减轻计算开销，会选择一部分不稳定神经元进行模拟。策略包括：
- 基于极性的（Polarity-based）： 根据边界敏感性选择激活状态最不确定的神经元（用于 Marabou）。
- 基于评分的（Score-based）： 根据现有的启发式算法（如 BaBSR）选择排名靠前的神经元（用于 $\alpha$ - $\beta$ -CROWN）。
前瞻深度 ( $d$ )： 模拟递归拆分的次数。作者研究了深度为 2 的前瞻，特别是在搜索树顶部，这受到了 MILP 中强分支（strong branching）文献的启发。
评分函数： 用于评估模拟分支质量的指标：
- 基于神经元固定（Neuron-fixing-based）： 计算在边界传播后，有多少先前不稳定的神经元变为相位固定（激活或不激活）状态。它倾向于选择能使两个分支中都有许多神经元被固定的平衡拆分。
- 基于边界缩减（Bound-reduction-based）： 衡量变量边界的缩减程度或与决策阈值的接近程度。
相位固定（Phase Fixing）： 前瞻的一个关键结果是能够收紧变量边界。如果一个模拟拆分保证了某个神经元的边界严格大于零或小于零，则该神经元的相位被“固定”。这些发现可用于导出有效的引理并剪枝搜索空间。

具体实现

该方法在两种不同的 BaB 验证器中进行了实例化：

Marabou： 一种基于 CPU 的 SMT 验证器。作者使用了基于极性的预选策略、深度为 2 的前瞻以及神经元固定指标。此处启用了相位固定。
$\alpha$ - $\beta$ -CROWN： 一种基于 GPU 加速的边界传播验证器。作者使用 BaBSR 进行预选、深度为 2 的前瞻以及基于边界缩减的指标。在此实例化中未使用相位固定，因为 $\alpha$ -CROWN 中的自适应 ReLU 规则可能会在预激活边界收紧时导致边界放宽，使得相位固定逻辑在此上下文中是不健全的。

核心贡献

通用框架： 论文定义了一个通用的配方，可以将前瞻集成到任何分支定界验证器中，并对预选、深度和评估指标进行了参数化。
统一 FSB： 作者证明了当前的先进启发式算法——过滤智能分支（FSB），可以被视为前瞻策略的一个特例实例化（具体为以 BaBSR 为基础启发式的深度-1 前瞻）。
引理生成： 除了改进分支决策外，前瞻过程还能生成额外的信息（收紧后的边界），这些信息可用于导出有效的引理，从而进一步剪枝搜索空间。
实证验证： 该方法在两种截然不同的求解器范式（基于 SMT 和基于 GPU 边界传播）中进行了实现和评估，展示了广泛的适用性。

结果

作者在多个基准测试（NAP, NN4Sys, MNIST, CIFAR, TinyImageNet）上将前瞻分支与现有启发式算法（BaBSR, Pseudo-Impact, FSB）进行了对比评估。

Marabou： 前瞻分支显著增加了 BaBSR 和 Pseudo-Impact 启发式算法解决的实例数量。在 NAP 基准测试中，前瞻比 BaBSR 多解决了高达 47 个实例（BaBSR 为 30 个）。虽然开销可能会减慢简单实例的速度，但改进的分支质量在困难实例上占据主导地位，从而实现了显著的加速。
$\alpha$ - $\beta$ -CROWN： 前瞻在性能上持续优于 FSB。在需要完整 BaB 的 UNSAT 实例中，前瞻实现了 15.4% 至 24.3% 的加速，并解决了 FSB 无法解决的独特实例。
总体而言： 集成前瞻导致了验证时间的持续加速，并在所评估的工具中提升了高达 57% 的已解决实例数量。

意义与主张

论文声称前瞻分支是增强完备神经网络验证性能的一种具有普遍适用性的策略。通过在关键分支决策（特别是搜索树顶部）中投入额外的计算，该方法捕捉到了局部启发式算法所忽略的级联效应。

作者将这项工作定位为对一种通用分支策略的系统性研究，该策略超越了基于局部信息的“快速”决策。他们指出，虽然设计空间非常广阔（包括更深的模拟或在搜索后期进行周期性调用），但他们目前的结果表明，即使是有限的前瞻（深度-2）也能产生显著的性能增益。这项工作也补充了学习型启发式算法，后者可以作为前瞻模板中的预选策略。

论文总结道，前瞻分支有效地改进了包括 SMT 和 GPU 加速在内的验证器，这表明它是减少验证时间并增加安全关键型 DNN 可解实例数量的一种鲁棒技术。