arXiv:2603.12232cs.LOcs.AI2026-03被引 1

通过复用验证过程中的冲突信息,加速神经网络验证。

Incremental Neural Network Verification via Learned Conflicts

  • 基于分支定界法,记录并复用不同查询间的不可行激活组合冲突。
  • 在三个任务中实现最高1.9倍的加速,减少重复搜索开销。
  • 适合需要连续验证多个相关查询的场景,如鲁棒性分析与特征提取。

神经网络验证常作为大型分析流程的核心组件,需对同一网络生成一系列紧密相关的验证查询。现有验证器通常独立求解每个查询,忽略先前运行中获得的信息,导致反复探索相同的不可行搜索区域。本文提出一种增量验证技术,通过跨查询复用已学习的冲突信息来减少冗余。该方法可集成于任意基于分支定界法的验证器中。在验证过程中,系统记录与不可行激活状态组合相关的冲突,并在多次运行间保留。我们形式化了验证查询间的细化关系,证明针对某查询学习的冲突在查询细化后依然有效,支持安全的冲突继承。继承的冲突由SAT求解器进行一致性检查与传播,可在搜索早期识别并剪枝不可行子问题。我们在Marabou验证器中实现该技术,并在局部鲁棒性半径计算、输入分割验证和最小必要特征集提取三个任务上进行评估。实验表明,增量冲突复用显著降低验证开销,相比非增量基线最高提速1.9倍。

原文摘要 · Abstract (English)

Neural network verification is often used as a core component within larger analysis procedures, which generate sequences of closely related verification queries over the same network. In existing neural network verifiers, each query is typically solved independently, and information learned during previous runs is discarded, leading to repeated exploration of the same infeasible regions of the search space. In this work, we aim to expedite verification by reducing this redundancy. We propose an incremental verification technique that reuses learned conflicts across related verification queries. The technique can be added on top of any branch-and-bound-based neural network verifier. During verification, the verifier records conflicts corresponding to learned infeasible combinations of activation phases, and retains them across runs. We formalize a refinement relation between verification queries and show that conflicts learned for a query remain valid under refinement, enabling sound conflict inheritance. Inherited conflicts are handled using a SAT solver to perform consistency checks and propagation, allowing infeasible subproblems to be detected and pruned early during search. We implement the proposed technique in the Marabou verifier and evaluate it on three verification tasks: local robustness radius determination, verification with input splitting, and minimal sufficient feature set extraction. Our experiments show that incremental conflict reuse reduces verification effort and yields speedups of up to $1.9\times$ over a non-incremental baseline.

神经网络验证增量推理冲突复用分支定界

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。