Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Incremental Neural Network Verification via Learned Conflicts

Raya Elsaleh, Liam Davis, Haoze Wu, Guy Katz

Abstract

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.

Incremental Neural Network Verification via Learned Conflicts

Abstract

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 over a non-incremental baseline.
Paper Structure (49 sections, 7 theorems, 9 equations, 5 figures, 3 tables, 5 algorithms)

This paper contains 49 sections, 7 theorems, 9 equations, 5 figures, 3 tables, 5 algorithms.

Table of Contents

  1. Introduction
  2. Background
  3. Neural Networks and the Verification Problem
  4. Neural Networks.
  5. Verification Queries.
  6. Branch-and-Bound Verification
  7. Case Splitting.
  8. Branch-and-Bound Search and Search Tree.
  9. Bound Propagation.
  10. Incremental Verification via Learned Conflicts
  11. Conflicts and Query Refinement
  12. Learned Conflicts.
  13. Query Refinement.
  14. Soundness of Conflict Reuse
  15. Using Conflicts during Verification
  16. ...and 34 more sections

Key Result

lemma 1

Let $q_1$ and $q_2$ be verification queries such that $q_2 \preceq q_1$, and let $\{\ell_1,\ldots,\ell_k\}$ be a set of literals. If the subproblem is infeasible, then the subproblem is also infeasible.

Figures (5)

  • Figure 1: Branch-and-bound search tree over ReLU phase decisions.
  • Figure 2: Incremental vs. non-incremental for robustness radius determination.
  • Figure 3: Incremental vs. non-incremental for input splitting.
  • Figure 4: Minimal sufficient feature set visualizations for GTSRB inputs. Pixels not included in the explanation are shown in gray.
  • Figure 5: Incremental vs. non-incremental explanation size over time.

Theorems & Definitions (18)

  • definition 1: Conflict Clause
  • definition 2: Query Refinement
  • lemma 1: Monotonicity of Infeasibility Under Refinement
  • theorem 1: Sound Conflict Reuse under Refinement
  • lemma 2: Soundness of SAT-Based Pruning
  • lemma 3: Soundness of SAT-Based Implied Assignments
  • definition 3: Local Robustness Radius
  • proposition 1: Robustness Query Refinement
  • proposition 2: Input Splits are Refinements
  • definition 4: Minimal Sufficient Feature Set
  • ...and 8 more