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".

该研究介绍了 UR4NNV 验证框架，它首次利用了 DNN 的欠逼近可达性分析方法，针对具有 ReLU 激活函数的 DNN 并采用基于二叉树分支的欠逼近算法。UR4NNV 有效验证 DNN 属性且在达到验证轮数和未能证伪属性时提供置信水平，实验比较结果显示 UR4NNV 在解决 “未知困境” 方面的有效性和效率，显著减少了影响。