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.

翻译：深度神经网络（DNN）已成为解决现实问题的有效方法。然而，与人类编写的软件类似，DNN也可能存在缺陷并遭受攻击。为解决这一问题，研究者们探索了多种验证DNN行为的算法方法。本文提出了一种新的验证方法NeuralSAT，该方法适配了现代SMT求解器中广泛使用的DPLL(T)算法。SMT求解器的一个关键特性在于通过冲突子句学习与搜索重启来扩展验证规模。与以往的DNN验证方法不同，NeuralSAT将基于抽象演绎的理论求解器与子句学习相结合，实验评估结果清晰证明了该方法在一组具有挑战性的验证基准测试中的优势。