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 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验证工具的开发方向。