Deep neural networks (DNNs) are increasingly being deployed to perform safety-critical tasks. The opacity of DNNs, which prevents humans from reasoning about them, presents new safety and security challenges. To address these challenges, the verification community has begun developing techniques for rigorously analyzing DNNs, with numerous verification algorithms proposed in recent years. While a significant amount of work has gone into developing these verification algorithms, little work has been devoted to rigorously studying the computability and complexity of the underlying theoretical problems. Here, we seek to contribute to the bridging of this gap. We focus on two kinds of DNNs: those that employ piecewise-linear activation functions (e.g., ReLU), and those that employ piecewise-smooth activation functions (e.g., Sigmoids). We prove the two following theorems: 1) The decidability of verifying DNNs with a particular set of piecewise-smooth activation functions is equivalent to a well-known, open problem formulated by Tarski; and 2) The DNN verification problem for any quantifier-free linear arithmetic specification can be reduced to the DNN reachability problem, whose approximation is NP-complete. These results answer two fundamental questions about the computability and complexity of DNN verification, and the ways it is affected by the network's activation functions and error tolerance; and could help guide future efforts in developing DNN verification tools.

翻译：深度神经网络（DNN）正越来越多地被部署于执行安全关键任务。DNN的不透明性阻碍了人类对其的推理，带来了新的安全与安保挑战。为应对这些挑战，验证社区已开始开发用于严格分析DNN的技术，近年提出了众多验证算法。尽管大量工作投入于开发这些验证算法，但对底层理论问题的可计算性与复杂性的严格研究却鲜有涉及。本文旨在为弥合这一差距做出贡献。我们关注两类DNN：采用分段线性激活函数（如ReLU）的DNN，以及采用分段光滑激活函数（如Sigmoid）的DNN。我们证明以下两个定理：1）具有特定分段光滑激活函数集的DNN验证的可判定性等价于Tarski提出的一个著名开放问题；2）任意无量词线性算术规范的DNN验证问题可归约为DNN可达性问题，其近似是NP-完全的。这些结果回答了关于DNN验证的可计算性与复杂性的两个基本问题，以及网络激活函数和误差容限对其的影响方式；并有望为未来DNN验证工具的开发工作提供指导。