Incremental Neural Network Verification via Learned Conflicts

As deep neural networks (DNNs) are increasingly applied in safety-critical applications such as autonomous driving, medical diagnosis, and aerospace systems, ensuring their reliability and safety becomes crucial. Despite their strong empirical performance in tasks such as control and image recognition, the complexity and opacity of neural networks make it difficult to ensure their reliability and safety in these critical settings. To address this issue, numerous neural network verification methods have been proposed, aiming to provide rigorous guarantees about network behavior. However, for networks with piecewise-linear activation functions, such as ReLUs, the verification problem is NP-complete, which hinders scalability. As neural networks are adopted across increasingly diverse and high-stakes domains, the demand for scalable verification techniques continues to grow. Therefore, improving the efficiency of neural network verification is imperative.

In practice, DNN verification is often not performed as a single, isolated query, but rather invoked repeatedly within larger analysis procedures. For example, in formal explainability, verification queries are issued repeatedly to reason about the contribution of different input features to a given prediction under progressively refined constraints; similarly, in robustness radius computation, verification queries are invoked iteratively to narrow down the maximum safe perturbation radius around a given input. Such analyses naturally give rise to sequences of closely related verification queries that differ in limited aspects of their specifications, such as refined input domains or strengthened output constraints. Despite this, current verification tools do not explicitly exploit this structural similarity: each query is restarted from scratch, and information derived during previous runs is discarded.

This paper proposes an incremental verification technique that accelerates the neural network verification process by reusing learned conflicts. This technique can be integrated into 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 develop a framework for conflict recording and sound reuse that integrates directly with branch-and-bound-based verifiers and employ a SAT solver to efficiently manage and apply large collections of learned conflicts during solving.

• �� Incremental Verification Framework: Records conflicts that arise during branch-and-bound verification, where each conflict captures an infeasible combination of branching decisions.
• �� Conflict Retention: These conflicts are preserved beyond individual verification runs and reused in subsequent queries with refined specifications.
• �� Conflict Inheritance: We formally define a refinement condition for the conflict to remain valid and show that this condition can be established in several important applications of neural network verification.
• �� SAT Solver Usage: During branch-and-bound search, a SAT solver is used to reason about inherited conflict clauses as an additional pruning and propagation step.
• �� Implementation: The proposed method is implemented in the Marabou verifier and evaluated on three representative verification tasks.

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. In the local robustness radius determination task, we conducted experiments on the MNIST dataset, and the results show that the incremental method achieved an average solving time 1.3x faster than the non-incremental method. In the verification with input splitting task, the incremental method effectively reduced verification time during the training of Lyapunov neural certificates. We used the CaDiCaL SAT solver for conflict reasoning, and all verification queries induced by the same task share a single ICA instance. Propagation from inherited conflicts may detect that the current partial assignment is infeasible, allowing the verifier to prune the subproblem immediately, or it may derive additional ReLU phase assignments via unit propagation.

Experimental results show that incremental conflict reuse reduces verification effort and yields speedups of up to 1.9x over a non-incremental baseline across three verification tasks. In the local robustness radius determination task, the incremental method achieved an average solving time 1.3x faster than the non-incremental method on the MNIST dataset. In the verification with input splitting task, the incremental method effectively reduced verification time during the training of Lyapunov neural certificates. Propagation from inherited conflicts may detect that the current partial assignment is infeasible, allowing the verifier to prune the subproblem immediately, or it may derive additional ReLU phase assignments via unit propagation.

The proposed incremental verification technique can be directly applied to neural network models requiring efficient verification, especially in safety-critical applications such as autonomous driving and medical diagnosis. By reducing redundant computation, this technique can significantly improve verification efficiency and reduce computational costs. Additionally, this technique can be used in other scenarios requiring multiple verifications, such as model optimization and tuning.

Despite the impressive performance of the proposed incremental verification technique across multiple verification tasks, it may encounter memory limitations when dealing with very large-scale neural networks, as it requires storing a large amount of conflict information. Additionally, the effectiveness of conflict reuse may not meet expectations for certain types of neural network architectures. In some cases, the inheritance of conflicts may lead to additional computational overhead. Future research directions include exploring how to implement incremental verification techniques on larger-scale neural networks and how to apply this technique to other types of neural network architectures.