Deep Neural Networks (DNNs) have emerged as an effective approach to tackling real-world problems. However, like human-written software, automatically-generated DNNs can have bugs and be attacked. This thus attracts many recent interests in developing effective and scalable DNN verification techniques and tools. In this work, we introduce a NeuralSAT, a new constraint solving approach to DNN verification. The design of NeuralSAT follows the DPLL(T) algorithm used modern SMT solving, which includes (conflict) clause learning, abstraction, and theory solving, and thus NeuralSAT can be considered as an SMT framework for DNNs. Preliminary results show that the NeuralSAT prototype is competitive to the state-of-the-art. We hope, with proper optimization and engineering, NeuralSAT will carry the power and success of modern SAT/SMT solvers to DNN verification. NeuralSAT is avaliable from: https://github.com/dynaroars/neuralsat-solver

翻译：深度神经网络（DNN）已成为解决现实问题的有效途径。然而，如同人工编写的软件一样，自动生成的DNN可能存在缺陷并易受攻击。这促使近年来在开发高效可扩展的DNN验证技术与工具方面涌现了大量研究兴趣。本文提出NeuralSAT——一种面向DNN验证的新型约束求解方法。NeuralSAT的设计遵循现代可满足性模理论（SMT）求解中使用的DPLL(T)算法，涵盖（冲突）子句学习、抽象化与理论求解，因此可将其视为面向DNN的SMT求解框架。初步结果表明，NeuralSAT原型系统已具备与现有最优方法竞争的能力。我们期望，通过适当的优化与工程开发，NeuralSAT能够将现代SAT/SMT求解器的效能与成功经验引入DNN验证领域。NeuralSAT代码可从以下地址获取：https://github.com/dynaroars/neuralsat-solver