UR4NNV: Neural Network Verification, Under-approximation Reachability
  Works!
Zhen Liang Taoran Wu Ran Zhao Bai Xue Ji Wang Wenjing Yang Shaojun Deng Wanwei Liu
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".