Proof-Driven Clause Learning in Neural Network Verification
This work addresses the critical need for efficient safety verification of DNNs, which is essential for their widespread adoption, though it is incremental as it builds on existing SAT/SMT solving techniques.
The paper tackles the scalability problem in deep neural network (DNN) safety verification by proposing a proof-driven clause learning approach based on Conflict-Driven Clause Learning (CDCL), achieving a 2X--3X improvement over similar methods and outperforming state-of-the-art in specific cases.
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.