DNN Verification, Reachability, and the Exponential Function Problem
DNN Verification, Reachability, and the Exponential Function Problem
复制标题
DOI：
10.48550/arxiv.2305.06064
复制
发表时间：
2023-05
期刊：
影响因子：
--
通讯作者：
Omri Isac;Yoni Zohar;Clark W. Barrett;Guy Katz
中科院分区：
文献类型：
--
作者：
Omri Isac;Yoni Zohar;Clark W. Barrett;Guy Katz
深度神经网络（dnn）越来越多地被用于执行安全关键任务。深度神经网络的不透明性使人类无法对其进行推理，这带来了新的安全和安保挑战。为了应对这些挑战，验证社区已经开始开发严格分析dnn的技术，近年来提出了许多验证算法。虽然大量的工作已经投入到开发这些验证算法中，但很少有工作专门用于严格研究潜在理论问题的可计算性和复杂性。在此，我们力求为弥合这一差距作出贡献。我们关注两种dnn：采用分段线性激活函数的dnn（例如，ReLU）和采用分段平滑激活函数的dnn（例如，Sigmoids）。我们证明了以下两个定理：1)用一组特定的分段光滑激活函数验证dnn的可判定性等价于一个众所周知的由Tarski提出的开放问题；(2)任意无量词线性算法规范的DNN验证问题可归结为DNN可达性问题，其近似为np完全问题。这些结果回答了两个基本问题：DNN验证的可计算性和复杂性，以及它受网络激活函数和容错性影响的方式；并且可以帮助指导未来开发深度神经网络验证工具的工作。
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.