Deep Neural Networks are increasingly adopted in critical tasks that require a high level of safety, e.g., autonomous driving. While state-of-the-art verifiers can be employed to check whether a DNN is unsafe w.r.t. some given property (i.e., whether there is at least one unsafe input configuration), their yes/no output is not informative enough for other purposes, such as shielding, model selection, or training improvements. In this paper, we introduce the #DNN-Verification problem, which involves counting the number of input configurations of a DNN that result in a violation of a particular safety property. We analyze the complexity of this problem and propose a novel approach that returns the exact count of violations. Due to the #P-completeness of the problem, we also propose a randomized, approximate method that provides a provable probabilistic bound of the correct count while significantly reducing computational requirements. We present experimental results on a set of safety-critical benchmarks that demonstrate the effectiveness of our approximate method and evaluate the tightness of the bound.

本文介绍了DNN-Verification问题，分析了其复杂性并提出了一种新颖的方法，该方法返回违反特定安全属性的DNN输入配置的确切计数。考虑到问题的#P完备性，我们还提出了一种随机的、近似的方法，该方法提供了一个可证明的概率界限，同时显著减少了计算需求。我们在一组安全关键基准上呈现了实验结果，证明了我们的近似方法的有效性，并评估了界限的紧密度。

DNN-验证问题：计算深度神经网络的不安全输入数量