Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verifying Global Two-Safety Properties in Neural Networks with Confidence

Anagha Athavale, Ezio Bartocci, Maria Christakis, Matteo Maffei, Dejan Nickovic, Georg Weissenbacher

TL;DR

This work characterize and prove the soundness of the soundness of the static analysis technique, and implements it on top of Marabou, a safety analysis tool for neural networks, conducting a performance evaluation on several publicly available benchmarks for DNN verification.

Abstract

We present the first automated verification technique for confidence-based 2-safety properties, such as global robustness and global fairness, in deep neural networks (DNNs). Our approach combines self-composition to leverage existing reachability analysis techniques and a novel abstraction of the softmax function, which is amenable to automated verification. We characterize and prove the soundness of our static analysis technique. Furthermore, we implement it on top of Marabou, a safety analysis tool for neural networks, conducting a performance evaluation on several publicly available benchmarks for DNN verification.

Verifying Global Two-Safety Properties in Neural Networks with Confidence

TL;DR

This work characterize and prove the soundness of the soundness of the static analysis technique, and implements it on top of Marabou, a safety analysis tool for neural networks, conducting a performance evaluation on several publicly available benchmarks for DNN verification.

Abstract

We present the first automated verification technique for confidence-based 2-safety properties, such as global robustness and global fairness, in deep neural networks (DNNs). Our approach combines self-composition to leverage existing reachability analysis techniques and a novel abstraction of the softmax function, which is amenable to automated verification. We characterize and prove the soundness of our static analysis technique. Furthermore, we implement it on top of Marabou, a safety analysis tool for neural networks, conducting a performance evaluation on several publicly available benchmarks for DNN verification.
Paper Structure (25 sections, 6 theorems, 49 equations, 6 figures, 2 tables)

This paper contains 25 sections, 6 theorems, 49 equations, 6 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Local robustness and fairness
  3. Global robustness and fairness
  4. Our contributions
  5. Background
  6. Feed-Forward Neural Networks
  7. Hyperproperties
  8. Relational Verification and Self-Composition
  9. Robustness and Fairness
  10. Confidence Based Global Verification of Feed-Forward Neural Networks
  11. Encoding 2-Safety Properties as Product Neural Network
  12. Product Neural Network
  13. Transfer Functions and Operators
  14. Softmax Approximation
  15. Softmax in terms of $\max$ and $\operatorname{Sig}\xspace$
  16. ...and 10 more sections

Key Result

theorem 1

Let $\operatorname{softmax}\xspace$ and $\widehat{\operatorname{softmax}\xspace}$ compute the real and linearly approximated softmax (with precision $\delta$), respectively for the last layer of $n \geq 2$ neurons $\vec{z}$ of a neural network and $z_i = max(z_1, \cdots, z_n)$. Then, we have the fol

Figures (6)

  • Figure 1: (a) Local, (b) partitioned-global and (c) our confidence-based robustness. $x_1$ and $x_2$ denote continuous input points, while $x_3$ denotes a categorical input in the partitioned-global approach (b). The shades of gray in (c) depict the level of confidence of the neural network with respect to the given inputs -- dark gray denotes high while white denotes low confidence level. The neural network is robust to the pair of purple points in all three cases (a), (b) and (c). The neural network is not robust for the pair of blue points in the case of local and partitioned-global (b) robustness, but is robust according to our definition (c). Finally, the neural network is not robust for the pair of green points according to both the local and our confidence-based global robustness (a) and (c), but is robust with respect to the partitioned-global robustness (b). The global partitioning method does not catch the counterexample, because the two green points are in separate partitions.
  • Figure 2: (Simplified) Approximation of sigmoid with 4 linear segments
  • Figure 3: Input distance vs. confidence for German credit dataset
  • Figure 4: Input distance vs. confidence for adult dataset
  • Figure 5: Input distance vs. confidence for law school dataset
  • ...and 1 more figures

Theorems & Definitions (16)

  • definition 1: Local Robustness
  • definition 2: Global robustness
  • definition 3: Global fairness
  • definition 4: Confidence-based global 2-safety
  • theorem 1
  • proof
  • theorem 2
  • proof
  • theorem 3
  • proof
  • ...and 6 more