Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verification of Neural Networks' Global Robustness

Anan Kabaha, Dana Drachsler-Cohen

TL;DR

This work proposes a new global robustness property for classifiers aiming at finding the minimal globally robust bound, which naturally extends the popular local robustness property for classifiers and introduces VHAGaR, an anytime verifier for computing this bound.

Abstract

Neural networks are successful in various applications but are also susceptible to adversarial attacks. To show the safety of network classifiers, many verifiers have been introduced to reason about the local robustness of a given input to a given perturbation. While successful, local robustness cannot generalize to unseen inputs. Several works analyze global robustness properties, however, neither can provide a precise guarantee about the cases where a network classifier does not change its classification. In this work, we propose a new global robustness property for classifiers aiming at finding the minimal globally robust bound, which naturally extends the popular local robustness property for classifiers. We introduce VHAGaR, an anytime verifier for computing this bound. VHAGaR relies on three main ideas: encoding the problem as a mixed-integer programming and pruning the search space by identifying dependencies stemming from the perturbation or the network's computation and generalizing adversarial attacks to unknown inputs. We evaluate VHAGaR on several datasets and classifiers and show that, given a three hour timeout, the average gap between the lower and upper bound on the minimal globally robust bound computed by VHAGaR is 1.9, while the gap of an existing global robustness verifier is 154.7. Moreover, VHAGaR is 130.6x faster than this verifier. Our results further indicate that leveraging dependencies and adversarial attacks makes VHAGaR 78.6x faster.

Verification of Neural Networks' Global Robustness

TL;DR

This work proposes a new global robustness property for classifiers aiming at finding the minimal globally robust bound, which naturally extends the popular local robustness property for classifiers and introduces VHAGaR, an anytime verifier for computing this bound.

Abstract

Neural networks are successful in various applications but are also susceptible to adversarial attacks. To show the safety of network classifiers, many verifiers have been introduced to reason about the local robustness of a given input to a given perturbation. While successful, local robustness cannot generalize to unseen inputs. Several works analyze global robustness properties, however, neither can provide a precise guarantee about the cases where a network classifier does not change its classification. In this work, we propose a new global robustness property for classifiers aiming at finding the minimal globally robust bound, which naturally extends the popular local robustness property for classifiers. We introduce VHAGaR, an anytime verifier for computing this bound. VHAGaR relies on three main ideas: encoding the problem as a mixed-integer programming and pruning the search space by identifying dependencies stemming from the perturbation or the network's computation and generalizing adversarial attacks to unknown inputs. We evaluate VHAGaR on several datasets and classifiers and show that, given a three hour timeout, the average gap between the lower and upper bound on the minimal globally robust bound computed by VHAGaR is 1.9, while the gap of an existing global robustness verifier is 154.7. Moreover, VHAGaR is 130.6x faster than this verifier. Our results further indicate that leveraging dependencies and adversarial attacks makes VHAGaR 78.6x faster.
Paper Structure (47 sections, 6 theorems, 9 equations, 7 figures, 4 tables, 2 algorithms)

This paper contains 47 sections, 6 theorems, 9 equations, 7 figures, 4 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Minimal Globally Robust Bounds
  4. Perturbations
  5. Local robustness
  6. Towards a global robustness property
  7. $\delta$-Global Robustness
  8. Targeted global robustness
  9. Overview of Key Ideas
  10. Minimal Globally Robust Bound via Optimization
  11. Problem complexity
  12. Anytime optimization
  13. Reducing Complexity via Encoding of Dependencies
  14. Example
  15. Computing a Suboptimal Lower Bound by a Hyper-Adversarial Attack
  16. ...and 32 more sections

Key Result

lemma 1

Let $\delta^*_{(1)}$ be the optimal value of Problem problem1 and $\delta^*_{(2)}$ be the optimal value of Problem problem2 (where $\delta^*_{(2)}\triangleq 0$ if Problem problem2 is infeasible). Then $\delta^*_{(1)} -\delta^*_{(2)} =\Delta$, where $\Delta$ is the precision level.

Figures (7)

  • Figure 1: (a) The perturbations supported by VHAGaR. (b) VHAGaR's upper and lower bounds on the minimal globally robust bound vs. sampling approaches, Marabou and a MIP-only variant of VHAGaR.
  • Figure 2: The bounds as a function of the execution time, when providing a MIP solver (a) our encoding, (b) additionally our dependencies, and (c) additionally our suboptimal lower bound and optimization hints.
  • Figure 3: An example of the perturbation dependencies of an occlusion perturbation blackening the pixel $(1,1)$.
  • Figure 4: An example of running the hyper-adversarial attack to obtain a suboptimal lower bound on the maximal globally non-robust bound for the occlusion perturbation blackening the pixel (1, 1).
  • Figure 5: Illustration of VHAGaR.
  • ...and 2 more figures

Theorems & Definitions (12)

  • definition 1: Class Confidence
  • definition 2: $\delta$-Globally Robust Classifier
  • definition 3: Minimal Globally Robust Bound
  • definition 4: $\delta$-Targeted Globally Robust Classifier
  • lemma 1
  • proof
  • lemma 2
  • lemma 3
  • lemma 4
  • lemma 5: Dependency Propagation
  • ...and 2 more