Identifying safe areas is a key point to guarantee trust for systems that are
based on Deep Neural Networks (DNNs). To this end, we introduce the
AllDNN-Verification problem: given a safety property and a DNN, enumerate the
set of all the regions of the property input domain which are safe, i.e., where
the property does hold. Due to the #P-hardness of the problem, we propose an
efficient approximation method called epsilon-ProVe. Our approach exploits a
controllable underestimation of the output reachable sets obtained via
statistical prediction of tolerance limits, and can provide a tight (with
provable probabilistic guarantees) lower estimate of the safe areas. Our
empirical evaluation on different standard benchmarks shows the scalability and
effectiveness of our method, offering valuable insights for this new type of
verification of DNNs.

鉴于深度神经网络 (DNNs) 所基于的系统的可信保证，识别安全区域是一个关键问题。为此，我们提出了 AllDNN-Verification 问题：给定一个安全属性和一个 DNN，列举出在属性输入域中所有安全的区域，即属性成立的区域。由于该问题是 #P - 难问题，我们提出了一种高效的近似方法，名为 epsilon-ProVe。我们的方法利用对输出可达集合进行的统计预测容限限制的可控低估，并能够提供安全区域的一个紧凑的 (具有可证明的概率保证) 下界估计。我们在不同的标准基准测试上进行了实证评估，展示了我们方法的可扩展性和有效性，并为这种新类型的 DNN 验证提供了有价值的洞见。