Proof-Driven Clause Learning in Neural Network Verification

TL;DR

This work tackles the scalability barrier in safety verification for large DNNs by introducing a Conflict-Driven Clause Learning (CDCL) approach that derives conflict clauses from UNSAT proofs to prune the search space. It formulates DNN verification within a DPLL($\mathcal{T}$) framework, using a Boolean abstraction of neuron activations and a theory solver for linear constraints, enabling modular SAT/theory solving and proof production. The authors present a novel UNSAT-proof–driven algorithm to extract effective conflict clauses, implement it atop the IPASIR-UP interface, and evaluate it on diverse benchmarks, achieving 2x–3x improvements over a similar approach and, in some cases, surpassing state-of-the-art verifiers. The results suggest that integrating proof-based CDCL with DNN verifiers can substantially enhance scalability and opens avenues for combining CDCL with other optimization techniques for even larger networks in safety-critical contexts.

Abstract

The widespread adoption of deep neural networks (DNNs) requires efficient techniques for safety verification. Existing methods struggle to scale to real-world DNNs, and tremendous efforts are being put into improving their scalability. In this work, we propose an approach for improving the scalability of DNN verifiers using Conflict-Driven Clause Learning (CDCL) -- an approach that has proven highly successful in SAT and SMT solving. We present a novel algorithm for deriving conflict clauses using UNSAT proofs, and propose several optimizations for expediting it. Our approach allows a modular integration of SAT solvers and DNN verifiers, and we implement it on top of an interface designed for this purpose. The evaluation of our implementation over several benchmarks suggests a 2X--3X improvement over a similar approach, with specific cases outperforming the state of the art.