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

翻译：深度神经网络（DNN）已成为解决现实问题的一种有效方法。然而，如同人类编写的软件一样，自动生成的DNN可能存在缺陷并遭受攻击。这促使近期研究界对开发有效且可扩展的DNN验证技术与工具产生了浓厚兴趣。本文提出NeuralSAT——一种用于DNN验证的新型约束求解方法。NeuralSAT的设计遵循现代SMT求解中使用的DPLL(T)算法，该算法包含（冲突）子句学习、抽象化和理论求解，因此NeuralSAT可被视为一种面向DNN的SMT框架。初步结果表明，NeuralSAT原型与现有最优方法相比具有竞争力。我们期望，通过适当的优化与工程实现，NeuralSAT能够将现代SAT/SMT求解器的强大能力与成功经验引入DNN验证领域。NeuralSAT可通过以下链接获取：https://github.com/dynaroars/neuralsat