Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Provably Bounding Neural Network Preimages

Suhas Kotha, Christopher Brix, Zico Kolter, Krishnamurthy Dvijotham, Huan Zhang

TL;DR

This work tackles inverse verification for neural networks by introducing INVPROP, a GPU-accelerated, LP-free bound-propagation method that over-approximates the preimage of a linearly constrained output set $f^{-1}(\mathcal{S}_{\text{out}})$. By unifying INVPROP with traditional bound propagation and applying a dual-relaxation chain (MILP -> LP -> dual), the authors derive tight, reusable lower bounds on intermediate activations under output constraints, enabling iterative tightening and branching. The approach yields dramatic improvements across benchmarks: up to $\sim$2500x tighter and $\sim$2.5x faster in control tasks, and up to $257\times$ tighter and $3.29\times$ faster for high-dimensional quadrotor models, while strengthening robustness verification and enabling OOD detection. The method is integrated into $α,\!β$-CROWN and demonstrates strong practical impact on safety-critical scenarios, including large models like YOLO in VNN-COMP '23, and supports more reliable OOD calibration and backward reachability analyses.

Abstract

Most work on the formal verification of neural networks has focused on bounding the set of outputs that correspond to a given set of inputs (for example, bounded perturbations of a nominal input). However, many use cases of neural network verification require solving the inverse problem, or over-approximating the set of inputs that lead to certain outputs. We present the INVPROP algorithm for verifying properties over the preimage of a linearly constrained output set, which can be combined with branch-and-bound to increase precision. Contrary to other approaches, our efficient algorithm is GPU-accelerated and does not require a linear programming solver. We demonstrate our algorithm for identifying safe control regions for a dynamical system via backward reachability analysis, verifying adversarial robustness, and detecting out-of-distribution inputs to a neural network. Our results show that in certain settings, we find over-approximations over 2500x tighter than prior work while being 2.5x faster. By strengthening robustness verification with output constraints, we consistently verify more properties than the previous state-of-the-art on multiple benchmarks, including a large model with 167k neurons in VNN-COMP 2023. Our algorithm has been incorporated into the $α,\!β$-CROWN verifier, available at https://abcrown.org.

Provably Bounding Neural Network Preimages

TL;DR

This work tackles inverse verification for neural networks by introducing INVPROP, a GPU-accelerated, LP-free bound-propagation method that over-approximates the preimage of a linearly constrained output set . By unifying INVPROP with traditional bound propagation and applying a dual-relaxation chain (MILP -> LP -> dual), the authors derive tight, reusable lower bounds on intermediate activations under output constraints, enabling iterative tightening and branching. The approach yields dramatic improvements across benchmarks: up to 2500x tighter and 2.5x faster in control tasks, and up to tighter and faster for high-dimensional quadrotor models, while strengthening robustness verification and enabling OOD detection. The method is integrated into -CROWN and demonstrates strong practical impact on safety-critical scenarios, including large models like YOLO in VNN-COMP '23, and supports more reliable OOD calibration and backward reachability analyses.

Abstract

Most work on the formal verification of neural networks has focused on bounding the set of outputs that correspond to a given set of inputs (for example, bounded perturbations of a nominal input). However, many use cases of neural network verification require solving the inverse problem, or over-approximating the set of inputs that lead to certain outputs. We present the INVPROP algorithm for verifying properties over the preimage of a linearly constrained output set, which can be combined with branch-and-bound to increase precision. Contrary to other approaches, our efficient algorithm is GPU-accelerated and does not require a linear programming solver. We demonstrate our algorithm for identifying safe control regions for a dynamical system via backward reachability analysis, verifying adversarial robustness, and detecting out-of-distribution inputs to a neural network. Our results show that in certain settings, we find over-approximations over 2500x tighter than prior work while being 2.5x faster. By strengthening robustness verification with output constraints, we consistently verify more properties than the previous state-of-the-art on multiple benchmarks, including a large model with 167k neurons in VNN-COMP 2023. Our algorithm has been incorporated into the -CROWN verifier, available at https://abcrown.org.
Paper Structure (48 sections, 2 theorems, 22 equations, 9 figures, 4 tables, 1 algorithm)

This paper contains 48 sections, 2 theorems, 22 equations, 9 figures, 4 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Background and Problem Setup
  3. Notation
  4. Problem Statement
  5. Applications
  6. Backward Reachability Analysis for Neural Feedback Loops.
  7. Robustness Verification
  8. Determining what inputs lead to confident predictions.
  9. Approach
  10. Convex over-approximation
  11. The INVPROP Algorithm
  12. The Mixed Integer Linear Programming (MILP) Formulation
  13. The Linear Programming (LP) Formulation
  14. The Inverse Propagation (INVPROP) Formulation
  15. Connection to forward verification
  16. ...and 33 more sections

Key Result

Theorem 1

Given an output set $\mathcal{S}_{\text{out}} = \{\boldsymbol{y} : \mathbf{H}\boldsymbol{y} + \mathbf{d} \leq \mathbf{0}\}$ and vector $\boldsymbol{c}$, $g_{\boldsymbol{c}}(\boldsymbol{\alpha}, \boldsymbol{\gamma})$ is a lower bound to the linear program in eq:LP for $\boldsymbol{0} \leq \boldsymbol where every term can be directly recursively computed via

Figures (9)

  • Figure 1: Visualization of relaxations. The inner green region depicts the true $f^{-1}(\mathcal{S}_{\text{out}})$, the blue relaxation depicts the intersection of finite half-spaces solved via MILP, the red relaxation displays the same via LP, and the purple relaxation displays the same via INVPROP. Though this diagram displays looseness, we provide a comprehensive methodology to reduce the error in all three relaxations up to arbitrary precision (Section \ref{['sec:branching']}).
  • Figure 2: Necessity of Iterative Tightening. Our approach enables us to iteratively tighten the bounds of all layers, with each iteration allowing for a smaller approximation ratio with respect to the true preimage. Green: Sum of bound intervals for all neurons in the third layer (second hidden layer); Blue: ratio between volumes of over-approximation and preimage. Measured for step $t=10$ of the control benchmark defined in Section \ref{['sec:control-results']}. Note that the improvement from iterative tightening is two orders of magnitude for intermediate bounds, and four orders of magnitude for the volume of the over-approximation.
  • Figure 3: Double Integrator. Each green region represents the preimage of the system one to ten steps back from the obstacle (red box). Each preimage is approximated $1$ million samples. The blue bounding boxes represent over-approximations, and INVPROP tightly over-approximates preimages even ten steps back.
  • Figure 4: 6D Quadrotor. We visualize the three dimensions of the 6D quadrotor that specify physical position. We consider the initial state range of the black box and simulate a few one-step trajectories, indicated by the orange lines. Our obstacle is the red box. For the three images, the blue box represents the over-approximation computed by (a) ReBreach-LP with no partitioning, (b) ReBreach-LP with 15625 partitions, and (c) INVPROP, respectively. A tighter blue box is better.
  • Figure 5: YOLO Results. Runtime comparison of $\alpha,\!\beta$-CROWN and $\alpha,\!\beta$-CROWN+INVPROP on the YOLO benchmark (167k neurons and 5 residual layers). For the comparison, only those test instances were used that could not immediately be verified by $\alpha,\!\beta$-CROWN without any iterative tightening of intermediate layer bounds. $\alpha,\!\beta$-CROWN+INVPROP can verify more properties and is faster for almost all instances.
  • ...and 4 more figures

Theorems & Definitions (4)

  • Theorem 1: Bounding input half-spaces
  • proof
  • Example 1
  • Theorem 2: Lower-bounding combination of neurons