Provably Bounding Neural Network Preimages
Authors: Suhas Kotha
Christopher Brix
J Zico Kolter
Krishnamurthy Dj Dvijotham
Huan Zhang
Venue: NeurIPS 2023 spotlight (2023)
Keywords: Trustworthy ML
Formal Verification
Safe Control
OOD Detection
TL;DR: We present an efficient algorithm to over-approximate the preimage of a neural network.

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 $2500\times$ tighter than prior work while being $2.5\times$ 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 $\alpha,\beta$-CROWN verifier, available at https://abcrown.org.

Provably Bounding Neural Network Preimages
Suhas Kotha"
Christopher Brix"
Carnegie Mellon
RWTH Aachen
suhask@andrew. edu
rrrixess.rtthaaccheee de
Zico Kolter
Krishnamurthy (Dj) Dvijotham Google DeepMind
Huan Zhang UIUC huanChuan-zhang.. com
Carnegie Mellon
Bosch Center for AI zkolterêcs. cmu edu
avijotthancs@gmallccom com
Abstract
Most work on the formal verification of neural networks has focused on bounding the set of outputs that correspond to 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-approximatin the set of inputs that lead to certain outputs. We present the INVPROP algorithm for verifying properties over the preimage of linearly constrained output set, which to increase precision. Contrary to other
can be combined with branch-and-boun approaches, our efficient algorithm GPU-accelerated and does not require linear programming solver. We demonstrate our algorithm for identifying safe control regions for dynamical system via backward reachability analysis, verifying adversarial robustness, and detecting out-of-distribuie Our results show that in certain settings, we find over-approximmation over 2500 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 state-of-the-art the-art multiple benchmarks, including large model with 167k neurons in VNN-COMP 2023, Our algorithm has been incorporated into the a.3-CROWN verifier, available at httpps:/ haapss:///bcro.... org.
inputs to a neural network.
Introduction
Applying neural networks to safety-critical settings often requires reasoning about constraints on the inputs and outputs a neural network. For example, for a physical system controlled by neural network policy, it is of interest to understand which initial states will lead to unsafe state such as colliding with an obstacle. Formal verification of neural networks seeks to provide provable guarantees demonstrating that networks satisfy formal specifications Most work to date has focused on developing algorithms that can bound the outputs of neural network given constraints the inputs, which can be used for applications such analyzing the robustness of a neural network to perturbations of given input (Wong and Kolter 2018 Dvijotham
their inputs and outputs.
al. 2018 Zhang al., 2018a Raghunathan al. 2018 Gehr et al. | 2018).
In this work, we address the inverse problem of over wer-approximating neural network's preimage: given a set of outputs Sout (described by linear constraints on the network output), we seek to find that provably contains all inputs that lead such outputs. For example, for our neural network policy, this would correspond to the states that collide with an obstacle one step in the future. Though the verification problem is already challenging due to non-convexity and high dimensionality. this new problem is even more difficult since neural networks are generally not invertible.
Equal contribution, Equal advising Instructions for reproducing our results are available
37th Conference on Neural Information Processing Systems (NcurIPS 2023).

---

Specifically, representative efficient verifiers (such as tfate-of-the-arr bound propaaatooo propagation-based based meth- ods [Zhang al. 2022) ) can only compute bounds utilizing constraints on the input and critically depend on having tight bounds on intermediate activations. In the setting of this paper, however, the bounds derived from the imput constraints are almost vacuous, since the only constraints on the input are that it should be from the valid input domain. We efficiently solve this problem by significandly generalizing the existing bound propagation based verification framework, allowing one to leverage output constraints when tightening the intermediate activations. Our contributions are as follows:
We develop an effective bound propagation framework, Inverse Propagation for Neural Network Verification (INVPROP), for the inverse verification problem for neural networks, i.e., the problem of over-approximating the set of inputs that leads to a given set of outputs. Importantly, INVPROP requires no linear programming solver and can compute bounds on any intermediate layer.
We unify INVPROP and traditional bound propagation into a more general verification framework, allowing us to connect our method to standard tools, such as the state-of-the-an bound propagation
tool a, 3-CROWN [Zhang et al. 2018a Xu al., 2021 Wang et al. 2021 Zhang et al. 2022 Brix et al., 2023 Müller et al., 2023 Our contribution allows 0r,3- B.B-CRRWN to tighten intermediate bounds with respect to output constraints, which could not be done by the original tool.
We demonstrate that tight inverse verification requires multiple iterative refinements of intermediate bounds. While layer bounds in standard bound propagation only depend on the bounds of their predecessors, INVPROP incorporates bounds of all layers in the network.
We improve the state of the art on control benchmark [Rober et al. [022a by providing 2500 tighter bounds, 2.5x faster, for a Double Integrator and 257 x tighter bounds, 3.29x faster, for 6D Quadrotor. Furthermore, we demonstrate that INVPROP can strengthen robustness verification with output constraints and verify more robustness properties in less time compared to existing tools. Finally, we demonstrate its applicability in OOD detection.
Background and Problem Setup
2.1 Notation
We use [L.] for T. E N to refer to the set (1,2,..., ..,...... LJ. w())
:. to refer to column j of the matrix W(),
[++ to refer to max(0, +), and [:]- to refer to - min(0, -. We use boldface symbols for vectors and
matrices (such as (x))) and W and regular symbols for scalars (such as (())) We use a @ y to denote element-wise multiplication of vectors x, y.
We define L layer ReLU neural network by its weight matrices (()) and bias vectors (() for i E [L]. The output of the neural network for the input (0) from bounded input domain X is computed by alternately applying linear layers o = ((-((1)) + (()) and ReLU layers ( (O, ()) until we receive the output (44 (which we refer to as the logits). Note that we treat softmax component of the loss function, the neural network.
2.2 Problem Statement
Given a neural network f X' C - Rau and an output constraint Sont C Roa, we want to compute (Sout) X. Since precisely computing expressing f ( is an intractable problem in general, we strive to compute a tight over-approximation Sover such that (Sout) C Sover- In particular, we target the convex hull of the preimage via cutting-plane representation. S.u will be defined by set of linear constraints parameterized by Hf (x) + d < 0 in this work.
2.3 Applications
Backward Reachability Analysis for Neural Feedback Loops. Establishing safety guarantees for neural network policies is a challenging task. One problem of interest is to find a set of initial states that does not reach particular set of future states under the neural network policy. This can be helpful in collision avoidance or control with safety constraints. For example, consider discrete-time double integrator controller (Hu et al. 22200] where the state at time é 1 can be directly computed based on state at time following the equation
[0.5
x1+1 = f(x,)= =
2t +
π (xx)
0

---

with policy IR2 + R. If there is an obstacle in the room covering the region [4.5. x [-0.25, 0.25], is of interest to understand which states will enter the unsafe region in the next time-step. We can represent this obstacle set with linear constraints that define Sant-
f (Sam) denotes the set of states a such that x lies in the unsafe region given the control policy т. Overapproximating this set allows us to define the set of states to avoid one timestep in advance.
We can compose f with itself times to obtain the set of initial states where л would drive the system to the unsafe set after / steps.
Robustness Verification Adversarial robustness is one classic problem for neural network ver- ification where verifiers assess whether all perturbations of an input yield the same classification. INVPROP can be used to speed up this verification by exploiting an implicit output constraint. We follow Wang et al. [2021] and use the canonical form of verifying a property by proving that mingex f(z) 0. f(z) will be negative if and only if is adversarial example. This mini- mization problem can be rewritten as f(r)) X (x) [Yang et al. 2021b]. If no adversarial example exists, the infimum is computed over empty set and returns positive infinity, indicating local robustness. If at least one adversarial example exists, the result is guaranteed to be negative. With the output constraint fx) 2 O. we only analyze inputs that yield an incorrect classification, reducing the search space and tightening verification bounds.
Determining what inputs lead to confident predictions. It is challenging train a classifier that knows when it doesn't 't know. A simple and effective approach is to train with an additional logit representing OOD abstention. Labeled data for this additional class is generated via outlier exposure, or adding synthetic training data known to be OOD [Hendrycks et al. 2018 Chen et al. 2021].
Consider the logits y produced by a binary classifier trained in this manner. The classifier can classify in-distribution data by comparing yo and yı, the logits corresponding to the two in-distribution labels. The quantity max (oo 31) - -y2 known as the logit gap, can be used to identify out-of-distribution
data (Fig. 7 in Appendix A). Can the logit gap correctly identify data far from the training data as being OOD? To answer this quesiton, we can compute the preimage of the set
Sou { max(yo 81) 2 3/3
We detail how to model this set with linear constraints in Appendix F. INVPROP enables to over-approximate f (Strt),), answering whether the classifier learned to correctly identify OOD data.
3 Approach
3.1 Convex over-approximation
Suppose want to find convex over-approximmtion of f- The tightest such set is its convex hull, which is the intersection of all half-spaces that contain f (S [Boyd et al. 2004). This intersection equivalent to Degro (æ c æ 2 min (a.")s., c x') which means that we can build over-approximation by taking this intersection for finitely many Furthermore, replacing the minimization problem with a lower bound to its value still yields a valid half-space, where a tighter bound yields tighter approximation.
We focus convex over-approximatione for two reasons: First, checking that the preimage satisfies a linear constraint e æ + d 2 0 is equivalent to minimizing the linear function æ + e x over the preimage, which in turn equivalent to minimizing the linear function over CONV (S-1(S..n) [Boyd et al., 2004]. Second, the convex hull and its tractable over-approximations are conveniently represented as intersections of linear constraints on the preimage, each of which can be quickly computed after single precomputation phase to tighten bounds on intermediate neurons using the INVPROP algorithm outlined in the next section.
For the above reasons, we will focus on solving the following constrained optimization problem.
min
T ax;
s.t. x E X;
f (x) E Soat
Note that this differs from the widely studied forward verification problem, which can be phrased as
min SES
c f
where Sin a set representing constraints on the input, and the goal of the verification is to establish that the output f (x) satisfies linear constraint of the form e (æ) > d for all æ e Sm.
3

---

Figure Visualization of relaxations. The in- ner green region depicts the true (Sam), the blue relaxation depicts the intersection of finite half-spaces solved via MILP, the red relaxation dis- plays the same via LP, and the purple relaxation displays the same via INVPROP. Though this dia- gram displays looseness, wC provide a comprehen- sive methodology to reduce the error in all three relaxations up to arbitrary precision (Section 3.3
S Sover 2
SLP 2
SMILP 2
f (S
3.2 The INVPROP Algorithm
As brief overview of our method, we first construct the Mixed Integer Linear Program (MILP) for solving this optimization problem, which generates the over-approximation SMILP when solved for finitely many Then, relax the MILP to a Linear Program (LP), which can construct the over-approximation SLP- Finally, we relax the LP via its Lagrangian dual, which will be used to construct over-approximation Saver- This chain of relaxations is visualized in Figure 1
The Mixed Integer Linear Programming (MILP) Formulation For feed-forward ReLU neural networks, the non non-linearities from the max operator can be encoded via integer variables, and this problem admits a MILP encoding similar to prior work in adversarial robustness [Tjeng et 2017] Problem (I) is equivalent to:
min c x
(2a)
H d S 0: x (i) = g +b()) iE [L];
E X; (0) x;
(2b)
(2c)
a max(0, o0));
ie [6
(2d)
The Linear Programming (LP) Formulation Unfortunately, finding an exact solution to this MILP is NP-complete [Katz et al. 2017]. To sidestep the intractability exact verification, we can compute lower bounds for this program via its convex relaxation. We consider bounds on the outputs of intermediate layers:
Based on these bounds, we can take the ReLU triangle relaxation
EElers 2017 to get the LP
min z.
x
(3a)
X: (10) < - ()
-00==
Ha (1) +d ddd
(3b)
(1) = w (1-1) (1-1) (0)
(3c)
0 < x (1) x (1) < a (1)
2(0)
u
(1) - -z()= 18)
i [Z]
(3d)
u(
< u (0) are either the bounds implicit in X, or a refinement of these obtained via previous rounds of bound propagation input branching (see Algorithm [ for details). Most efficient neural network verifiers do solve an LP formulation of verification directly because LP solvers are often slow for problem instances involving neural networks. Instead, the bound propagation framework [Zhang et al., [0188a] Wang et al.) 202T]] Zhang et al., [022] practical and efficient way to lower bound the LP relaxation of the forward verification problem. However, there are two major roadblocks to applying existing methods here: Typical poond-propagation cannot directly handle the output constraints (Eq. 3bb and the objective involving input layer variables (Eq. Baj. This is true for optimizing bounds on the input, intermediate layers, and the output layer, all of which need to be iteratively tightened as demonstrated later.
where the bounds (0) < x

---

The Inverse Propagation (INVPROP) Formulation By changing the LP above to optimize the (4)
quantity a (input layer) or zjj (intermediate layers) for i [L 1]. the bounds for the j-th neuron of layer i can be tightened in separate LP calls. However, this program is too expensive to be run
multiple times for each neuron.
Xu et al. 2021 Wang et al. 202 Zhang et al. 2022), we efficiently lower bound the solution of the LP by optimizing its Lagrangian dual. This dual is highly structured [Wong and Kolter 2018) allowing us
Inspired by the success of CROWN-famity neural network verifiers (Zhagg al. 201 Sa
(2) by closed-form expressions of the to bound input half-spaces e x and intermediate bounds 2/2 W,
dual variables. Our main generalization is the ability to optimize input or intermediate layer bounds with the output constraints after them in the neural network, as shown in the following theorem.
Theorem 1 (Bounding input half-spaces) Given output set Saut {y Hy + d < 0} and vector c, ge(0x 7) is a lower bound the linear program for 0 S a S 1, 7 2 0, and ge defined via
90(a, 7) - [c [
1
c - OOT w
u 10
E
ui (
i=1 JEI=()
where every term can be directly recursively computed via
I I-() = {j: ) S 0}:
I+ = (j 14) こ 0):
I= = =5: <0 =
D(L) Yi 1 n (1+11 w w
Vi 11
(1)
I-)
(6)
0,
jEI
viE --
1+ ( 10,0
j JEZ=10
Proof. Full proof is presented in Appendix D
In Appendix C show how bound intermediate neurons in the network using similar approach. Since the intermediate bounds might depend on bounds on neurons in subsequent layers (due to the output constraint), prior work such as a-CROWN [Xu et al. 2021]. Instead, we must iteratively tighten intermediate layer bounds with respect to the tightest bounds all neurons computed thus far. This iterative approach can tighten the initially loose bounds by several orders of magnitude, as shown in Figure 2 After performing this procedure once, the intermediate bounds can be used tightly lower bound c x for any e via Theorem I Therefore, this computation can be shared across all the constraints we use describe Sover- Our algorithm can be expressed in terms of forward/backwand through layers of the neural network and implemented via standard deep learning modules in libraries like PyTorrc [Paszke al.) al.| [209]. Since all of the operations are auto-differentialle we can tighten our lower bound using standard gradient ascent (projected by the dual variable constraints).
cannot simply optimize bounds in single forward pass layer by layer, unlike
passes
10
10a
Figure 2: Necessity of Iterative Tightening. Our approach enables us to iteratively tighten the bounds of all layers, with each iteration allow- ing for smaller approximation ratio with respect to the true preimage. Green: Sum of bound in- tervals for all neurons in the third layer (second hidden layer); Blue: ratio between volumes over- approximation and preimage. Measured for step t= 10 of the control benchmark defined in Sec- tion 4.1 Note that the improvement from iterative tightening is two orders of magnitude for interme- diate bounds, and four orders of magnitude for the volume of the over-approximation.
Approximation Ratio
Bounds of layer 3
103
10a
10a
10a
10"
10a
0
10
20
30
40
50
60
Iteration
5

---

implement our Algorithm 1 INVPROP. Can be applied to branches for non-convex overapproximations Lower and upper bound of all neurons and all constraints are optimized using distinct and y values in g.
Initialize ((0) ( via cheap bound propagation methods for the forward verification problem
while lower bounds for (0)) are improving do for E {T. 1, - 2, ... 1,0} do
for j E layer neurons, b (lower, upper) do Optimize o from Theorem 2 via gradient ascent improve bound on neuron j in layer i with sense 6 (lower/upper)
if b upper then update
"j
(8) else update 1/1)
Optimize ge from Theorem via gradient ascent to improve lower bound on c' x for all c
Connection to forward verification Our bound Theorem Theorem[Jintrodi introduues the dual variable y, which enforces the output constraint during optimization. In fact, we conceptual interpretation of our result. For the optimization problem in (T). taking the dual with respect to the constraint Hf (a) + d s 0 yields the lower bound
this variable to get better
max min cx + 7 (Hf (z) d)
s.t. Z 7 2 0
The objective can be represented minimizing linear function of the output of residual neural network with a skip connection from the input to the output layer, subject to constraints on the input. Now, f(x) appears in the objective, similar the standard forward verification problem with an augmented network architecture. Similarly, optimizing an intermediate bound is equivalent to skip connection from layer the output (Appendix E.. These connections allow
method using standard verification tools Brix et al. 2023 Xu et al. 2021 2020].
When f is feedforward ReLU network, the lower bound described in this section is precisely the same as Theorem [ (since both are solving the dual of the same linear program). This shows that the introduction of constitutes our generalization to the bound propagation framework.
Selection of The dependence of the optimization on is not major limitation. The bounds of all intermediate neurons are optimized only with respect to the input and output constraints, not the hyperplanes used to describe the input half-space. Thus, their optimized bounds can be shared across the optimization of all input hyperplanes. For applications such as adversarial robustness, the box constraint of two hyperplanes per dimension could be chosen scalably bound the input. The selection of appropriate depends on the application and is not our main focus.
3.3 Branch and Bound
Though more rounds of iterative tightening will lower the gap in Sover St,, our current formulation still faces two sources of looseness: the gap in Sip 2 SMILP and the gap in SMILP 2 (Son). To overcome both of these issues, we can make use of branching [Bunel et al. 2020 While there several possibilities here, we focus on input branching, which gave the biggest empirical gains in our
experiments described in Section More concretely, we divide the input domain X' = (7(0) u (0) into several regions by choosing coordinate i and computing
X X' n (x: a s1), X, = X n (x < s
so that X' = Xe U M.. Doing this recursively, we obtain several regions and can compute an overapproximation of ff (S..)) when the input is in each of those regions, and take union of the resulting sets. The finer the input domain of our over-approximation the tighter the approximation.
Results
We evaluate INVPROP on three different benchmarks. Across benchmarks, we find orders of magnitude improvement over prior work, and our methods work even for relatively large networks (167k neurons) and high dimensionality inputs (81 dimensions). All implementation details are described in Appendix F and the utilized hardware is described in Appendix G

---

Figure 3: Double Integrator. Each green region represents the preimage of the system one to 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 ten steps back.
(a) ReBreach-LLP
(b) INVPROP
Table 1: Double Integrator Results. IN- VPROP vs SOTA (from Figure 3). We are significantly tighter and faster than ReBreach-LP method even without input branching.
METHOD
REBREACH-LP
INVPROP
INPUT BRANCHING APPROX RATIO TIME (SEC)
YES
NO
4021.47 42.86 + 0.04
1.46
17.89 0.03
4.1 Backward Reachability Analysis for Neural Feedback Loops
Double Integrator After combining the state-feedback control policy of the benchmark with the state transition function from Section 2.3 (see Section F2). we get a three layer MLP with 12, and 2 neurons, which is typical for applications in this setting. We model multiple time steps via composing copies of this function Moreover, we leverage intermediate bounds for time step to bound the L time step transition. We measure the tightness of an over-approximation using its Approximation Ratio, defined as vollf-"(S.. Both of these volumes are heuristically estimated with 1 million samples of the input space. While INVPROP allows the optimization of arbitrary input cutting planes, we use 40 planes with slopes of equally distributed angles.
SSm))
We find that INVPROP significantly tighter and faster than ReBreach-LPP the SOTA available method for this problem [Rober et al. 2022a b) As evident in Figure 3 ReBreach-LPP suffers from increasingly weak bounds as t increases, whereas our approach is able to compute tight bounds for all t. Different to their implementation, we are able to leverage the output constraint to improve the intermediate neuron bounds. Furthermore, we can iteratively tighten these bounds with respect to each other. Even though we optimize many more quantities, our efficient bound propagation allows us to solve the problem faster overall. We provide a visualization of the improvement of the approximation ratio score and intermediate bounds over time in Figure 2 tightness and speed are quantified in Table
Both our increased
6D Quadrotor We consider over-approximating the preimage of the linearized quadrotor discussed in Figure 15 Rober et al. [2022)). This quadrotor has a 6-dimensional state space with dimensions dedicated to position and given by the dynamics
1
0
0
1
0
0
0.5
0
0
0
1
0
0
0.5
0
0
0
1
0
0
0
0
0.5
Ft+11
0
+
T(x;))
0
0
0
0
0
0
0
0
0
0
1
0
1
The policy, after performing the same encoding as the double integrator and clipping policy outputs,
forms five layer MLP with 26, 26, 9, 9,9, and 3 neurons. For these dynamics, we want to prove that
the initial state range of [-5.25. - 4.75 [-25, 255 x [2.25, 2.75] x (0.95, 0.99) [-0.01, 0.00) x
[-1,1] x [1.5, x [-1,1] x [-1, x 1, (red box). We try to find the tightest bounding box in the 3 position dimensions, reflecting total of 6 input cutting planes (one for each direction in each dimension). To benchmark against prior work, we run ReBreach-LP with no output partitioning and
[-0.01, 0.01] (black box in Figure 4 will never collide with the obstacle at [-1,1]
'Frr example, the 10 time step transition function can be represented as a 21 layer MLP (after fusing consecutive linear layers in the composition).
"We do not compare with Everett et al. [2022) which improves upon ReBreach-La LP,, as their implementation faces numerical instability when applied for ten timesteps. However, preliminary experiments show that we also outperform their bounds.
7

---

3.5
3.5
35
3.0
3.0
25
2
2,5
2.0
2.0
2.0
1.5
1.5
1.5
4
2
2 91
2
2
0
(a) ReBreach-LLP no partitions
(b) ReBreach-L.P 15625 partitions
(c) INVPROP
Figure 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-LPP with 15625 partitions, and (c) INVPROP, respectively. A tighter blue box is better.
Table 2: Quadrotor Results. We compare the tightness of the over-approximations and run time (mean and std taken over 5 runs).
METHOD
REBREACH-LP
REBREACH-LP
INVPROP
PARTITIONS
N/A
15625
N/A 0.0000249
APPROX VoL.
64
0.064
TIME (SEC)
11.8 2.2
662.2 + 31.4
213.8 + 11.1
ReBreach-L.P with 15625 output partitions. We run our algorithm with no branching. In Figure 4 we compare these three strategies, and we find that over-approximation of the pre-image (in blue) smaller than the state-of-the-ar over-approximattons by 257 times while being 3.29 times faster. Therefore, our algorithm scales well to higher dimensional control examples.
4.2 Robustness Verification
Similar to us. Yang et al. [2021b] encode the implicit output constraint of the local robustness verification query tighten the bounds on neurons. However, they need LP solver, which does scale to large problems. The state-of-the-ar verification toolkit a, R.8-CROWN (Zhang et al. 201 8a Xu et al. 2021 Wang et al. 2021 Zhang et al., (2022) is able to scale large networks, but does not currently utilize the implicit output constraint. We demonstrate the benefit of encoding the output constraint by extending a-3-CROWN and comparing the performance on the benchmark used by
Yang et al. [0021b] as well as benchmarks from the VNN-COMP 2023 |Brix et al. 2023
Yang et al. 2021b) provides four networks with ReLU activation functions and dense linear layers of 2/6/6/9 layers of 100/100/200/200 neurons, each trained on MNIST. For each network, 50 inputs were tested for local robustness. For the complete benchmark definition, we refer to Yang et al. bb. The DeepSRGR results are taken from Yang et al. [2021b), they do not report a timeout for their experiments. Both e.B-CROWN and a,3oCRRONY BACROW+INVPRRO
MNIST
were run with per-input timeout of 5 minutes. Except for the input bounds. all bounds of all layers of each network are tightened using output constraints. We report the results in Table 3 Notably, we verify more instances than the SOTA tool a,8-CROWN, in sometimes less than fifth the average runtime. We include a more detailed comparison between the results for R-B-CROWN and ..9-CROWN+INVPROP in Appendix H
VNN-COMP '23: YOLO In 2023, the VNN-COMP contained YOLO as an unscored benchmark for object detection. It is a modified version of YOLOv2 [Redmon and Farhadi 2016 with network of 167k neurons and 5 residual layers, and is available at [Zhong] 2023 Brix 2023 The network processes 52 52 images and uses convolutions, average pooling and ReLU activations. This benchmark is well suited for INVPROP, as the definition of the adversarial examples is a conjunction of constraints over the output. Therefore, a strong output constraint can be used to tighten the bounds of intermediate layers. The benchmark consists of 464 instances, of which 72 were randomly selected for the VNN-COMP. For our comparison, we remove those 348 instances that o, 3-CROWN verifies robust without tightening the bounds of any intermediate layer. Those instances are verified within

---

Minitss
Figure 5: YOLO Results. Runtime comparison of a.S- CROWN and R.WWWOWN--NVPPRP on the YOLO bench- mark (167k neurons and 5 residual layers). For the com- parison, only those test instances were used that could not immediately be verified by a,3-CROWN without any itcrative tightening of intermediate layer bounds. a,3- CROWN+INVPROP can verify more properties and is faster for almost all instances.
100
a.f-CROWN
0.5 CROWN
Instaces Verifiel
Table 3: MNIST Results. Robustness verification with DeepSRGR (output constraints via LP solver),
a, 0.S-CROWN (GPU support) and R.B-CROWN-INPPROP (output constraints with GPU support)
NETWORK
DEEPSRGR
a,8-CROWN
a,B-CROWN INVPROP
VERIF.
AVG. TIME [S]
VERIF.
AVG. TIME [S]
VERIF. AVG. TIME [S]
FFN4 (3x100)
35
781
45
7.4
45
6.4
FFNS (6x100)
31
1689
38
6.7
39
8.7
FFN6 (6x200)
31
6178
29
5.4
30
1.0
FFN7 (9x200)
8960
3.2
less than four seconds each by both methods, with no room for improvement. We compare the performance of n.ß-CROWN and a,ß-CROWN INVPROP on the remaining 116 instances in Figure 5 a,B-CROON can verify 48 instances, all other instances reach the timeout five minutes. After extending CROWN with INVPROP on the last two intermediate layers, almost all instances can be solved faster, and previously timed out instances become verifiable.
4.3 OOD Detection
Consider the calibrated OOD detector presented as discussed in Section encoded by a four layer MLP with 200, 200, 3, and neurons. We over-approximate the of inputs which induce sufficiently high in-distribution (ID) confidence (measured by max (yo, 31 > y2) using 40 hyper- planes of equal slope, pictured in green in Figure 6 This set non-convex, making the convex hull poor wer-approximmtton. With input space branches, we get a much tighter over-approximation as shown in the right plot. We compare the performance of our approach with and without branching over the input space with the MILP baseline (see Table This demonstrates simple proof-of-coneept for how INVPROP can used for verifying some calibration properties.
5 Related Work
Formally Verified Neural Networks. There has been a large body of work on the formal veri-
fication of neural networks, tackling the problem from the angles of Interval Bound Propagation
Gooaa et al.) 2018 Gehr et al.] 2018), Convex Relaxations [Wong and Kolter, 2018 Shiqi et al.
2018 Salman al., 2019 Dvijotham et al. 2018), Abstract Interpretation (Singh al. [0188 LP
Ehlers 2017]. SDP Raghunathan et al. 2018). SMT [Kazz et al. 2017]. and MILP [Teeng et al..
2017
However, most of this work is for forward verification (i.e., bounding the NN output given
Table OOD Results. Comparison of methods for wvrraaprroximatin the preimage of the OOD region (Figure 6). A lower approximation ratio (APPROX RAT.) is better.
425
-15
INPUT BRANCH.
APPROX RATIO
(a) No branching
(b) Branching
METHOD
TIME (SEC)
Figure 6: OOD Detection. Green: Empirical ID inputs (1 million samples). Blue: border of the verified preimage. Branching is union of preimages for each quadrants.
MILPP
NO
1.47
1562.26
INVPROP
NO
4.39
3.77 + 0.02
INVPROP
YES
1.14
12.02 + 0.06

---

set of inputs). Our work strietly generalizes bound propagation as presented in Xu et al. 2021 since setting Y O in Theorem Saareem/rrevveee recovers its results.
Formal Analysis of the Input Domain Prior work has studied trying to determine the inverse of a neural network [Kindermann and Linden 1990] [Sadd and Wunsch, 2007], though these methods are prohibitively slow. Zhang et al. [ [018b] used an LP solver to compute changes to a given input that would lead to change in the classification result while adhering to additional criteria. Yang et al. [2021b] encode the overapproximated network in an LP problem to tighten bounds by incorporating the output constraint. They require an LP solver and we compare our performance against theirs in Section 4.2 Zhong et al.
2023 Wu et al. 2022] similarly tighten intermediate bounds by using an LP solver. Dimitrov al.
2022 compute input regions that only consist of adversarial examples (i.e., adhere to given output constraint) that are maximized using an LP solver. Finally, a concurrent work Zhang et al. [2023] targets under- and over-approximating the preimage via LiRPA-based forward verification Xu et al. 2020] with input-space and ReLU-space partitioning: since our work can be viewed as a generalization of LiPRA, their work may benefit from our results of tightening the intermediate layer bounds using output constraints during bound propagation.
Formal Verification for Neural Feedback Loops. Our control application was motivated by the growing body of work on backward reachability analysis and ver-aiprox states that result in a target set (Everett et al. 2021]. The original method solely utilized input constraints for deriving intermediate bounds. The later development of Everett et al. 2022 improved upon this by optimizing (()) and (0) with respect to output bounds but their implementation faces numerical instability when applied for many iterations. We also support the partitioning over the input space introduced by Rober et al. The work of Vincent and Schwager [021] explores utilizing an LP with complete neuron branching to verify control safety, which can be viewed as domain-speciffe implementation of our MILP formulation of the inverse verification problem.
Certified OOD detection. There is a wide variety of OOD detection systems Yang et al. 202 la
Salchi al.
2022]. Commonly, they are evaluated empirically based on known OOD data Wang it al. 2022 Liang et al. 2018 Chen et al., [021]. Therefore, they fail to provide verified guarantees for their effectiveness. In fact, many OOD detection systems are susceptible to adversarial attacks
[Sehwag et al.) 2019 Chen et al. 2022]. Meinke et al.] [202T] show how to verify robustness to
adversarial examples around given input samples. |Berrada al. 202T develop a general framework for certifying properties of output distributions of neural networks given constraints on the input distribution. However, this work still constrained to verifying properties of the outputs given constraints (albeit probabilistic) on the inputs, and INVPROP is able to certify arbitrary regions of the input space that lead to confident predictions.
6 Discussion
We present the challenge of aver-approximatin neural network preimages and provide an efficient algorithm to solve it. By doing so, we demonstrate strong performance on multiple application areas. We believe there a large scope for future investigation and new applications of INVPROP.
Limitations For higher-dimensional instances, our method would best work for box over- approximations (2d hyperplanes in d dimensions) and would struggle at more complicated shapes such as spheres. We expect more complex problems will benefit from a domain-speciie -ppaaifi strategy. Moreover, iteratively refining all of the intermediate bounds utilizing INVPROP faces quadratic dependence on network depth, as opposed to a linear dependence traditional forward verification. To mitigate this, output constraints could only be applied layers close to the output, for robustness. Finally, our branching strategy might not scale to higher dimensions, though this trade-off is well-studied [Bunel et al. 2020
used
Wang et al., 2021 Palma et al.) 2023
Potential Negative Social Impact Our work improves reliable ML through facilitating systems that provably align with practitioner expectations and we expect INVPROP to have positive societal impact. We acknowledge that our improvements may be repurposed as model attacks, though we believe the positive use cases of our technique greatly outweigh current speculation of misusage.
We thank Michael Everett and Nicholas Rober for helpful discussion and feedback on the paper. Huan Zhang acknowledges the support of the Schmidt Futures A12050 Early Career Fellowship.
Acknowledgements
10

---

References
Leonard Berrada, Sumanth Dathathri, Krishnamurthy Dvijotham, Robert Stanforth, Rudy R Bunel, Jonathan Uesato, Sven Gowal, and M Pawan Kumar. Make sure you're unsure: A framework for verifying probabilistic specifications. Advances in Neural Information Processing Systems, 34:
11136-11147, 2021.
Stephen Boyd, Stephen P Boyd, and Lieven Vandenberghe. Convex optimization. Cambridge University Press, 2004.
Christopher Brix. Vnn-comp 2023 benchmarks. https///tttiiicmmoomssshshhhhhha benchmarks 2023.
Christopher Brix, Mark Niklas Müller, Stanley Bak, Taylor T. Johnson, and Changliu Liu. First three years of the international verification of neural networks competition (ynn-comp), 2023. URL
https://arxiv.orr/ab///// 23001551111
Rudy Bunel, P Mudigonda, Ilker Turkaslan, P Torr, Jingyue Lu, and Pushmeet Kohli. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 21 (2020), 2020.
Jiefeng Chen, Yixuan Li, Xi Wu, Yingyu Liang, and Somesh Jha. Atom: Robustifying out-of- distribution detection using outlier mining. In Proceedings of European Conference Machine Learning and Principles and Practice of Knowledge Discovery in Databases (ECML PKDD), 2021.
Jiefeng Chen, Yixuan Li, Xi Wu, Yingyu Liang, and Somesh Jha. Robust out-of-distribttion detection for neural networks. In The AAAI-22 Workshop Adversarial Machine Learning and Beyond, 2022. http:://oppoereeeee..rtttotoonnn _Dz
Dimitar Iliev Dimitrov, Gagandeep Singh, Timon Gehr, and Martin Vechev. Provably robust ad- versarial examples. In International Conference Learning Representations, 2022. URL http:pppeeeeeeeeeee///oo/omiiiii
dual approach to scalable verification of deep networks. In UAI, volume 1, page 3, 2018. Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy A Mann, and Pushmeet Kohli. A
Ruediger Ehlers. Formal verification of piece-wise linear feed-forward neural networks. In In- lernational Symposium on Automated Technology for Verification and Analysis, pages 269-286.
Springer, 2017.
Michael Everett, Golnaz Habibi, Chuangchuang Sun, and Jonathan P How. Reachability analysis of neural feedback loops. IEEE Access, 9:163988-163953, 2021.
Michael Everett, Rudy Bunel, and Shayegan Omidshafiei. Drip: Domain refinement iteration
with polytopes for backward reachability analysis of neural feedback loops. arXiv preprint arXiv:2212.046446 2022.
Timon Gehr, Matthew Mirman, Dana Machsler-Cohhe. Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. Ai2: Safety and robustness certification of neural networks with abstract interpretation. In 2018 IEEE Symposium Security and Privacy (SP), pages 3-18, 2018, doi: 10. 109/SP.2018 00058.
Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovic, Timothy Mann, and Pushmeet Kohli. On the effectiveness of interval bound propagation for training verifiably robust models. arXiv preprint 1810.12110, 2018.
Dan Hendrycks, Mantas Mazeika, and Thomas Dietterich. Deep anomaly detection with outlier exposure. arXiv preprint 18Xiv:1812.0444 046666, 2018
Haimin Hu, Mahyar Fazlyab, Manfred Morari, and George Pappas. Reach-sdp: Reachability analysis of closed-loop systems with neural network controllers via semidefinite programming. In 2020 59th IEEE Conference on Decision and Control (CDC), pages 5929-5934, 2020. doi: 10. 0DL11999DD442330220009992222

---

Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In International conference on computer aided verification, pages 97-117. Springer, 2017.
J Kindermann and A Linden. Inversion of neural networks by gradient descent. Parallel Computing, 14(3)277-286,, 1990. ISSN 0167-8191. doi: http::://oii.or///11/ 1rg (0016/0166-111190990000110001110 1-J. URL
Shiyu Liang, Yixuan Li, and R. Srikant. Enhancing the reliability of out-of-distribution image detection in neural networks. In International Conference on Learning Representations, 2018.
URL httpps//wpppneeeevvveee//o/uuuud VGkIxRZ
Alexander Meinke, Julian Bitterwolf, and Matthias Hein. Provably robust detection of out-of- distribution data (almost) for free. arXiv preprint arXiv:2106.04266, 2021.
Mark Niklas Müller, Christopher Brix, Stanley Bak, Changliu Liu, and Taylor T. Johnson. The third international verification of neural networks competition (ynn-comp 2022): Summary and results, 2023.
Alessandro De Palma, Rudy Bunel, Krishnamurthy Dvijotham, M. Pawan Kumar, and Robert Stanforth. Ibp regularization for verified adversarial robustness via branch-and-bound, 2023.
Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Kopf, Edward Yang. Zachary DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala. Pytorch: An imperative style, high-performance deep learning library. In Advances in Neural Information Processing Sys- tems 32, pages 8024-8035, Curran Associates, Inc., 2019. URL http://papers htt-pyoooochaa--mpprratti------e
http::/ppapers.ncurpss.o wwwrips.cc/papppce... learning------------ learning- library.pdff
Aditi Raghunathan, Jacob Steinhardt, and Percy Liang. Certified defenses against adversarial examples. arXiv preprint arXiv:1801.09344 2018.
Joseph Redmon and Ali Farhadi. YOLO9000: better, faster, stronger. CoRR, abs/1612.08222,, 2016. URL http://arrii.oor//ab///111.....0
Nicholas Rober, Michael Everett, Songan Zhang, and Jonathan How. A hybrid partitioning strategy for backward reachability of neural feedback loops. arXiv preprint arXivv2210.07918, 2022a.
Nicholas Rober, Sydney M Katz, Chelsea Sidrane, Esen Yel, Michael Everett, Mykel Kochenderfer, and Jonathan P How. Backward reachability analysis of neural feedback loops: Techniques for linear and nonlincar systems. arXiv preprint arXiv:2209.14077 2022b.
Emad Saad and Donald C. Wunsch. Neural network explanation using inversion. Neural Networks, 20(1):78-93, 2007. ISSN 0893-6080. doi: http:://doi.org/1001000 101
http:///wwr.......oooeeeeeeee..0 www.eet.2006007.00000 URL
Mohammadreza Salehi, Hossein Mirzaei, Dan Hendrycks, Yixuan Li, Mohammad Hossein Rohban, and Mohammad Sabokrou. A unified survey on anomaly, novelty, open-set, and out of-distribution detection: Solutions and future challenges. Transactions on Machine Learning Research, 2022.
URL
Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang. A convex relaxation barrier to tight robustness verification of neural networks. Advances in Neural Information Processing Systems, 32, 2019.
Vikash Sehwag, Arjun Nitin Bhagoji, Liwei Song, Chawin Sitawarin, Daniel Cullina, Mung Chiang, and Prateek Mittal. Analyzing the robustness open-world machine learning. In Proceedings of the 12th ACM Workshop on Artificial Intelligence and Security, AlSec'19) 19, page 115-116, New York, NY, USA, 2019. Association for Computing Machinery. ISBN 9781 458146936..39 doi: 10.1 10.1145/33885013335333 URL URt.mp////oooorr/000155155555513
12

---

Wang Shiqi, Kexin Pei, Whitehouse Justin, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks. In 32nd Conference on Neural Information Processing Systems (NIPS), Montreal, Canada, 2018.
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianche and R. Garnett, editors, Advances in Neural Information Processing Systems. volume 31. Curran Associates, Inc., 2018. URL 01146608008e9777e11rss7777ffa
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks, Proc. ACM Program. Lang., 3(POP), jan 2019. doi: 10.1145/329035.
URL https://doi.orrg org// 101.1111444/29554
Vincent Tjeng, Kai Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. arXiv preprint arXiv:1711.07356 2017.
Joseph A. Vincent and Mac Schwager. Reachable polyhedral marching (rpm): A safety verifi- cation algorithm for robotic systems with deep neural network components. In 2021 IEEE International Conference on Robotics and Automation (ICRA), pages 9029-9035, 2021. doi:
Haoqi Wang. Zhizhong Li, Litong Feng, and Wayne Zhang. Vim: Out-of-distributioo with virtual- logit matching. In Proceedings of the IEEF/CVF Conference on Computer Vision and Putlern Recognition, 2022.
Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. Advances in Neural Information Processing Systems, 34, 2021.
Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. In International Conference on Machine Learning, pages 5286-5295. PMLR,
2018.
Haoze Wu, Clark Barrett, Mahmood Sharif, Nina Narodytska, and Gagandeep Singh. Scalable verification of gnn-based job schedulers. Proc. ACM Program. Lang., 6(0OPSLA2), oct 2022. doi: 10. 10.1145/3563325. URL https://bb..rrg111.1145555555553
Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai- Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsich. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information P Processing Systems, 33, 2020.
Kaidi Xu, Huan Zhang. Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. Fast and Complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In International Conference Learning Representations, 2021. URL
https://ppenreviewwee///oo VZXXBIGN
Jingkang Yang, Kaiyang Zhou, Yixuan Li, and Ziwei Liu. Generalized out-of-distribution detection: 2021a.
A survey. arXiv preprint 2
Pengfei Yang, Renjue Li, Jianlin Li, Cheng-Chao Huang, Jingyi Wang, Jun Sun, Bai Xue, and Lijun Zhang. Improving neural network verification through spurious region guided refinement. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 389-408, Cham, 2021b. Springer International Publishing. ISBN 978-3-030-72016-
Huan Zhang, Tsui- Wei Weng, Pin- Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. Advances in Neural Information Processing Systems, 11:4939-4948, 2018a. URL httpps://arxiv.or//pdd/i
1.00:// 1.08666.6011
Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. General cutting planes for bound- proppddtopagtiin--aae bbase neural network verification. Advances in Neural Information Processing Systems, 2022.
13

---

Xin Zhang, Armando Solar-Lezama, and Rishabh Singh. Interpreting neural network judgments via minimal, stable, and symbolic corrections. S. Bengio, Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett, editors, Advances in Neural Information Processing Systems, volume 31. Curran Associates, Inc., 201 URL httpp://pocceeddiggg...uuipppppp hapepp//pprrrilspppeprreeep 2018/hle/30089 a62 a222112222200000000222222222bbb3
Xiyue Zhang, Benjie Wang, and Marta Kwiatkowska. Provable preimage under-approximation for neural networks. arXiv preprint arXiv:2505.033666, 2023.
Xiangru Zhong. Yolo-benchmark. https//ggihbbb.omm/iiggguuuu/ubo
2023.
Yuyi Zhong, Quang-Trung Ta, and Siau-Cheng Khoo. Arena: Enhancing abstract refinement for neural network verilication. In Cezara Dragoi, Michael Emmi, and Jingbo Wang, editors, Verification, Model Checking, and Abstract Interpretation, pages 366-388, Cham, 2023. Springer Nature Switzerland. ISBN -77-3-003-24950-1
14

---

A OOD Detection
Training data
Logit Gap Heatmap
class
Class
-2
-2
Figure 7: To improve our model's ability to detect data outside the training distribution (of green and red points), we randomly sample points that are far from every training point. In the right contour, we see that the model's confidence of in-distribution increases as we approach the centers of the distribution, demonstrating model is more calibrated.
For the OOD benchmark, we train a neural network on two clusters of data. Standard training add in OOD data through sampling the input space and
would lead an uncalibrated predictor, rejecting inputs that are too close to any training data point. Training a classifier on this dataset induces the contour the right, which is a calibrated classifier we can certify properties over. For our experiments, we consider high-confidence output as 90% confidence of the data being in-distribution.
B Example
Example 1. Consider the toy neural network in Figure under = [- and Saut = (y:1
1.02). Suppose wanted to find the tightest I2(), uo (bounds (1) If we only enforce the constraints preceding the ReLU (standard bound propagation), we get [-2, 2]. we only enforce the constraints following the ReLU, we get (-o0, 1.02]. However, when utilize all of the constraints, we find that the true intermediate bounds are [0, 0.01], which is over 100 times tighter than the intersection of the two previous methods (all derivations provided below). Therefore, techniques are necessary for optimizing intermediate bounds in this setting.
B.1 Deriving Intermediate Bounds for Example
()) Since the only constraint have is 2 E [[ 2], the tightest intermediate bounds we can derive are [- 2].
Preceding Constraints.
The linear layer gives z (1)
(0)
Following Constraints. Since the output of ReLU is non-negative, know that a:1) ..(1.) 0. Since an = -00 + (1) and the output constraint enforces a/ < 1.02, we derive that # < 1.02. that ( can take the entire interval [0, 1.02). Since the only
If set a0) 1.02
constraint we have on wi is that ReLU(e (1) (1), ) our desired interval is the preimage of [0, 1.02].
(1)
(1) This means that m/ can take any value the interval (-oc, 1.02].
(1) + 1. Therefore, if All Constraints. We first note that by the first linear layer, we have 20 2
2 (I) is less than 0, then (1) less than 1, which means ReLU(z) ReLU(z is less than which contradicts the output constraint. If x
(1) is always non negative, then we have that the output equivalent to ReLU(2)()) (2) ReLU(x;() + 2x Therefore, the output constraint implies
(1) z < 0.01. Any 2 [0, 0.01] is achievable by setting the input to the desired value.
(1)
15

---

(1)
ReLU
zp
$0
(2)
40
(1)
ReLU
11
Figure 8: A simple neural network from R to R. Every node is the sum of its incoming nodes unless the edge is labeled ReLU.
C Optimizing Intermediate Bounds
We present generalized theorem which provides a lower bound for any linear combination of à (0) and (+), We prove this theorem in Appendix D We note that by selecting the coefficients of these variables (named ( for E {0, 1...., 11), we recover the two following functionalities which we name (e 7) and g¹. (ax, 7) (respectively).
When the only nonzero coefficients are ( = c, we recover Theorem bound (e( 7)
We refer to this 1, we can lower bound 1 by gig gl (a, (a, 7). If
When the only nonzero coefficient is oj we set oj 1, we can upper bound u by Ru.jer (ax, 7).
With this, present generalized theorem.
Theorem 2 (Lower-bounding combination of neurons). Given an output set Sow = -y Hy+d < <0} and vector c, g( 7) is lower bound to the linear program in (3) with objective c ((()
ΣL- T for 0 s a s 1, 7 O, and defined via
g(a, = [(OOT (O)Tw()) (10)
[ -D T(T) (0)
10
(
Σ
u, (5) 15
jEZ+
where every term can be directly recursively computed via
I {j: : u < 0}
(+) (j:13 0}
=1) (j 14 <0 (
(()) -
2 (++)T (++)
2 :0
j E (+
1
j ( (0)
a
11
13) (8)
(6)
j I+(0
10)
16

---

D Dual Derivation
We first incorporate the output constraint Hz + 0 by folding this linear transformation of the output into the final linear layer of the network, customary in prior work [Wang al. 2021 Zhang ct al. 2022].
We now prove the generalized theorem as described in As a conceptual overview of our proof, we take the Lagrange dual of the linear program derive unconstrained optimization problem. From here, we derive constraints that must be satisfied in the max min formulation. These constraints yield the bound propagation procedure we display in Theorem 1 We start with the convex relaxation.
L-1
(0) 4 (0)
Σ
( (1)
min
2,
(0) 2 (0) (
s.t.
x (L) < 0
1 W (i-1) + bb,);
ie (4],
8/ 2 0:j E I=
8/ 2 2) 10 11 =
(u) 19)0)) su (1)
16 I+(0)
8) =j 1
2) = 0: (1
From this, we take the Lagrange dual most of the constraints. In doing so, introduce new dual variable for each constraint. Note that we do not dualize every constraint since they can easily be dealt with later.
L-1
L
(0) (0)) ())
(1)
T (D)
+ Σ
((T (z -w(()(0) -b()) -b())
min max P.
i=1
1=1
+
-1 + (8) (1)
(1)
(1)
- =100) 1110 (luf) - -100 )a!"
m 2 (1) + u [0)
i=1 jEI+(1)
s.t. (0) < (0)
< u (0)
3/ =0 0 210 = 1. . E
1 2 0;
T +20;
720; A20
Since we took the dual of a linear program, the solution to the min-max optimization is equivalent to the solution of the max-min optimization by strong duality. Therefore, we can solve the following program (cquivalent up rearrangement).
17

---

(vll) +7) x(1) + (c - -uOt waa) 210)
max min P. 2,
4-1
Σ
- (1n)
(v(0)
- (10) 2/
Σ
(v5 + x
+
i= (e
jEZ
4-1
+
+
1
(EI+(1)
(6+1)
w
W((+t)
(0
19)))))))))
1-1
Σ DOT ((0)
Σ
Σ 5
==1
S.t. 1 < a S uu!) (0)
# 2 0;
t 2 0:
720; A20
To minimize (c(²)T (I) W()) a (0) subject to 1 < (0) S {0) we can consider the choice must make in each dimension. If the jth entry of the coefficient is positive, we should set ((00) (() Otherwise, we should set 5000 = u
(el)+t) x(()+ [c(OT DDOT w(] (00) [c(OTT - -OTT ())
max min M.H.T,7.A ø.
1-1
L-1
(1(0) ((+1)
Σ
Σ (u)) + c (1)
2
jEI-(1)
jEz-
+ (10+++0~~00+++)))
(1) (000
jEIZ())
(
w
w(i+!)
(
1-1
Σ
ELOTT
(0)
Σ Σ
1=1
i=1 jez=(0
s.t. p 2 0;
T T2
0;
720; A20
From here, we note that the variables & or å are unconstrained variables. Therefore, if any of their coefficients are nonzero, the inner minimization can immediately drive its value to -cc. As such, the outer maximization must set all of these coefficients to zero. Therefore, we can derive constraints from this restructured optimization and remove the free variables ă.
18

---

c!O)T D(U) [ (0)
- (()) 0
Σ T
max P.U.T,Y.
1-1
+ Σ
Σ
1/0 1
im jEIZ())
((4) -7
s.t.
1/ = (++)T W(++1) (++1)
W
( -
1/ (10 = oj .j E
(6) = 1 (9, 4 - 5/ 9 jJ I=
(1)
1/
((+1))T W
(1+1) 9 1/ (4) + +7, (1)
2 (u)
(1)
. I=
1 0: T 0; 7 72 0; X20
For the following, we define of0 ((+ ( We note that since the upper and lower
bounds of the neuron relaxation can not be tight simulataneously, at least one of (u (5) (()) }
(e)
(i)
write them as (u, ) [0 10/[1+ 1+ and
and H4j + Tj must be non-zero. Therefore,
Mi + T (1) 1_ We then use the fact that 7/ lies in the interval 0 and 2/()) to get the
(5)
following bound propagation procedure.
(0) -00TT~0000 22) way 100)
[ -D0T BDTTaa u()) Σ b
max 2,007
T-11
1 10
my
+
u. ()) ((0
1= (c)=
(1)
s.t.
(+IT w(+1) - 0 E
1
/ = 3 .j EI-( (1)
0 = (H+)T w (++)
10
"
++ a3 10
10
20. E
I+(1)
03 0 (10
0j E 0011: 0
In this program, aj are optimizable parameters controlling the relaxation of neuron j in layer i, similar to the ones appearing in Xu et al. 2021 7, as discussed in the body of the paper, is the parameter which enforces the output constraint throughout this entire bound propagation procedure.
E Connection to Forward Verification for Intermediate Bounds
We consider the general objective presented in C and aim to minimize () a
-!-1 (()
min (0) (0
OT i
s.t. ;;
Hf a + d 50
If we take the dual of the constraint, then we get the program
19

---

1-1 e T (0) + +- (Hf(x)) + +d)
min (
S.L. x ZE Y 2
We note that the objective here can be expressed as neural network with residual stream f()) and skip connection with linear weight c(9) from the pre-activations of layer to the final output for every layer. In theory, we could construct this neural network and directly pass a forward verification tool which could iteratively tighten all bounds for solution.
F Implementation
As stated in Algorithm T INVPROP first initializes bounds for all layers using some computationally cheap technique. Based on the input bounds given by X, we first compute intermediate bounds using interval propagation and then tighten them based the reverse symbolic interval propagation (RSIP) technique (Singh et al. 2019). While INVPROP will iteratively tighten those bounds over time, we found RSIP to reduce the total necessary runtime significantly compared an initialization based solely on interval propagation. We initialize all a with 0.5 and all y with 0.025.
The optimization is performed for all lower and upper bounds of all neurons in each layer in parallel, starting with the last layer and moving forward to the input layer. The bounds of the cutting hyperplanes are optimized last, together with the bounds on the input neurons. The improvements on x are measured every 10th iteration. Before doing so, the bounds of the hyperplanes are tightened for 10 extra steps to improve their precision. We detect convergence by monitoring e æ. If successive iterations see minimal improvement, we stop or branch on the input space. All cutting hyperplanes are evenly distributed to maximize their information gain. For 40 hyperplanes in 2D input space, we rotate each plane by 9 All reported runtimes under 10 minutes are computed as the average of five runs.
F.1 Encoding Non-Linear Constraints
To support non-linear output sets, such as the maximum operation used in the OOD example in Section the non-linearity needs be encoded, such that it can be expressed as linear constraints over the modified network. We rewrite max(U1, V22 max(y) y/, 0) + 1/2 and add an additional ReLU layer for this operation. Note that to pass y22 through this layer without modifying it, one can either write 1/2 = max 0) max 0), 3/2 = max(y2 M, 0) + M where M is the lower bound of all possible y2- We find that avoiding the additional ReLUU relaxations that would occur for the first approach is beneficial for the optimization and compute lower bound of M using interval propagation. As ya (for the OOD class) should not be changed by this operation either, we apply the same trick of subtracting and adding its lower bound.
F.2 Control Benchmark Encoding
We encode the entire control formula x = Ax + Bu as one feedforward network by encoding the residual connection as regular fully connected layers. To this end, we use the same technique described in Section F.I to shift the bounds into the positive regime, feed them forward and then shift them back.
To compute Sover for a timestep t >> 1, we first stack the network t times, then simplify it by merging consecutive linear layers. All bounds of layers not affected by this merging that also appear in the network for t - 1 timesteps are reused. Their bounds are already tight enough and are not optimized further. Note that this is different than using the previous Sover the new target region and using an unstacked network: All bounds of the new layers are still optimized w.r.t. the precise target Soat Therefore, do not suffer from accumulating inaccuracies.
G Hardware
For the control benchmark, all experiments were performed on Dual Xeon Gold 6138. For the OOD benchmark, all experiments were performed on an Intel Xeon Platinum 8160 processor using 8 cores and 40GB RAM, well as V100-SXM2 GPU.
20

---

100
One Minute
10
0.1
a. a. CROWN + INVPROP a.B-CROWN
0.01
20
40
60
80
100
120
140
160
Number of Instances Verified
Figure 9: Detailed runtime comparison of a,,3CRROWN and a,d-CROWN + INVPROP. Except for few instances, a,9-CROWN extended with INVPROP can verify the properties faster, and can prove robustness for some instances that cause timeout for pure a,3-CROWN, The timeout per instance 5 minutes.
For the MNIST and YOLO robostness verification benchmarks, an AWS instance type g5.2xlarge used, with is equipped with AMD EPYC 7R32 processor with 8 cores, 32GB RAM,, well as an A10G GPU.
H Robustness Verification
For the comparison in Section 4.2, we have implemented the concept of INVPROP in a,,-CRRWN. Figure compares the performance of a.8-CROWN and a,3-CROWN INVPROP the MNIST benchmark defined by Yang et al. 2021bb
21


Reviews:
[{"review_id": "FFtg4YdfkG", "reviewer": "Reviewer_bSxe", "summary": "The paper considers the problem of computing approximations of the set of\ninputs for which a given neural network satisfies certain output constraints.\nTo solve the problem, the paper discusses adaptations of a number of approaches\nfrom standard neural network verification, including MILP and LP formulations,\nand motivates the development of bound propagation methods and optimisations of\nthe Lagrangian duals. Experimental results of the resulting method are reported\non (i) backward reachability analysis for neural feedback loops; (ii) OOD\nDetection; (iii) robustness verification.", "questions": "Could you please discuss the overhead of the incorporation of the output\nconstraint to forward verification when larger, i.e., with millions of ReLU\nnodes, networks are considered?\n", "limitations": "Adequately addressed.", "rating": 7, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "The problem studied is well motivated and its applicability is sufficiently\nexemplified.\n\nThe adaptation of the α,β-Crown method to solve the problem is novel.\n\nThe efficacy of the resulting method is evaluated on a range of benchmarks,\nwhere it is shown to outperform the state-of-the-art in backward reachability\nanalysis. The connection of backward propagation to standard forward\nverification is brilliant to see, especially its utilisation towards more\nefficient forward verification.", "weaknesses": "The contribution is incremental to the α,β-Crown method.\n\nAt its present stage the method is limited to low-dimensional networks. Also,\nno scalability is discussed with respect to big (but still low-dimensional)\nnetworks.\n\nAn important feature of the α,β-Crown framework on which the method is based,\nnamely node branching, is not discussed but left as future work, thereby giving\na \"preliminary\" feel to the paper.\n", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for the helpful feedback! Thanks to your review, we have run more expansive evaluations (including **8112-dimensional inputs** and **167k neurons**), **fully implemented branching** from abCROWN with INVPROP, and improved our discussion of limitations.\n\n> At its present stage the method is limited to low-dimensional networks. Also, no scalability is discussed with respect to big (but still low-dimensional) networks.\n\nIn light of these suggestions, we have run new experiments to highlight the strength of our method. In the verified robustness setting, our method handles 8112-dimensional inputs for 167k neuron networks. In the control setting, our method handles a 6-dimensional quadrotor control problem. Furthermore, we provide more details on scalability across dimensions/neurons/branching in our new limitations section. Please see our new results and limitations in our general response and PDF.\n\n> The contribution is incremental to the α,β-Crown method.\n\nThough INVPROP builds on the alpha-beta-CROWN framework, we believe that this work represents many significant technical contributions such as iteratively refining intermediate bounds, incorporating constraints sequentially after a layer’s intermediate bounds, and leveraging constraints on the output layer. None of these were supported by existing alpha-beta-CROWN, and INVPROP enables tight verification for novel applications such as control, and tightens bounds for existing robustness verification problems.  Since we’re compatible with the framework, we can easily leverage existing state-of-the-art verification tools, as shown in our new adversarial robustness verification experiments.\n\n> An important feature of the α,β-Crown framework on which the method is based, namely node branching, is not discussed but left as future work, thereby giving a \"preliminary\" feel to the paper.\n\nIn our new experiments, we have integrated INVPROP with alpha-beta-CROWN and **fully implemented branching** over neurons and inputs. Utilizing Branch and Bound for verification is independent of this work, and the trade-off between the tightness of verification and computational constraints is well-studied in prior literature.\n\n> Could you please discuss the overhead of the incorporation of the output constraint to forward verification when larger, i.e., with millions of ReLU nodes, networks are considered?\n\nIn our new limitations section, we discuss how the output constraint scales with neural network size. Specifically, using the output constraints for tightening the intermediate bounds for every layer incurs a quadratic dependence in runtime, but we can use our framework for tightening a single layer and still see the benefits, as seen in our new evaluation results for the YOLO benchmark in VNN-COMP 2023.\n\n—\n\nWe hope that we’ve addressed the proposed concerns and would be more than happy to answer additional questions! \n"}, {"review_id": "nLZk5oaSgf", "reviewer": "Reviewer_PXif", "summary": "The paper considers verified neural network inversion. Given a set of output values, the goal is to compute the pre-image of these, i.e., the inputs that lie within this output set (given as a linear constraint over the output space).\nTo address this, the authors propose INVPROP, an algorithm that computes \nan over-approximation of the convex hull of the pre-image.\n\nThis set is represented as the intersection of multiple half-space constraints.\n\nGiven a direction vector finding the corresponding half-space constraint can be phrased as an optimization problem. Formulating this as a mixed-integer linear program (MILP) allows to recover a tight convex hull (assuming enough direction vectors are used). To improve efficiency at the cost of tightness this MILP can be relaxed into a LP. This is similar to the same problem in standard forward verification, however, in contrast to there, a constructive closed-form solution to the LP is not available.\n\nInspired by the CROWN verification algorithm the authors propose to consider the dual of the LP. This formulation allows to obtain a lower bound of the LP and thus a over-approximation to the convex hull. This approach, termed INVPROP, now can be solved by traversing the neural network back-to-front and obtaining neuron bounds via gradient ascent.\nAs in forward verification, this can be tightened by branching the problem and obtaining bounds for sub-problems.\n\nINVPROP is evaluated: on backward-reachability for neural control policies, out-of-distribution detection, and robustness verification (combined with a forward verification algorithm), where it achieves strong results.\n", "questions": "- What is $z$ in (2a)? Is it a typo and not needed for the optimization problem?\n- Line 267 refers to Figure 4 which is just found in the appendix.  Even with the Figure the description in line 267/268 is not clear to me. Can you clarify the setting in the OOD approach?\n- Can you discuss the scalability of the approach? What are the key limiting factors? How large is the role of the input dimensionality? Ideally, this is also shown through further experiments, but I understand that this is hard within the constraints of the rebuttal.\n\n\nEDIT POST REBUTTAL: My questions have been answered, thereby addressing the above weaknesses. I have thus updated my score.", "limitations": "There is some discussion of limitations though it is not very clear to me what the key limiting factors, e.g. on the scalability of the approach are. (See questions.)\nSocietal impact is discussed in a manner appropriate to the paper.", "rating": 7, "confidence": 4, "soundness": 4, "presentation": 2, "contribution": 3, "strengths": "- Creative and Novel Approach\n- The mathematical results appear sound and well motivated\n- Good empirical results, though -- other than the improvements in certified robustness -- on niche benchmarks and settings\n- Well connected with related and prior work", "weaknesses": "- While overall quite easy to read/follow, the presentation appears a bit sloppy and rushed \n- There is no discussion of the limitations and scalability of the approach, other than the mention of per-neuron branching\n- While the evaluation highlights why the approach is useful, it does not provide a good understanding of the limitations of the approach, i.e. the first two tasks are rather low-dimensional and the verification task is only discussed very briefly\n\nSee the below questions for more details and addressable points.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for the helpful feedback! Thanks to your review, we have run more expansive evaluations (including **8112-dimensional inputs** and **167k neurons**), extended our reachability analysis to a **6-dimensional state quadrotor**, and improved our discussion of limitations.\n\n> Can you discuss the scalability of the approach? What are the key limiting factors? How large is the role of the input dimensionality? Ideally, this is also shown through further experiments, but I understand that this is hard within the constraints of the rebuttal.\n\n> While the evaluation highlights why the approach is useful, it does not provide a good understanding of the limitations of the approach, i.e. the first two tasks are rather low-dimensional and the verification task is only discussed very briefly\n\nIn light of these suggestions, we have run new experiments to highlight the strength of our method. In the verified robustness setting, our method handles 8112-dimensional inputs for 167k neuron networks. In the control setting, our method handles a 6-dimensional quadrotor control problem. Furthermore, we provide more details on scalability across dimensions/neurons/branching in our new limitations section. Please see our new results and limitations in our general response and PDF.\n\n> There is no discussion of the limitations and scalability of the approach, other than the mention of per-neuron branching\n\nWe agree with the reviewer that we have not adequately discussed our limitations with respect to how INVPROP as well as node branching scales with size. We have rewritten a more comprehensive limitations section, which we provide in the general response. We hope this addresses the concerns raised in this regard.\n\n> What is z in (2a)? Is it a typo and not needed for the optimization problem?\n\nThank you for spotting this typo, we have fixed it.\n\n> Line 267 refers to Figure 4 which is just found in the appendix. Even with the Figure the description in line 267/268 is not clear to me. Can you clarify the setting in the OOD approach?\n\nWe agree that we have not properly introduced the OOD setting, and we add the following section to our Appendix to properly describe the exact setup in this case.\n\nA simple approach to train a classifier that “knows when it doesn’t know” is to train a classifier with an additional logit representing (out of distribution) OOD-ness. Labeled data for this additional class is generated via outlier exposure, i.e., adding synthetic training data with features drawn from an OOD distribution (known as outlier exposure [1]) and labels corresponding to the additional OOD logit [2]).\n\nConsider the logits $y$ produced by a classifier trained in this manner for a binary classification task. The classifier can classify in-distribution data by comparing $y_0$ and $y_1$, the logits corresponding to the two in-distribution labels. The quantity $\\max(y_0, y_1) - y_2$, known as the logit gap, can be used to identify out-of-distribution data (Figures 3 and 4).\n\nA natural question to ask is: Can it correctly identify data points far from the training data as being OOD? In order to do so, one needs to compute the preimage of the set $\\mathcal{S}_{\\text{out}} = \\{y : \\max(y_0, y_1) \\geq y_2\\}$. We detail how to model this set with linear constraints in Appendix F.1. INVPROP enables us to compute an overapproximation of the pre-image, thereby answering the question of whether the classifier learned to correctly identify OOD data.\n\nIn the OOD example, the model was trained to distinguish three classes. Two are defined by the two classes in Figures 3 and 4. The third class represents “out-of-distribution” inputs. All inputs outside of the two circles should be assigned to the OOD class.\n\n> While overall quite easy to read/follow, the presentation appears a bit sloppy and rushed\n\nThank you for your feedback in this regard! We would love to improve our presentation and would appreciate further concrete suggestions on what sections could use the most help. \n\n—\nWe hope that we’ve addressed the proposed concerns and would be more than happy to answer additional questions! \n\n[1] Deep anomaly detection with outlier exposure, D Hendrycks, M Mazeika, T Dietterich\n[2] ATOM: Robustifying Out-of-distribution Detection Using Outlier Mining, Jiefeng Chen, Yixuan Li, Xi Wu, Yingyu Liang, Somesh Jha\n"}, {"review_id": "EtRR6AiZXv", "reviewer": "Reviewer_K762", "summary": "The authors propose INVPROP, an algorithm for constructing certified bounds on the pre-image of neural networks with ReLU activations. The method constructs a convex over-approximation of the pre-image by implicitly optimizing the dual relaxation of a MILP problem. Empirical evaluation shows considerable improvement over the state of the art.", "questions": "Line 77. Why is inverting a neural network an intractable problem? It is clearly possible to compute it, albeit expensive to do so. In the end, f is a Lipschitz-continuous function, thus locally invertible.\n\nAfter line 89, why is the first matrix not the identity? Surely the robot cannot teleport on the x_1 dimension. Also, why can the policy only control diagonal movement along the line [0.5, 1]? If these numbers are chosen just for illustration\npurpose, then why presenting the \"robot in a 2d environment\" story altogether?\n\nHow are the concrete bounds [l,u] computed? Algorithm 1 says \"cheap bound propagation\", but these are only applicable for the forward verification problem. how to compute them for a general problem?\n\nAt Line 166, the proposed bounds yield a parallelogram domain around ReLU(x), whose shape is regulated by z. Why not using the classic, traingular domain from DeepPoly? What are the advantages of your parallelogram domain here?", "limitations": "The authors are not up-front on the fact that c in Equation (1) is extracted at random. The problem of how to do so is finally discussed in Sections 4 and 7. However, it is not clear how the choice of c impact the tightness of the pre-image. More specifically, in line 247, sampling 40 random planes may be ok for this particular 2-dimensional problem. Similarly, I can see how this works well for the OOD task in Section 4.2. At the same time, it is unclear how well that works for the MNIST task in Section 5. The authors offer no comment about this therein.", "rating": 7, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "The authors' method is elegant and clear. Furthermore, I can see how it could be used as the baseline for many future works. Inverting neural networks is a notoriously difficult problem, and I commend the authors for proposing a workable solution.", "weaknesses": "The paper is dense to read at times, and the connection to existing works is often left to the reader. More specifically, most of the related work is presented at the end of the paper (Section 6). The state-of-the-art methods in neural network inversion (Rober 2022, Everett 2022) are mentioned for the first time in lines 249 and 256. Furthermore, no mention of earlier works in neural network inversion (see examples below) leave the reader with the feeling that this is a new problem that was never studied before:\n\n\tKindermann, Linden, 1990, \"Inversion of neural networks by gradient descent\"\n\tSaad, Wunsch, 2007, \"Neural network explanation using inversion\"\n\nI think the authors' contribution would shine even more if they introduced a little more historical perspective on the topic.\n\nWhile reading the paper, I found a few minor writing issues, which I list below. For more detailed algorithmic question, see the \"questions\" and \"limitations\" secvtions of this review.\n\nMany unnumbered equations make referencing difficult. See for instance lines 89, 144 and 166 in the main paper, lines 525-526 in Appendix E.\n\nLines 50-53. This contribution is difficult to parse without a strong understanding of ab-CROWN and local robustness problems.\n\nRobustness verification is presented in Section 5. Given the structure of the paper, I believe it should be in Section 4.3.\n\nLine 314, \"forumalation\" should be \"formulation\".\n\nAppendix E, the output domain weights H and d are not present in the proof, which I guess it is for clarity, but the authors do not acknowledge this.\n\nAppendix E, in lines 525-526 there is an extra term \\sum c^ix^i in the objective that is not explained.\n\nThe formatting of figures and tables in Section 4 is ugly. At least, all tables and figures in page 8 should be flushed to the top, in order to avoid having a piece of main text in between them.\n", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for the helpful feedback! Thanks to your review, we have run more expansive evaluations (including **8112-dimensional inputs** and **167k neurons**), improved our discussion of limitations, and better situated ourselves within prior work.\n\n> I think the authors' contribution would shine even more if they introduced a little more historical perspective on the topic.\n\nWe agree with the suggestion of better situating this approach within the context of prior work. We have added references to neural network inversion and discussed our relationship with this work.\n\n> Line 77. Why is inverting a neural network an intractable problem? It is clearly possible to compute it, albeit expensive to do so. In the end, f is a Lipschitz-continuous function, thus locally invertible.\n\nThank you for pointing this out, we tone down our claim to discuss how it is computationally difficult to compute the exact pre-image. Our original writing was discussing the fact that neural networks are not strictly invertible, but we agree that they are locally invertible.\n\n> After line 89, why is the first matrix not the identity? Surely the robot cannot teleport on the x_1 dimension. Also, why can the policy only control diagonal movement along the line [0.5, 1]? If these numbers are chosen just for illustration purpose, then why presenting the \"robot in a 2d environment\" story altogether?\n\nWe agree that the robot scenario does not properly highlight our story. We change this story to the DoubleIntegrator task we target later in the paper (since these dynamics are precisely the ones we verify in Section 4.1).\n\n> How are the concrete bounds [l,u] computed? Algorithm 1 says \"cheap bound propagation\", but these are only applicable for the forward verification problem. how to compute them for a general problem?\n\nWe supply our initial bounding box for the input domain, denoted $l^{(0)}, u^{(0)}$, to a forward verification algorithm as an input set to over-approximate. This allows us to initialize [l, u] for every layer with a loose over-approximation.\n\n>At Line 166, the proposed bounds yield a parallelogram domain around ReLU(x), whose shape is regulated by z. Why not using the classic, traingular domain from DeepPoly? What are the advantages of your parallelogram domain here?\n\nThe parallelogram domain is equivalent to the classic triangle domain from DeepPoly. This is simply a reparameterization of those bounds for mathematical convenience and compatibility with the GCP-CROWN paper (Zhang et al., 2023). When z is projected out, the relaxation becomes triangular. Using triangular bounds would cause no change in tightness and would only alter the formulation of our theorem.\n\n> The authors are not up-front on the fact that c in Equation (1) is extracted at random\n\n> it is not clear how the choice of c impact the tightness of the pre-image.\n\nIn our control and OOD example, we utilize 40 evenly spaced hyperplanes as mentioned in Line 247. The selection of hyperplanes is a domain-specific consideration and is a separate consideration from the INVPROP algorithm. In higher dimensional applications, using two planes per input dimension, the positive and negative unit vectors, gives a box over-approximation of the pre-image. We find that this scales well in practice for robustness verification tasks (as it offers improvements for robustness verification in dimension 8112 and control verification in dimension 6) and scales well in theory since the number of hyperplanes necessary would be linear in the input dimension. \n\n—\n\nWe appreciate the detailed analysis of our writing and agree with all of the minor writing issues. All of these issues will be addressed in a camera-ready version of this paper. We hope that we’ve addressed the proposed concerns and would be more than happy to answer additional questions!\n"}, {"review_id": "OZnPUcPfSP", "reviewer": "Reviewer_XnFH", "summary": "This paper presents a novel approach to bounding the preimages of neural networks using a sequence of relaxations. Results are provided for a toy controls problem and a robustness verification task.", "questions": "1. I am not sure why the controls benchmark task is referred to as a \"robot moving on the floor of a room.\" This is a double integrator task, as described in the cited work that originally presented the problem. Of course this can be considered a planar system with strange dynamics, but it's not clear why that would be done when the dynamics have a classic double integrator structure.\n2. I'm confused on the discrepancy between the reported results for the baseline method. Specifically, the approximation ratio of ReBreach is about 4000, which is orders of magnitude higher than what I would expect based on the results in the original paper (errors less than 10x the true volume). What is causing this discrepancy?\n3. In Figure 3, on the left side without input splitting, why is the convex hull so loose? I would expect it to tightly wrap around the green circles.", "limitations": "The main limitations are mentioned explicitly. ", "rating": 7, "confidence": 3, "soundness": 3, "presentation": 4, "contribution": 2, "strengths": "1. The paper addresses an important recent developement in the literature.\n2. The paper is well presented and motivated. I like the direct correspondence between the visualization in Figure 1 and the derivation of the method in Section 3.\n3. The proposed approach is novel and has some promising results for toy problems. I believe all the steps in the derivation of the approach are correct, although I have not checked them carefully.", "weaknesses": "1. My main concern is that the main experiment that the approach is evaluated on (reachability analysis) is very small (12 + 7 + 2 neurons), even by verification standards. It is true that these optimization-problem flavored verification approaches are generally evaluated on small networks, ab-CROWN for example can be evaluated for substantially larger networks on datasets like CIFAR-10. Given that these approaches incur exponential runtime with network size, I am skeptical that they can ever be relevant for networks of a practical size.\n2. Similarly, many proposed details scale poorly with input data dimension (as mentioned in the limitations). I believe that the number of sampled c would need to grow exponentially with input dimension, as would the branch-and-bound scheme.\n3. I recommend the authors tone down their presentation somewhat. In 2.2, it should be claimed that only an approximation of the convex hull is computed (not the exact convex hull). Also referring to the controls problem as an \"established benchmark\" is somewhat of a stretch as this is a recent unpublished preprint with only a couple citations.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for the feedback!  Thanks to your review, we have demonstrated our scalability through much more difficult robustness verification (including **8112-dimensional inputs** and **167k neurons**) and tested another reachability analysis problem of a **6-dimensional state quadrotor**.\n\n> Given that these approaches incur exponential runtime with network size, I am skeptical that they can ever be relevant for networks of a practical size.\n\nIn light of these suggestions, we have run new experiments to highlight the strength of our method. In the verified robustness setting, our method handles **8112-dimensional inputs** for **167k neuron** networks. In the control setting, our method handles a **6-dimensional quadrotor control** problem. Furthermore, we provide more details on scalability across dimensions/neurons/branching in our new limitations section. Please see our new results and limitations in our general response and PDF.\n\n> Similarly, many proposed details scale poorly with input data dimension (as mentioned in the limitations). I believe that the number of sampled c would need to grow exponentially with input dimension, as would the branch-and-bound scheme.\n\nThe selection of hyperplanes is a domain-specific consideration and is a separate consideration from the INVPROP algorithm. For example, in higher dimensional applications, using two planes per input dimension, the positive and negative unit vectors, gives a box over-approximation of the pre-image. We find that this scales well in practice for robustness verification tasks (as it offers improvements for robustness verification in dimension 8112 and control verification in dimension 6) and scales well in theory since the number of hyperplanes necessary would be linear in the input dimension. \n\nIn our new results, we integrate INVPROP with alpha-beta-CROWN and show that it works well in the case of robustness verification. Utilizing Branch and Bound for verification is independent of this work, and the trade-off between the tightness of verification and computational constraints is well-studied in prior literature. \n\nWe now provide this discussion in our limitations section. \n\n>I recommend the authors tone down their presentation somewhat. In 2.2, it should be claimed that only an approximation of the convex hull is computed (not the exact convex hull). Also referring to the controls problem as an \"established benchmark\" is somewhat of a stretch as this is a recent unpublished preprint with only a couple citations.\n\nThank you for this suggestion. We have toned down the claim to \"we aim to over-approximation the convex hull\". As for the benchmark, it has been covered in a body of other papers outside of the DRIP preprint (the benchmark is from \"nfl_veripy: Formal Verification of Neural Feedback Loops (NFLs)\", but we cannot leave a link here per NeurIPS rule).\n\n>I am not sure why the controls benchmark task is referred to as a \"robot moving on the floor of a room.\" This is a double integrator task, as described in the cited work that originally presented the problem. Of course this can be considered a planar system with strange dynamics, but it's not clear why that would be done when the dynamics have a classic double integrator structure.\n\nWe agree that the robot scenario does not properly highlight our story. We change this story to the DoubleIntegrator task we target later in the paper (since these dynamics are precisely the ones we verify in Section 4.1).\n\n>I'm confused on the discrepancy between the reported results for the baseline method. Specifically, the approximation ratio of ReBreach is about 4000, which is orders of magnitude higher than what I would expect based on the results in the original paper (errors less than 10x the true volume). What is causing this discrepancy?\n\nThe original paper only reports results for five timesteps back. We find this benchmark too simple, so we repeat this benchmark for ten timesteps back, where exponential error accrues due to looseness in the over-approximation.\n\n>In Figure 3, on the left side without input splitting, why is the convex hull so loose? I would expect it to tightly wrap around the green circles.\n\nOne possibility is that the convex over-approximation needs neuron branching or further input/output branching to get the tightest hyperplanes. Another possibility is that we did not run our \"without splitting\" algorithm for sufficient iterations, so it did not converge to the true convex hull.\n\n–\n\nWe hope that we’ve addressed the proposed concerns and would be more than happy to answer additional questions! \n"}]

Author rebuttal:
We thank the reviewers for their helpful and constructive comments about our paper. 

Thanks to the reviews, we have run a large suite of new experiments where we have evaluated our method on robustness verification for **inputs of dimension 8112** and neural networks of **167k neurons**, including complicated networks which feature convolutional layers, skip connections, and pooling. We also introduce new experiments for over-approximating the pre-image in a **6-dimensional quadrotor control** problem, where we improve upon state-of-the-art by **257 times tighter, 3.29 times faster**. We believe this addresses many concerns about the practical scalability of INVPROP, hyperplane selection, and branching. Furthermore, we provide a more nuanced discussion of these components of our approach in our new limitations section.

**New robustness verification experiments on large networks**

We performed an additional experiment using a benchmark from the VNN-COMP 2023. We extended alpha-beta-CROWN with support for output constraints using INVPROP. To reduce the runtime cost of incorporating output constraints, they were only applied to the penultimate layer of the network. Also, they are only used during the alpha-CROWN computation, i.e., during the optimization of relaxations of intermediate layers. If this step fails to prove UNSAT, alpha-beta-CROWN performs branching over the hidden neurons to remove nonlinearities. As alpha-beta-CROWN doesn’t update the intermediate relaxations in this second step, output constraints are not applied, however, the tighter intermediate layer bounds obtained from INVPROP in the first step (alpha-CROWN) also help improve the bounds after branching. We provide a comparison of the original alpha-beta-CROWN and our extended version in Figure 1. With output constraints, 5 of the 9 instances that **previously timed out (300s) were now solved on average within 16.2 seconds**. For instances that can be verified by vanilla alpha-beta-CROWN, INVPROP reduces the verification time on average 13.9 seconds.

**New quadrotor benchmark for higher dimension control**

We consider over-approximating the pre-image of the quadrotor discussed in Figure 15 of [1]. This quadrotor has a 6-dimensional state space, with 3 dimensions dedicated to position in the (x,y,z) coordinate space. We run prior work and our algorithm to find the tightest bounding box in this 3d space, reflecting a total of 6 constraints (one for each direction in each dimension). We run our algorithm with no branching. To benchmark against prior work, we run ReBreach-LP with no output partitioning and ReBreach-LP with 15625 output partitions using SkipLP, disciplined parametric programming, and the guided partitioning algorithm discussed in [1]. In Figure 2 and Table 1, we compare these three strategies, and we find that our over-approximation of the pre-image (in blue) is smaller than the state-of-the-art over-approximations by **257 times, 3.29 times faster**. Therefore, our algorithm scales well to higher dimensional control examples.

**New limitations section**

For higher-dimensional instances, our method would best work for box over-approximations (which require $2d$ hyperplanes in $d$ dimensions) and would struggle at more complicated shapes such as sphere pre-images. Though our hyperplane selection strategy works well in our application domains, we expect that more complex problems will benefit from a domain-specific strategy.

Iteratively refining all of the intermediate bounds utilizing INVPROP faces a quadratic dependence on network depth, as opposed to a linear dependence in traditional forward verification. Otherwise, our method scales similarly to verification of adversarial robustness [3] as can be seen in “Connection to forward verification”. To mitigate this, output constraints could only be applied to layers close to the output, as we used for the VNN-COMP23 YOLO benchmark.

Though our branching strategy works for verification in our case, it might not scale to higher dimensions. However, utilizing Branch and Bound for verification is independent of this work, and the trade-off between the tightness of verification and computational constraints is well-studied in prior literature ([2], [3], [4]). 

—

We hope that we have addressed any concerns and would be happy to answer any further questions to help inform an accurate assessment of our contribution!

[1] Backward Reachability Analysis of Neural Feedback Loops: Techniques for Linear and Nonlinear Systems, Nicholas Rober, Sydney M. Katz, Chelsea Sidrane, Esen Yel, Michael Everett, Mykel J. Kochenderfer, Jonathan P. How  
[2] Branch and Bound for Piecewise Linear Neural Network Verification, Rudy Bunel, Jingyue Lu, Ilker Turkaslan, Philip H.S. Torr, Pushmeet Kohli, M. Pawan Kumar  
[3] Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification, Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, J. Zico Kolter  
[4] IBP Regularization for Verified Adversarial Robustness via Branch-and-Bound, Alessandro De Palma, Rudy Bunel, Krishnamurthy Dvijotham, M. Pawan Kumar, Robert Stanforth  


Meta-review: The reviewers are happy to accept the paper. Please incorporate all the discussions and new experiments into the final version.
Decision: Accept (spotlight)