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.

翻译：识别安全区域是确保基于深度神经网络（DNN）的系统可信的关键。为此，我们引入了AllDNN-Verification问题：给定一个安全属性和一个DNN，枚举属性输入域中所有安全的区域，即属性成立的空间。由于该问题属于#P难问题，我们提出了一种高效的近似方法——epsilon-ProVe。该方法通过基于容忍限统计预测的可控输出可达集欠估计，能够提供具有可证概率保证的紧致安全区域下界估计。我们在不同标准基准上的实证评估显示了该方法的可扩展性和有效性，为这种新型DNN验证提供了有价值的见解。