Recently, formal verification of deep neural networks (DNNs) has garnered considerable attention, and over-approximation based methods have become popular due to their effectiveness and efficiency. However, these strategies face challenges in addressing the "unknown dilemma" concerning whether the exact output region or the introduced approximation error violates the property in question. To address this, this paper introduces the UR4NNV verification framework, which utilizes under-approximation reachability analysis for DNN verification for the first time. UR4NNV focuses on DNNs with Rectified Linear Unit (ReLU) activations and employs a binary tree branch-based under-approximation algorithm. In each epoch, UR4NNV under-approximates a sub-polytope of the reachable set and verifies this polytope against the given property. Through a trial-and-error approach, UR4NNV effectively falsifies DNN properties while providing confidence levels when reaching verification epoch bounds and failing falsifying properties. Experimental comparisons with existing verification methods demonstrate the effectiveness and efficiency of UR4NNV, significantly reducing the impact of the "unknown dilemma".

翻译：近年来，深度神经网络（DNN）的形式化验证备受关注，基于过逼近的方法因其有效性和高效性而流行。然而，这些策略在应对“未知困境”——即无法确定精确输出区域或引入的近似误差是否违反待验证属性——时面临挑战。为此，本文首次提出UR4NNV验证框架，利用欠逼近可达性分析进行DNN验证。UR4NNV专注于具有修正线性单元（ReLU）激活函数的DNN，并采用基于二叉树的欠逼近算法。在每次迭代中，UR4NNV对可达集的子多胞体进行欠逼近，并验证该多胞体是否满足给定属性。通过试错方法，UR4NNV能有效证伪DNN属性，同时在达到验证迭代上限且未能证伪属性时提供置信度水平。与现有验证方法的实验比较表明，UR4NNV在有效性和高效性方面均具优势，显著降低了“未知困境”的影响。