A DPLL(T) Framework for Verifying Deep Neural Networks

• DOI: 10.48550/arxiv.2307.10266
• Publication Date: 2023-01-01
• Authors: Duong, Hai; Nguyen, ThanhVu; Dwyer, Matthew
• Keywords: Software Engineering (cs.SE); FOS: Computer and information sciences; Computer Science - Machine Learning; Computer Science - Logic in Computer Science; Computer Science - Software Engineering; Machine Learning (cs.LG); Logic in Computer Science (cs.LO)

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.<br/>NeuralSAT is avaliable at: https://github.com/dynaroars/neuralsat<br/>