Incremental Neural Network Verification via Learned Conflicts

This paper proposes an incremental neural network verification technique that reuses learned conflicts across related queries via a SAT solver to prune infeasible search spaces early, achieving speedups of up to 1.9x over non-incremental baselines.

The Gist

Imagine you are a detective trying to solve a massive, complex mystery: Is this AI safe?

To answer this, you have to check if the AI can ever make a dangerous mistake (like a self-driving car ignoring a stop sign). Because AI is so complicated, you can't just look at it once. You have to break the problem down into millions of tiny scenarios, checking them one by one. This process is called Neural Network Verification.

The Problem: The "Amnesiac" Detective

In the old way of doing this, the detective (the computer program) was like someone with amnesia.

• Scenario A: The detective checks if the car crashes if a pedestrian is 5 meters away. They spend hours checking every angle and conclude, "No crash possible here." They write this down, but then immediately throw the notes in the trash.
• Scenario B: The detective checks if the car crashes if a pedestrian is 4 meters away. This is a stricter rule (closer distance), so it's harder to prove safety. The detective starts from scratch, re-checking all the angles they already checked in Scenario A. They waste hours re-discovering that "No crash possible here" again.

This is inefficient. It's like re-reading the same chapter of a book every time you want to know what happens next, even though you already know the plot.

The Solution: The "Smart Notebook"

This paper introduces a new method called Incremental Verification via Learned Conflicts.

Think of this as giving the detective a Smart Notebook that remembers every dead end they've ever hit.

1. The "Conflict": When the detective realizes a specific combination of clues leads to a contradiction (e.g., "If the pedestrian is here AND the car is going that fast, it's impossible to stop"), they call this a Conflict. It's a "Do Not Enter" sign for that specific path.
2. The Notebook: Instead of throwing the notes away, the detective writes the "Do Not Enter" sign in the Smart Notebook.
3. The Refinement: When the detective moves to the next, stricter scenario (like the 4-meter distance), they open the notebook. They see the old "Do Not Enter" signs. Since the new scenario is just a tighter version of the old one, those old signs still apply!
4. The Result: The detective can instantly skip millions of dead-end paths they already know are impossible. They only have to explore the new, uncharted territory.

How It Works in Real Life (The Three Test Cases)

The authors tested this "Smart Notebook" on three different types of AI safety checks:

1. The "Safety Bubble" (Robustness Radius):

   • The Task: How close can a pedestrian get before the AI might crash?
   • The Analogy: Imagine testing a bubble. You test a huge bubble (10 meters), then a smaller one (9 meters), then 8 meters.
   • The Win: When you shrink the bubble, you don't need to re-test the outside edges you already proved were safe. The notebook remembers them. Result: 1.35x faster.

2. The "Divide and Conquer" (Input Splitting):

   • The Task: The problem is too big to solve at once, so you chop the input space into tiny pieces (like slicing a pizza) and check each slice.
   • The Analogy: If you slice a pizza and realize the crust on the left slice is burnt (a conflict), you know the whole left side is bad. When you slice the left side again into smaller pieces, you don't need to check the burnt crust again. The notebook remembers the "burnt" status.
   • The Win: This saved the most time because the detective could skip huge chunks of the pizza. Result: 1.9x faster (almost double the speed!).

3. The "Essential Ingredients" (Feature Extraction):

   • The Task: What is the minimum amount of information the AI needs to make a decision? (e.g., Does it need to see the whole stop sign, or just the red octagon shape?)
   • The Analogy: You are trying to find the secret ingredient in a soup. You taste the soup with all ingredients, then remove one, then remove another. If you realize "Salt" is the only thing that makes it taste bad, you write that down. Next time you try a slightly different soup, you already know "Salt" is the problem, so you don't waste time tasting it again.
   • The Win: It didn't just make it faster; it helped the detective find the answer sooner if they had to stop early.

The Bottom Line

The paper proves that by simply remembering what didn't work in previous, similar tests, we can make AI safety checks nearly twice as fast.

It's the difference between a detective who forgets everything after every case and a detective who keeps a detailed case file. The second detective solves crimes much faster because they don't waste time re-solving the same dead ends.

In short: Don't reinvent the wheel. If you already proved a path is a dead end, write it down and skip it next time. This makes AI safer and faster to verify.

Technical Summary

1. Problem Statement

Neural network verification is a critical component for ensuring the safety and reliability of Deep Neural Networks (DNNs) in safety-critical domains (e.g., autonomous driving, aerospace). The verification problem for networks with piecewise-linear activations (like ReLU) is NP-complete.

In practice, verification is rarely a single, isolated query. Instead, it is often embedded within larger analysis procedures that generate sequences of closely related verification queries over the same network. Examples include:

• Robustness Radius Computation: Iteratively narrowing the search for the maximum safe perturbation radius.
• Input Splitting (Divide-and-Conquer): Recursively partitioning the input space to verify difficult properties.
• Formal Explainability: Iteratively refining constraints to identify minimal sufficient feature sets.

The Core Issue: Existing neural network verifiers (typically based on Branch-and-Bound) treat each query independently. They discard all information learned during previous runs. This leads to redundant exploration of the same infeasible regions of the search space, significantly hindering scalability and efficiency.

2. Methodology

The authors propose an incremental verification framework that reuses "learned conflicts" (lemmas) across related verification queries. The approach is designed to be a lightweight extension that can be layered on top of any existing Branch-and-Bound-based verifier.

Key Concepts

• Conflict Clauses: During Branch-and-Bound search, when a subproblem is found to be infeasible (UNSAT), the specific combination of ReLU activation phase decisions (branching decisions) that led to this infeasibility is recorded as a conflict clause.
• Query Refinement: The framework formalizes a relationship between queries. A query $q_2$ is a refinement of $q_1$ ($q_2 \preceq q_1$) if they operate on the same network but $q_2$ has stricter constraints (i.e., a smaller input domain $X$ and/or output domain $Y$).
• Monotonicity of Infeasibility: The paper proves a critical lemma: If a set of branching decisions is infeasible under a loose constraint ($q_1$), it remains infeasible under a stricter constraint ($q_2$). Therefore, conflicts learned for $q_1$ are soundly reusable for $q_2$.

Technical Workflow

1. Conflict Recording: As the verifier explores the search tree, it records UNSAT nodes as conflict clauses (sets of literals representing infeasible phase combinations).
2. Inheritance: When a new, refined query begins, the verifier loads the conflict clauses learned from previous, related queries.
3. SAT-Based Reasoning: The system employs a SAT solver (specifically CaDiCaL in the implementation) to manage these conflicts.
   • Consistency Checks: At each node of the Branch-and-Bound tree, the current partial assignment of ReLU phases is asserted as assumptions in the SAT solver. If the SAT solver detects a conflict with the inherited clauses, the node is immediately pruned (UNSAT).
   • Propagation: If the SAT solver finds implied literals (unit propagation), these are added to the verifier's bounds, further restricting the search space without needing to explore the tree.
4. Integration: The method is implemented as an "Incremental Conflict Analyser" (ICA) component that interfaces with the main Branch-and-Bound loop (e.g., in the Marabou verifier).

3. Key Contributions

• Formalization of Refinement: The paper provides a formal definition of query refinement and proves the soundness of inheriting conflict clauses from a coarser query to a finer one.
• Solver-Agnostic Framework: The technique is designed to work with any Branch-and-Bound verifier. It separates the conflict management logic from the core numeric reasoning.
• SAT Integration: It introduces a novel method of using a SAT solver not just for the final verification, but as a dynamic pruning and propagation engine during the Branch-and-Bound search to handle learned conflicts efficiently.
• Implementation: The approach is implemented and integrated into the Marabou verifier, a state-of-the-art DNN verification tool.

4. Experimental Results

The authors evaluated the approach on three distinct verification tasks using the Marabou verifier and CaDiCaL SAT solver:

Use Case	Description	Speedup	Key Findings
Local Robustness Radius	Determining the maximum safe perturbation radius via binary search.	1.35×	Reduced average solving time from 315.6s to 233.5s. Successfully solved more inputs within the timeout.
Input Splitting	Recursive partitioning of the input space (Divide-and-Conquer).	1.92×	The most significant gain. Reduced time from 84.1s to 43.9s. Solved 491/491 tasks vs. 489/491 for the baseline.
Minimal Sufficient Feature Set	Extracting explanations by iteratively freeing features.	N/A (Anytime)	While final explanation size was similar, the incremental method achieved smaller explanations faster (better anytime behavior), reducing the time to find a valid explanation.

General Observations:

• The speedup correlates with the strength of the refinement relationship. Tasks with strict refinement chains (like input splitting) saw the highest gains.
• The overhead of recording and managing conflicts was negligible compared to the time saved by pruning infeasible regions.

5. Significance

• Scalability: This work addresses a major bottleneck in neural network verification: the inability to leverage information across iterative analysis steps. By reusing learned conflicts, it significantly reduces the computational cost of complex verification workflows.
• Practical Impact: The method enables the verification of larger or more complex properties that were previously intractable due to time constraints.
• Theoretical Foundation: It bridges the gap between incremental SAT/SMT solving (a mature field) and neural network verification, providing a sound theoretical basis for conflict inheritance in the context of Branch-and-Bound search.
• Future Directions: The paper suggests future work on minimizing conflict clauses (to reduce SAT overhead) and using conflicts to guide branching heuristics, further optimizing the search process.

In conclusion, the paper demonstrates that incremental conflict reuse is a highly effective strategy for accelerating neural network verification, particularly in scenarios involving iterative refinement of constraints, without compromising the soundness of the verification results.