Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

UR4NNV: Neural Network Verification, Under-approximation Reachability Works!

Zhen Liang, Taoran Wu, Ran Zhao, Bai Xue, Ji Wang, Wenjing Yang, Shaojun Deng, Wanwei Liu

TL;DR

UR4NNV addresses the Unknown dilemma in DNN verification by introducing under-approximation reachability for ReLU networks. It represents reachable sets as polytopes and applies a random-branch under-approximation across multiple epochs to falsify properties, providing a confidence measure when exact completion is not feasible. On ACAS Xu benchmarks, UR4NNV achieves substantial falsification capability and repeatedly outperforms over-approximation methods in both effectiveness and efficiency, while also serving as a preprocessing step to accelerate traditional verifiers. The framework introduces soundness and completeness guarantees in the limit, along with practical optimization strategies that enable scalable, high-confidence DNN safety verification.

Abstract

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: Neural Network Verification, Under-approximation Reachability Works!

TL;DR

UR4NNV addresses the Unknown dilemma in DNN verification by introducing under-approximation reachability for ReLU networks. It represents reachable sets as polytopes and applies a random-branch under-approximation across multiple epochs to falsify properties, providing a confidence measure when exact completion is not feasible. On ACAS Xu benchmarks, UR4NNV achieves substantial falsification capability and repeatedly outperforms over-approximation methods in both effectiveness and efficiency, while also serving as a preprocessing step to accelerate traditional verifiers. The framework introduces soundness and completeness guarantees in the limit, along with practical optimization strategies that enable scalable, high-confidence DNN safety verification.

Abstract

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".
Paper Structure (16 sections, 4 theorems, 3 equations, 5 figures, 5 tables, 1 algorithm)

This paper contains 16 sections, 4 theorems, 3 equations, 5 figures, 5 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries and Notations
  3. Methodology
  4. Dilemma and Insight
  5. Under-approximation of ReLU DNNs
  6. UR4NNV Verification Framework
  7. Optimization Strategy
  8. Experiments
  9. Falsifying DNN Property
  10. Validating DNN Property with Confidence
  11. Optimization Strategy Comparison
  12. Related Work
  13. Conclusion
  14. Proof of Theorem \ref{['thm:under']}
  15. Proof of Theorem \ref{['thm: complete']}
  16. ...and 1 more sections

Key Result

Lemma 1

Affine transformations only change vertices but preserve polytopes' combinatorial structure, i.e., polytopes are closed under affine transformations 10.5555/285869.285884.

Figures (5)

  • Figure 1: Illustration on the unknown dilemma and coping insight.
  • Figure 2: Demonstrations of $\mathrm{ReLU}$ operators
  • Figure 3: Workflow of UR4NNV framework
  • Figure 4: Verifying properties with confidence levels
  • Figure 5: Depiction of the ACAS Xu DNN

Theorems & Definitions (6)

  • Lemma 1
  • Lemma 2
  • Theorem 1
  • Theorem 2
  • proof
  • proof