A DPLL(T) Framework for Verifying Deep Neural Networks
This addresses the need for reliable verification of DNNs, which are prone to bugs and attacks, but it appears incremental as it builds on existing SMT solver techniques.
The authors tackled the problem of verifying deep neural networks (DNNs) by introducing NeuralSAT, a new verification approach that adapts the DPLL(T) algorithm from SMT solvers, resulting in demonstrated benefits on challenging benchmarks.
Deep Neural Networks (DNNs) have emerged as an effective approach to tackling real-world problems. However, like human-written software, DNNs can have bugs and can be attacked. To address this, research has explored a wide-range of algorithmic approaches to verify DNN behavior. In this work, we introduce NeuralSAT, a new verification approach that adapts the widely-used DPLL(T) algorithm used in modern SMT solvers. A key feature of SMT solvers is the use of conflict clause learning and search restart to scale verification. Unlike prior DNN verification approaches, NeuralSAT combines an abstraction-based deductive theory solver with clause learning and an evaluation clearly demonstrates the benefits of the approach on a set of challenging verification benchmarks.