通过学习冲突进行增量神经网络验证
Incremental Neural Network Verification via Learned Conflicts
AI总结：
本文提出了一种基于冲突继承的增量神经网络验证方法，通过重用学习的冲突信息提升验证效率，实验显示在三个任务中实现了高达1.9倍的加速。
摘要：
神经网络验证常作为更大分析过程中的核心组件，生成同一网络上的相关验证查询序列。在现有神经网络验证器中，每个查询通常独立解决，先前运行中学习的信息被丢弃，导致重复探索搜索空间中的不可行区域。在本工作中，我们旨在通过减少这种冗余来加快验证。我们提出了一种增量验证技术，该技术可以在相关验证查询之间重用学习的冲突。该技术可以添加在任何基于分支限界法的神经网络验证器之上。在验证过程中，验证器记录与学习的不可行激活阶段组合相对应的冲突，并在多次运行中保留它们。我们正式定义了验证查询之间的细化关系，并表明为查询学习的冲突在细化下仍然有效，从而实现声音的冲突继承。继承的冲突通过SAT求解器进行一致性检查和传播，允许在搜索过程中早期检测并修剪不可行的子问题。我们将在Marabou验证器中实现所提出的技术，并在三个验证任务上进行评估：局部鲁棒半径确定、输入分割验证以及最小充分特征集提取。我们的实验表明，增量冲突重用减少了验证工作量，并在非增量基线上实现了高达1.9倍的加速。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
