Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guarantees

Luca Marzari, Davide Corsi, Enrico Marchesini, Alessandro Farinelli, Ferdinando Cicalese

TL;DR

This work introduces the AllDNN-Verification problem, given a safety property and a DNN, to enumerate the set of all the regions of the property input domain which are safe, i.e., where the property does hold, and proposes an efficient approximation method called ε-ProVe.

Abstract

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.

Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guarantees

TL;DR

This work introduces the AllDNN-Verification problem, given a safety property and a DNN, to enumerate the set of all the regions of the property input domain which are safe, i.e., where the property does hold, and proposes an efficient approximation method called ε-ProVe.

Abstract

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

This paper contains 17 sections, 4 theorems, 4 equations, 7 figures, 4 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. DNN-Verification
  4. #DNN-Verification
  5. The AllDNN-Verification Problem
  6. Hardness of AllDNN-Verification
  7. $\epsilon$-ProVe: a Provable (Probabilistic) Approach
  8. Probabilistic Reachable Set
  9. Computation of Safe Regions
  10. Theoretical Guarantees
  11. Empirical Evaluation
  12. Correctness and Scalability Experiments
  13. Discussion
  14. Supplementary Material
  15. Impact of Heuristics on $\epsilon$-ProVe Performances
  16. ...and 2 more sections

Key Result

Lemma 1

For any $R \in (0,1)$ and integer $n$, given a sample of $n$ values from a (continuous) set $X$ the probability that for at least a fraction $R$ of the values in a further possibly infinite sequence of samples from $X$ are all not smaller (respectively larger) than the minimum value (resp. maximum v

Figures (7)

  • Figure 1: A counterexample for a toy DNN-Verification problem.
  • Figure 2: Explanatory image execution of exact count for a particular $\mathcal{N}$ and safety property.
  • Figure 3: Explanatory image of how to exploit reachable set result for solving the AllDNN-Verification problem.
  • Figure 4: Example of computation single reachable set for a DNN with two outputs.
  • Figure 5: An example of applying Lemma \ref{['lemma3']} with $k=3$.
  • ...and 2 more figures

Theorems & Definitions (8)

  • Example 1
  • Definition 1: AllDNN-Verification Problem
  • Definition 2: $\epsilon$-Rectilinear Under-Approximation of safe areas for DNN ($\epsilon$-RUA-DNN)
  • Lemma 1
  • Proposition 2
  • Lemma 3
  • Theorem 4
  • proof