Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Out of the Shadows: Exploring a Latent Space for Neural Network Verification

Lukas Koller, Tobias Ladner, Matthias Althoff

TL;DR

This work tackles the challenge of formally verifying neural networks by addressing conservatism in traditional set-based approaches. It introduces a latent space built from projection-based set representations, where all considered sets are shadows of a fixed higher-dimensional hypercube, allowing safe constraints to be transferred from outputs back to inputs. The authors integrate this latent-space refinement into a branch-and-bound verification framework and demonstrate substantial improvements in subproblem reduction and GPU-based efficiency, achieving competitive performance on VNN-COMP'24 benchmarks. The approach also enables efficient counterexample extraction and is supported by thorough ablations, underscoring its practical impact for scalable, safety-critical neural-network verification.

Abstract

Neural networks are ubiquitous. However, they are often sensitive to small input changes. Hence, to prevent unexpected behavior in safety-critical applications, their formal verification -- a notoriously hard problem -- is necessary. Many state-of-the-art verification algorithms use reachability analysis or abstract interpretation to enclose the set of possible outputs of a neural network. Often, the verification is inconclusive due to the conservatism of the enclosure. To address this problem, we design a novel latent space for formal verification that enables the transfer of output specifications to the input space for an iterative specification-driven input refinement, i.e., we iteratively reduce the set of possible inputs to only enclose the unsafe ones. The latent space is constructed from a novel view of projection-based set representations, e.g., zonotopes, which are commonly used in reachability analysis of neural networks. A projection-based set representation is a "shadow" of a higher-dimensional set -- a latent space -- that does not change during a set propagation through a neural network. Hence, the input set and the output enclosure are "shadows" of the same latent space that we can use to transfer constraints. We present an efficient verification tool for neural networks that uses our iterative refinement to significantly reduce the number of subproblems in a branch-and-bound procedure. Using zonotopes as a set representation, unlike many other state-of-the-art approaches, our approach can be realized by only using matrix operations, which enables a significant speed-up through efficient GPU acceleration. We demonstrate that our tool achieves competitive performance, which would place it among the top-ranking tools of the last neural network verification competition (VNN-COMP'24).

Out of the Shadows: Exploring a Latent Space for Neural Network Verification

TL;DR

This work tackles the challenge of formally verifying neural networks by addressing conservatism in traditional set-based approaches. It introduces a latent space built from projection-based set representations, where all considered sets are shadows of a fixed higher-dimensional hypercube, allowing safe constraints to be transferred from outputs back to inputs. The authors integrate this latent-space refinement into a branch-and-bound verification framework and demonstrate substantial improvements in subproblem reduction and GPU-based efficiency, achieving competitive performance on VNN-COMP'24 benchmarks. The approach also enables efficient counterexample extraction and is supported by thorough ablations, underscoring its practical impact for scalable, safety-critical neural-network verification.

Abstract

Neural networks are ubiquitous. However, they are often sensitive to small input changes. Hence, to prevent unexpected behavior in safety-critical applications, their formal verification -- a notoriously hard problem -- is necessary. Many state-of-the-art verification algorithms use reachability analysis or abstract interpretation to enclose the set of possible outputs of a neural network. Often, the verification is inconclusive due to the conservatism of the enclosure. To address this problem, we design a novel latent space for formal verification that enables the transfer of output specifications to the input space for an iterative specification-driven input refinement, i.e., we iteratively reduce the set of possible inputs to only enclose the unsafe ones. The latent space is constructed from a novel view of projection-based set representations, e.g., zonotopes, which are commonly used in reachability analysis of neural networks. A projection-based set representation is a "shadow" of a higher-dimensional set -- a latent space -- that does not change during a set propagation through a neural network. Hence, the input set and the output enclosure are "shadows" of the same latent space that we can use to transfer constraints. We present an efficient verification tool for neural networks that uses our iterative refinement to significantly reduce the number of subproblems in a branch-and-bound procedure. Using zonotopes as a set representation, unlike many other state-of-the-art approaches, our approach can be realized by only using matrix operations, which enables a significant speed-up through efficient GPU acceleration. We demonstrate that our tool achieves competitive performance, which would place it among the top-ranking tools of the last neural network verification competition (VNN-COMP'24).

Paper Structure

This paper contains 25 sections, 4 theorems, 30 equations, 3 figures, 3 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Notation
  4. Feed-Forward Neural Networks
  5. Set-Based Computing
  6. Formal Verification of Neural Networks
  7. Problem Statement
  8. A Novel View on Zonotope Propagation
  9. Set-Based Falsification, Verification, and Input Refinement
  10. Set-Based Verification
  11. Set-Based Falsification
  12. Input Set Refinement and Constraint-Based Input Splitting
  13. Evaluation
  14. Ablation Studies
  15. Falsification Method
  16. ...and 10 more sections

Key Result

Proposition 1

Given a neural network $\NN\colon\mathbb{R}^{\numNeurons_0}\to\mathbb{R}^{\numNeurons_\numLayers}$ and an input set $\nnInputSet\subset\mathbb{R}^{\numNeurons_0}$, an enclosure $\nnOutputSet = \opEnclose{\NN}{\nnInputSet} \subset\mathbb{R}^{\numNeurons_\numLayers}$ of the image $\nnOutputSetExact \c

Figures (3)

  • Figure 1: (a) An illustration of a constrained zonotope and a sample with its generators; (b) the same constrained zonotope as the "shadow" of a constrained hypercube.
  • Figure 2: Illustrating the zonotope propagation through a linear layer and a nonlinear layer as the "shadows" of the same hypercube: (a) The input interval in the input space; (b) The output of the linear layer, which rotates and offsets the input set; (c) The output of the nonlinear layer tilts the hypercube to add the approximation errors. Using the hypercube, the unsafe set ( ) is transferred from the output space to the input space. Additionally, the hypercube is split along a hyperplane ( ) to exploit the piecewise linearity of the $\mathop{\mathrm{ReLU}}\nolimits$-activation function.
  • Figure 3: Illustration of an iterative refinement of the input set: The input set is iteratively refined (\ref{['prop:input_set_refinement']}). After the fourth iteration, the intersection with the unsafe set is empty, and the neural network is verified.

Theorems & Definitions (11)

  • Definition 1: Neural Network, bishop_2006
  • Definition 2: Zonotope, girard_2005
  • Definition 3: Constrained Zonotope, scott_et_al_2016
  • Proposition 1: Set Propagation, ladner_althoff_2023
  • Example 1
  • Proposition 2: Enclosing Unsafe Inputs
  • Corollary 1
  • proof
  • Proposition 3: Bounds of Bounded Polytope
  • proof
  • ...and 1 more