Zonotope Domains for Lagrangian Neural Network Verification
Authors: Matt Jordan
Jonathan Hayase
Alex Dimakis
Sewoong Oh
Venue: NeurIPS 2022 Accept (2022)
Keywords: neural network verification
lagrangian duality
robustness
zonotopes

Abstract: Neural network verification aims to provide provable bounds for the output of a neural network for a given input range. Notable prior works in this domain have either generated bounds using abstract domains, which preserve some dependency between intermediate neurons in the network; or framed verification as an optimization problem and solved a relaxation using Lagrangian methods. A key drawback of the latter technique is that each neuron is treated independently, thereby ignoring important neuron interactions. We provide an approach that merges these two threads and uses zonotopes within a Lagrangian decomposition. Crucially, we can decompose the problem of verifying a deep neural network into the verification of many 2-layer neural networks. While each of these problems is provably hard, we provide efficient relaxation methods that are amenable to efficient dual ascent procedures. Our technique yields bounds that improve upon both linear programming and Lagrangian-based verification techniques in both time and bound tightness.

Zonotope Domains for Lagrangian Neural Network Verification
Matt Jordan"
Jonathan Hayase* University of Washington jhayase@cs wareesswwshinnntnn edu
UT Austin
mjordan@cs. uteuus,eeccm
Alexandros G. Dimakis
Sewoong Oh University of Washington sewoongocs. washington, edu
UT Austin dimakisCaustin. utexas. edu
Abstract
Neural network verification aims to provide provable bounds for the output of a neural network for given input range. Notable prior works in this domain have either generated bounds using abstract domains, which preserve some dependency between intermediate neurons in the network; framed verification tion problem and solved a relaxation using Lagrangian methods. A key drawback of the latter technique is that each neuron treated independently. thereby ignoring important neuron interactions. We provide an approach that merges these two threads and uses zonotopes within a Lagrangian decomposition. Crucially, we can decompose the problem of verifying a deep neural network into the verification of many 2-layer neural networks. While each of these problems is provably hard, we provide efficient relaxation methods that are amenable to efficient dual ascent pro- cedures. Our technique yields bounds that improve upon both linear programming and Lagrangian- based verification techniques in both time and bound tightness.
optimiza-
Introduction
With the growing prevalence of machine learning in real-world applications, the brittleness of deep learning systems poses an even greater threat. It is well-known that deep neural networks are vulnerable adversarial examples, where minor change in the input network
major change in the output II There is a long history of defense techniques being proposed to improve the robustness of network, only researchers to focus instead on neural network verification, which, for a given network and range of input, aims verify whether a certain property is satistied for every input in that range. typical adversarial attack seeks to minimize the output of a scalar-valued network subject to certain input constraints. Verification provides lower bounds on the minimum output value achievable by such an adversary. Concretely, for scalur-valued network ff and input range X', verification provides lower bounds the problem min fx)).
completely broken shortly thereafter (2). This has inspired
As observed in 3 prior works in verification can be broadly categorized into primal and dual views. In the primal view, convex relaxations applied attain, for every intermediate layer of the network, convex superset of the true attainable range. For example, if = fL ...o fi, convex sets 2 are obtained such that {fx
fi( X) C z for [1...., L}.
"Equal contribution
'Github http://///ttttt..oo////eaaaaaaaa
36th Conference on Neural Information Processing Systems (NcurIPS 2022).

---

Under the dual lens, verification is treated as stagewise optimization problem and Lagrangian relaxation applied to yield a dual function that always provides valid lower bounds. Often, this dual function is decomposable into a sum of minimization problems which are efficiently computable. One hallmark of all existing dual verification techniques is that intermediate bounds 2 are required. In this case, either an efficient primal verification algorithm must first be applied or, for example, the dual verifier can be run iteratively on each neuron to provide upper and lower bounds for each intermediate layer.
Our approach is an attempt to combine the primal and dual threads of verification. We first apply a primal verification algorithm that generates bounds on the attainable range of each intermediate layer. To do this we leverage zonotopes, a more expressive class of polytopes than axis-aligned hyperboxes. Notably, we offer an improvement to existing zonotope bounds when we are also provided with incomparable hyperbox bounds. These zonotopic intermediate bounds are then applied to a dual verification framework, for which dual ascent can be performed. Our formulation may be viewed as taking the original nonconvex verification problem and decomposing it into many subproblems, where each subproblem is verification problem for 2-layer neural network. However, as even verifying a 2-layer network is hard in general, we further develop efficient relaxation techniques that allow for tractable dual ascent.
We introduce a novel algorithm, which we call ZonoDual, which i) highly scalable and amenable to GPU acceleration, ii) provides tighter bounds than both the prior primal and dual techniques upon which our approach is built, üi) is highly tunable and able effectively balance the competing objectives of bound tightness and computation speed, and iv) is applicable as an add-on to existing dual verification frameworks to further boost their performance. We apply ZualDual to variety of networks trained on MNIST and CIFAR-10 10 and demonstrate that ZonoDual outperforms the linear programming relaxation in both tightness and runtime, and yields a tighter bounding algorithm than the prior dual approaches.
We first discuss prior works in the verification domain. Then, we examine the existing dual framework that serves as the backbone for our algorithm, paying particular attention to the areas in which this may be tightened. Then, we discuss how we attain zonotope- based intermediate bounds and introduce the fundamental sub-problem required by our dual ascent algorithm. Ultimately, we combine these components into our final algorithm and demonstrate the scalability and tightness of our approach on networks trained on the MNIST and CIFAR-10 10 datasets.
2 Related Work
Neural network verification is well-studied problem and has been approached from several angles. Exactly solving the verification problem is known as complete verification, and is known to be NP-hard even for 2-layer ReLU networks 4 Complete verification approaches include mixed- integer programs, satisfiability modulo theories (SMT), geometric procedures, and branch- ann-bundd techniques 5 67 [0] In particular, branch-and- bound procedures generate custom branching rules to decompose verification into many smaller subproblems, which can be relaxed or further branched, allowing the algorithm to focus its efforts on the areas for greatest improvement [2] We stress that this current work focuses only on the 'bound' phase, and our approach may be applied to branched subproblems.
Often it is not necessary to exactly solve the verification problem, and only providing a lower bound to the minimization problem can suffice. This is known as incomplete verification. We closely examine the primal and dual verification threads, but first mention few lines of work that do not fit neatly into this paradigm: notable approaches here include semidefinite programming relaxations [1 or verification via provable upper bounds of the Lipschitz constant [15 16 [8]
Primal verification: A general theme in primal verification techniques is to generate convex sets that bound the attainable range of each intermediate layer. The simplest such approach is interval bound propagation (IBP) which computes a bounding hyperbox for each layer [19]. A more complex approach is to bound each intermediate layer with polytope. Several different polyhedral relaxations are available, with DeepPoly being on the lesser-complcxity side, PLANET being the canonical triangle relaxation, and the formulation by Anderson et. al being tightest albeit with exponential complexity (20 21 7 Zonotopes provide a happy medium, being both highly expressive and
computationally easy to work with 22 in section 4.
23
We will discuss zonotope relaxations more thoroughly
2

---

Dual verification: Orthogonal to the primal approaches exist several works which consider verifica- tion by relaxations in dual space 24 25
L2 26 27.. Here, verification is viewed an optimization problem with constraints enforced by layers of the network. The general scheme here is to introduce dual variables penalizing constraint violation, and then leverage weak duality provide valid lower bounds. The standard Lagrangian relaxation was first proposed in [24), and then several improve- ments have been made to provide provably tighter bounds, faster convergence, or generalizations of the augmented lagrangian. These techniques are highly scalable and notably, one recent work has been able to provide bounds tighter than even the standard LP relaxation [9]. Our approach will follow similar scheme, but differs fundamentally from prior works in that operate tighter primal domain and can therefore provide tighter bounds.
Lagrangian Decomposition
Problem Definition: In a canonical neural network verification problem, we are given a scalar- valued feedforward neural network, f()), composed of L. alternating compositions of affine layers and elementwise ReLU layers. We name the intermediate representations 20 =L, and are supplied with a subset, X, of the domain of f()), which we assume to be an axis-aligned hyperbox. Verification is then written as optimization problem
minimize #g =
2L
(Ia)
subject to
20
Wozo
(Ib)
2k+1 (z)1 (0 L
(1c)
where a denotes the ReLU operator applicd clementwise, and each We is the weight of an affine or convolutional layer. Our formulation is also amenable to bias terms everywhere, though omit these throughout for simplicity.
While there are several verification approaches leveraging Lagrangian duality, we consider the Lagrangian decomposition formulation introduced in (25). Here, each primal variable zn of the verification problem is replaced by pair of primal variables z - along with accompanying
Dual verification:
equality constraints, yielding an equivalent optimization problem:
minimize #o ZoE - 1
(2a)
subject to
20
A WorO
(2b)
1+ W (05k5
A
(2c)
26 =
(0sks
(2d)
By introducing unconstrained dual variables Ps: for each constraint in Equation 22d and maximizing over Pk. we attain an optimization problem that equivalent to the original. To tractably solve this, two relaxations are performed. First, weak duality is applied by swapping the max and min, which introduces the dual function ((),, for which every value of p provides a lower bound:
I--1
g(p) =
minimize ag X.EX ..... -.
Z
A +
Pk (
==x²
(3a)
k=
subject to
20
Wozo
(3b)
2++1
Wz+10(2)))
(0
(3c)
The goal now is to solve max, (p). The dual function can be decomposed into L subproblems by substituting equality constraints and rearranging the objective function:
L-2
x(p) = min Po Wozo 20E2
Σ
min PI WE+10 Pb. 26
oT. T.B B
(4a)
k=1
min W W2o(= =
- -Ta - Pi-1=
(4b)
In current state, is unlikely that g(p) for nonzero P will lead to any finite lower bound as each B
2g is unconstrained. In other words, only subproblem, (4a). has any information about the input
3

---

constraint (zo E )²). To remedy this, one can tighten the dual optimization by imposing intermediate bounds on 2 "s so long as those bounds include all feasible values. Specifically, for each 2 we can impose bounding set 2g, as long as the following implication holds:
To E X
B 2k E 2k
(5)
All prior dual approaches have chosen the sets 2u to be axis-aligned hyperboxes for two reasons. First, is extremely efficient to attain hyperbox bounds every layer. Second, when 2 hyperbox, the dual function can be evaluated efficiently by further decomposing each component of the dual along its coordinates. Equipped with intermediate bounds kg. and noting that g(p) is concave function of p. the standard procedure is to perform dual ascent on g(p). This requires gradients (p), which can easily be computed as the primal residuals. Letting 2g and BB be the argmin of the dual function, then V ppg(() = 2 2k
The key innovation in this work is to replace the intermediate bounds 3₁ with zonotopes everywhere. In this case, intermediate bounds may easily be computed as we will see in the next section. Zonotopes have a distinct advantage over hyperboxes in that every coordinate is no longer independent, and therefore neuron dependencies function and leads to larger dual values. However, this comes with the cost that the dual function is more computationally difficult to evaluate.
encoded. This further constrains the feasible set of the dual
4 Zonotopes
We start with a review of zonotopes and how they may be used to attain intermediate bounds. Then introduce the problem of ReLU programming. tie it to the dual decomposition formulation, and discuss our relaxations for efficient dual evaluation. Proofs of all claims are contained in the appendix.
Zonotope Properties: Zonotopes are class of polytopes, which we formally define using the notation (cc E) to refer to the set
Z(c = {c+ Ey y [-1,1]"
where c E Rd is called the center, and E E ddxm is called the generator matrix. Each column of the generator matrix is line segment in Rd, and ((c, E') can be equivalently be viewed as the Minkowski sum of each generator column offset by c; or as the affine map y - c Ey applied to the foe ball in R In particular, note that a hyperbox is zonotope with diagonal generator matrix. Zonotopes have several convenient properties:
Efficient Linear Programs: Linear programs can be solved in closed form over a zonotope:
min a a= == aT= c la E zE)(c
Closure under affine operators and Minkowski sums: given an affine map - Wr {W + bl 2 Z(c, E)} is equivalent to the zonotope Z(W c b, W E). The Minkowski sum of two sets A, B is defined A @ B == {i + of columns, the Minkowski sum of two zonotopes (c1, E1), (c2,, E2) is also zonotope:
the set
A, y E B). Letting Ej E| denotes concatenation
Z(c,, E1) @ ((e2, E2) ((cl + c2, E, E2).
Intermediate Bounds with Zonotopes: Prior work has developed efficient techniques to generate intermediate layer bounds using zonotopes for feedforward neural networks. The details are deferred to the appendix, and we can assume that we have access to a black box that, given a zonotope 2, is able to generate zonotope ) such that (a(=) 2 E 2 C y. Such an operation is called sound pushforward operator. One such pushforward operator known as DeepZ and can be applied repeatedly to provide valid zonotopic bounds for every intermediate layer of the neural network [22 We make two observations regarding these intermediate bounds here:
Proposition 4.1. Let Z be the kth zonotope bound provided by the Deepī procedure, and let Ha be the ttth intermediate bound provided by the Kolter-Wong dual procedure (20). Then the smallest hyperbox containing Z₁ is exactly Hk-
Proposition 4.2. Suppose Z is zonotope and H is hyperbox, such that Z g H. Then we can develop a sound pushforward operator for the ReLU operator that outputs a zonotope 2' containing the ReLU of every element of Z nHH, with the property that Z' (e)

---

The first proposition states that common technique for generating intermediate hyperbox bounds is never any tighter than the procedure we use to generate intermediate zonotope bounds. The second proposition describes an improved pushforward operator that offers improvements against DeepZ but requires extra information provided by a hyperbox.
ReLU Programming: We return our attention to the dual function introduced in equations Equa- tions (4a) and (4b). Note that the first term of Equation 4 linear program of a zonotope which can be solved extremely efficiently, while all other terms adopt a form we refer to as a ReLU program
Definition 4.1. Given a set 2 S R2, and two objective vectors c1, C2 E R.d, we say the ReLU Program is the optimization problem
min Z22
G cf 2 02 (2).
(6)
ReLU programming nonconvex for general C2. When 2 is an interval, only the endpoints, or 0 it is contained in the interval, are candidate optima. In this case, the ReLU program may be solved by evaluating the objective at each candidate. When 2 is hyperbox in Rd, each coordinate can be considered independently, amounting to solving d ReLU programs over intervals. The story quickly becomes more complicated
is a zonotope:
Theorem 4.1. When Z a zonotope, solving a ReLU program over Z is equivalent to a neural network verification problem for a 2-layer network, which is known to be NP-hard.
Remarks: This theorem implies that solving ReL.U programs over more complex sets, such as polytopes in general, is also NP-hard. However it remains an open question whether solving ReLU programs over other simpler sets such as parallepipeds, i.c. zonotopes with an invertible generator matrix, is hard. Note that ReLU programs can be solved exactly via Mixed-Intese Program (MIP) using the standard form for encoding a ReLU [5].
We pause here to observe the current situation. Lagrangian methods for verification first make a relaxation by applying weak duality. When using zonotopes for the intermediate bounds, one is able to decompose the very large non-convex optimization problem of deep network verification into many smaller subproblems which are equivalent to two-layer network verification problems. Unfortunately, each of these subproblems is also NP-hard, and thus must be further relaxed to attain tractability.
The primary relaxation technique we consider comes from the following observation. Consider a d-dimensional zonotope Z and ReLU programming objectives (C1, c2). Then, for any partition S U...UU Sn of {I....,d} d}, the inequality
Zonotope Partitioning:
d + 02,10(2))) 2
min Σ 10a ZE2
Σ min (c + j=1
=E
iES;
holds. This approach has nice geometric interpretation well. The decomposed minimization minlez Lies, (c1,22; + c2 (z:)) can be viewed as optimization over Z when it has been projected onto the linear subspace spanned by the elements of Sj. Projection onto a linear subspace is an affine operator, so each projection of 2 is itself a zonotope. Indeed, the projection onto the linear subspace spanned by Sj is simply the center and generator rows indexed by Sy-
Observe that if each Sj were singleton set, then decomposing the ReLU program according to these Sy's is equivalent to relaxing the ReLU program by casting& 2 to the smallest containing hyperbox. If the partition were the trivial partition (1,..., d). then 2 remains unchanged. Finally, notice that the Minkowski sum of every projection of 2 is itself a zonotope.
In this sense, by choosing any partitioning of coordinates, are able to relax Z into zonotope that is simultaneously a superset of and a subset of the hyperbox-relaxation of Z. This is optimistic for our dual ascent procedure, as any partitioning restricts the primal feasible space for the dual function evaluation. It is in this way that we are able to interpolate the coarseness of our relaxation, which is directly controlled by the coarseness of our partitioning. Because we expect the complexity of solving a ReLU program over a zonotope to be superlinear in the dimension, shattering a zonotope in this fashion can drastically improve the complexity of solving relaxation of a ReLU program.
Two-dimensional Zonotopes: A special case we consider is when we partition zonotope into 2- 2-dimensional groups. This is because a 2-dimensional zonotope can be significantly more descriptive
5

---

than 2-dimensional rectangle, but the solution of a ReLU program can still be computed efficiently. Observe that the argmin of a ReLU program over a 2-dimensional zonotope must occur at either i) a vertex of the zonotope, ii) a point where the zonotope crosses coordinate-axis, iii) the origin. This follows from the fact that a ReLU program over 2-dimensions may be viewed as 4 independent linear programs over the intersection of the zonotope and each orthant. For the purposes of ReLU programs, suffices to enumerate all vertices of the zonotope and compute any axis crossings or origin-containments It turns out that this may be done in nearly linear time:
Theorem 4.2. If ((e, E) is a 2-dimensional zonotope with m generators, Z has 2m vertices and the set of all vertices, axis crossings, and the containment of the origin can all be computed in Om log m) time.
5 The ZonoDual Algorithm
With both preliminaries of dual verification techniques and zonotopic primal verification techniques in hand, we can now fully describe the algorithm we employ in practice. We first describe the algorithm as it used to bound a single neuron's value, i.e. the output neuron. After we describe how we adapt our approach to the stagewise setting where our algorithm is applied to each intermediate neuron to yield tighter box bounds. Our algorithm can be described three main phases: an inilialization phase, where primal bounds are generated to define the feasible set for each subproblem in the dual function; an ileration phase, where the argmin of the dual function computed many times to provide informative gradients for updates to the dual variables; and an evaluation phase, where the primal bounds are tightened to yield a more computationally intensive dual function, which only needs to be evaluated a single time.
Naively, we can apply the DeepZ procedure here to attain a zonotope bounding the output range of the network at every layer. Both this procedure and our box-improved variant can be done extremely efficiently. We adapt two techniques from [25] in the initialization phase. First we notice that some very minor improvements to DeepZ can be made using an application of Proposition 4.2 when provided with the boxes from interval bound propagation. Second, we initialize the dual variables to the KW dual variables from (20), which by 4.1 are equivalent to the scale factors applied internally in the zonotope pushforward operators.
Initialization phase:
In the iteration phase, each intermediate zonotope 2₁ is partitioned into compo- nents that are amenable repeated evaluations of the dual function. We always initially partition each zonotope into 2-d chunks for which the dual function may be evaluated on a GPU without requiring any MIP calls. Recall that for a d-dimensional zonotope with m generators, after the initial (dm log m.) candidate optima computation, each ReLU program can be evaluated in O (dm) time. These initial 2-d partitions are computed using one of several simple heuristics, described in the appendix, with the aim to generate 2-d zonotopes which are as 'un-box-like" as possible. Optionally, after an initial 2-d iteration phase, these partitions may be combined and dual ascent can be applied, where each subproblem now requires several calls to a MIP solver. At any point during this phase, the dual function evaluations still provide valid lower bounds to the verification problem.
Iteration Phase:
Evaluation Phase: In this phase, we can presume that effective dual variables have been found during the previous phase. The objective here to tighten the feasible range of each subproblem, which will necessarily improve the value of the dual function. Because we only need to evaluate a bound on the dual function once here, we find that it often worth it to spend more time solving each subproblem. We do this by simply merging several partition elements together, converting our 2-dimensional zonotopes into higher-dimensional ones that require calls to a MIP solver to compute. Despite the theoretical intractibility of MIPs, we find that this procedure is remarkably efficient. In practice, it is often sufficient to only merge zonotopes at the later layers in a network where the dual function subproblems are the most negative. Finally, we note that as only bound upon the dual function is required here, and each subproblem is itself a 2-layer verification problem, the MIPs may be terminated early. Any other incomplete verification approach can be applied here as well.
Ultimately, our algorithm will always provide a valid lower bound to the verification problem so long as the dual function is evaluated appropriately. The provable correctness of our algorithm stems from i) the fact that weak duality always holds and any evaluation of the dual function with feasible dual variables provides a valid lower bound tot the primal problem; and ii) by leveraging zonotopes and a sound relaxation of them, we only ever provide lower bounds to the evaluation of the dual function. Further, can also guarantee that, for any fixed set of dual variables p, the bounds
Guarantees:

---

we provide will be tighter than those provided by the approach in [25]. This follows because we have reduced the feasible set within each dual subproblem, relative to the hyperbox approaches in prior works. Similarly, because = 0 is always valid choice, when the dual variables are optimized appropriately, we will provide tighter bounds than whichever primal verification method is applied at the initialization phase.
Stagewise computation:
When the network of interest is of sufficiently small size, any verification algorithm may be applied stagewise, where the algorithm computes upper and lower bounds to each neuron, starting from those the first layer. This is often effective for generating tighter intermediate box bounds, which in turn yields much tighter output bounds. However this comes the cost of running many calls to the verification algorithm. This can be parallellized for verification procedures amenable to GPU acceleration, but demands a large memory footprint.
At first glance, it may seem that such a stagewise procedure obviates the improvements attain by leveraging zonotopes: indeed, each stagewise bound is a box bound. However, we show that we can apply this stagewise trick our approach to generate tighter box bounds, which can then be employed by Proposition 4.2 to yield tighter zonotopic bounds. Additionally, in the case that these the improved zonotope bounds, these can be employed in imposing further constraints upon each subproblem. Instead of solving each ReLU program over zonotope, we can instead solve each ReLU program over the intersection of zonotope and hyperbox. In the case, it is trivial to apply elementwise constraints to each variable in the MIP- in fact, this often improves the running time of each MIP. In the 2-d case, we observe that we are able to solve ReLU programs over the intersection of a 2-d zonotope and rectangle as efficiently as solving over a 2-d zonotope alone. This the content of the following corollary to Theorem 4.2
box bounds are incomparable
Corollary 5.1. Given a 2-d zonotope with m generators, the set of candidate optimal points to ReLU program has cardinality no greater than (2m + 9) and is computable in time O(m log m).
To clarify the bound improvements and their corresponding runtime cost imposed by each step of our approach, we perform an ablation study on an MNIST fully connected network (MNIST FFNet). We report the bounds relative to the bound attained by the I.P relaxation in Table ??. We consider three initialization settings separately: the standard Deepž zonotopes, the DeepZ zonotopes augmented with IBP bounds, and zonotopes informed by the the box bounds from BDD+ 25 Then we perform dual ascent over 2-d zonotopes, before merging the zonotopes of the final layer only and evaluating the MIP. We report these numbers in Table ?? Here we see that a tight initialization does indeed help, but this gap shrinks after our dual ascent procedure. We also see substantial gain in bound improvement by using MIPs, even in the last layer's 's zonotopes alone.
Ablation study:
Experiments
We evaluate the effectiveness of our approach several networks trained on the MNIST and CIFAR- 10 datasets. While many recent verification techniques employ branch-and-bound strategy, we only provide innovations on the bounding component of this pipeline. Strong verifiers should employ both effective bounding algorithms and clever branching strategies, which are both necessary but fairly independent components. Like other dual-based verification techniques, our approach can be applied using any of a number of branching strategies. We focus our efforts primarily on the improvements of each considered method. We argue this is reasonable
in the bound provided by single choice of metric because most prior benchmarks focus on c-values far lower than typically used in adversarial attack scenarios. This artifically decreases the depth to which branching strategies must search, skewing the results. By focusing on the bound of the verification, we directly measure the metric that bounding algorithms such as ours seek to optimize. However, for the sake of completeness, we do also evaluate verified robustness percentage upon several benchmark MNIST networks. For bound evaluations, we separate our experiments into two cases: we first examine the setting where only the output neuron is optimized, which we denote the 'single-stage' setting; and the case where every neuron is optimized to provide tighter intermediate box bounds, denoted the 'stagewise' setting. We compare the bound and running time against the following approaches: BDD+ the Lagrangian Decomposition procedure proposed in 251, where the optimization is performed using optimal proximal step sizes; LP, the original linear programming relaxation using the PLANET relaxation on each ReLU neuron 20]; Anderson, the linear programming relaxation, where 1-cut is applied per neuron as in 77 AS, a recent Lagrangian technique which iteratively chooses cuts to employ from the Anderson relaxation 9
7

---

1.0
1.0
Algenthm
Algerahit
0.8
BDD
Poportion
Prpprtiom
Anderum
Anslenoon
ZiD-113
ZD-20
0.4
0.4
0.2
10
Bound
Figure 1: Cumulative density function plots of the bounds obtained by each algorithm for deep convolutional network trained on MNIST (left) and a deep convolutional network trained on CIFARIO (right). Lines further to the right indicate tighter bounds. Our algorithms are bolded in the legend.
Table 1: Timing data for the single-stage bounds.
All baselines are run implemented using the code and hyperparameter choices from prior works, and network weights are taken from ex- isting works where applicable. Architecture de-
Alg/Net
MNIST Deep
CIFAR SGD
BDD+ LP
2.5 0.2
1.5 + 0.1
0.5
6.2 0.6
scriptions are contained in the supplementary. We follow [25] construct scalar-valued ver- ification problems: for examples with label we compare the difference between the 7th and (i +i+ 1)th logit of network. We can extend this procedure multi-class task by applying the verification π - times for each incorrect logit.
ZD-2D
1.5
7.6
AS
1.2
10.2 0.8
ZD-MIP
23.1 12.4
11.0
Anderson
52.4 27.5
21.3 + 4.6
Single-stage bound evaluation: In the single-stage setting make the following hyperparameter choices for our approach. We initialize the intermediate bounds using zonotopes informed by the boxes attained by the best of the DeepZ bounds and the IBP bounds. We then decompose each zonotope into 2-dimensional partitions, using the "similarity" heuristic for fully-connected networks, and the 'spatial' heuristic for convolutional networks. Then perform 1000 iterations of the Adam optimizer during the dual ascent procedure. We report the value at the last iteration as ZD-2D. Then we merge the partitions of only the last layer of each network into 20-dimensional zonotopes, and evaluate the dual function under this new partitioning. We report these values as ZD-MIP.
We present results of approach on the MNIST-Deep network, which has 5196 neurons and 6 layers, evaluating over a domain of &o boxes with < = 0.1. Specifically we present cumulative density function plots: a point (x.
any curve in these plots indicates that that particular algorithm attains a bound tighter than x for (1 7)% of the examples. Curves further to the right indicate tighter bounds in aggregate. Figure (left) contains the distribution of reported bounds correctly-classine
every
example in the MNIST validation set. In Figure [ (right), we present a similar CDF plot for CIFAR-10 network with 6244 ReLU neurons and layers. For this CIFAR network, we set 5/ 35255, as in [9]. The average and standard deviation runtimes for these networks is provided in Table
1.0
1.0
Algonillm
Algurihm
0.8
Propartion
Propurtion
AS256
AS512
BDD+
2D
RD0+
7D
0.4
0.4
ASS13 ZD
0.2
0.2
10
30
-10
Bound
Bound
Figure 2: Stagewise bounds on the MNIST-FFNet (left) and MNIST-Deep (right) networks.
Stagewise bound evaluation: Now we turn our attention to the setting where enough computation time is allowed to perform the optimization procedure every neuron in turn, which is able to

---

Table Verified Robustness on MNIST Networks, Methods denoted with an asterisk had numbers
taken from (28).
Model
ZDD
BDD+
CROWN
PRIMA *
8-CROWN#
MLP 5x100
0.026
28.5% (24s)
19.8% (7s)
16.0% (Is)
51.0% (159s)
69.9% (102s)
MLP 8x100
0.026
21.8% (19s)
19.1% (15s)
18.2% (Is)
42.8% (301s)
62.0% (103s)
MLP 5x200
0.015
41.8% (28s)
33.2% (8s)
29.2% (2s)
69.0% (224s)
77.4% (86s)
MLP 8x200
0.015
29.7% (26s)
27.4% (17s)
25.9% (6s)
62.4% (395s)
73.5% (95s)
ConySmall 0.12
52.6% (38s)
16.6% (6s)
15.8% (3s)
59.8% (42s)
72.7% (7s)
generate tighter box bounds. Here we notice an interesting observation: our method can be improved by leveraging tighter intermediate box bounds, but is agnostic as to where these bounds come from. Indeed, our approach can take as input any collection of tighter box bounds and generate tighter zonotopes via Proposition 4.2] However, our current implementation of this tighter primal bound is not vectorized to be amenable, in the way that others are, to stagewise bounding procedures. This is purely an implementation detail, and instead use existing primal bounding techniques.
As baselines here, we compare against the IP approach, BDD+, and the active set approach with 256 and 512 iterations, denoted AS256, AS512. We leverage box bounds provided by each of these dual approaches to inform our zonotope bounds from which we can run our method, denoted by a - ZD. Note that BDD+ can never surpass bounds provided by the LP approach, whereas ours and the active set procedure can both improved even further with a longer runtime. Hence it not sufficient to provide better bound, but also do so more efficiently. In this case, our approach performs 2000 iterations of Adam on 2-D zonotopes and increases the partition size of the final two layers of each network to sizes of 16 and 20 respectively.
We present our results on the MNIST-FFNet and MNIST-Deep network which have 960 and 5196 neurons, and and layers respec- tively, again using an 0.1. CDF plots of bounds for these two networks are provided in with timing data in 2 We observe that the BDD+ bound completes very quickly, but attains bound only slightly worse than LP. Our approach, when initialized with the BDD+ bounds runs more efficiently than AS256, pro- viding bounds that are comparable or better than the slower AS512 approach.
Table 2: Timing data for stagewise bounds
AlglNet
MNIST Deep
MNIST Wide
BDD+
15.4 0.4
8.3 0.3
BDD+
ZD
51.7 0.9
36.4 6.8
AS256
4.6
AS256 + ZD
73.3
AS512
289.3
91.3
AS512 + ZD
119.2 6.9
LP
2132.2 + 494.4
387.1 + 65.5
% Verified Robustness: Finally we evaluate our approach comparing against all incorrect logits on MNIST trained networks, mirroring the setup of (28). We report numbers from unbranched version of ZD and BDD+ alongside several other verification techniques 22 30 3T Compared
to other efficient, branch- branch-friendly procedures such BDD+ and CROWN, approach provides tighter bounds at fair cost to efficiency. Our approach provides weaker bounds than PRIMA, but is significantly faster. 3-CROWN, in particular, leverages dual-based branching strategy which could be applied to our method. However due to its extremely efficient bounding procedure and the need to solve millions of subproblems for verification, it is unclear if our approach surpass this method.
7 Conclusion
In this work, we demonstrated how primal and dual verification techniques can be combined to yield efficient bounds that are tighter than either of them alone. Primal methods capture complex neuron dependencies, but do not optimize for a verification instance; while dual methods are highly scalable, but rely unnecessarily loose primal bounds. This work is a first step in combining these two approaches. We believe that this combination of approaches is a necessary direction for providing scalable and tight robustness guarantees for safety-critical applications of machine learning.
Acknowledgements: This work is supported in part by NSF grants CNS-2002664, DDMS-2334011 CCF-2019844 as part of NSF Institute for Foundations of Machine Learning (IFML), CNS-21 12471 as a part of NSF AI Institute for Future Edge Networks and Distributed Intelligence (AI-EDGE), CCF-1763702, 190129., CNS-2148IA
Tripods CCF-1934932, and research gifts by Western

---

Digital, WNCG IAP, UT Austin Machine Learning Lab (MLL), Cisco and the Archie Straiton Endowed Faculty Fellowship.
10

---

References
[1] Christian Szegedy, Wojeiech Zaremba, Iya Sutskever, Joan Bruna, Dumitru Erhan, lan Good- fellow, and Rob Fergus. Intriguing properties of neural networks. December 2013.
[2] Anish Athalye, Nicholas Carlini, and David Wagner. Obfuscated gradients give false sense of security: Circumventing defenses to adversarial examples. In Jennifer Dy and Andreas Krause, editors, Proceedings of the 35th International Conference Machine Learning, volume 80 of Proceedings of Machine Learning Research, pages 274-283. PMLR, 2018
[3] Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang. A convex relaxation barrier to tight robustness verification of neural networks. February 2019.
[4] Guy Katz, Clark Barrett, David Dill, Kyle Julian, and Mykel Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. February 2017.
[5] Vincent Tjeng, Kai Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. November 2017.
[6] Matteo Fischetti and Jason Jo. Deep neural networks and mixed integer linear optimization. Constraints, 23(3):29--309, July 2018.
[7] Ross Anderson, Joey Huchette, Will Ma, Christian Tjandraatmadja, and Juan Pablo Vielma. Strong mixed-integer programming formulations for trained neural networks. Mathematical Programming, pages 1-37, 2020.
[8] Matt Jordan, Justin Lewis, and Alexandros G Dimakis. Provable certificates for adversarial examples: Fitting ball in the union of polytopes. Advances in Neural Information Processing Systems 32, pages 1 14059-14069. 2019.
[9] Alessandro De Palma, Rudy Bunel, Alban Desmaison, Krishnamurthy Dvijotham, Pushmeet Kohli, Philip H S Torr, and M Pawan Kumar. Improved branch and bound for neural network verification via lagrangian decomposition. April 2021.
[10] 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. November 2020.
[11] Jingyue Lu and M Pawan Kumar. Neural network branching for neural network verification. arXiv preprint arXiv:1912.013222 2019.
[12] Alessandro De Palma, Harkirat Singh Behl, Rudy Bunel, Philip H S Torr, and M Pawan Ku- mar. Scaling the convex barrier with active sets. https://openrevier: http:pppwrreiiiiieeeea/aaaaieaaa uQfDy7Lr1TR Accessed: 2021-9-18.
[13] Aditi Raghunathan, Jacob Steinhardt, and Percy Liang. Semidefinite relaxations for certifying robustness to adversarial examples. November 2018.
[14] Sumanth Dathathri, Krishnamurthy Dvijotham, Alexey Kurakin, Aditi Raghunathan, Jonathan Uesato, Rudy Bunel, Shreya Shankar, Jacob Steinhardt, Ian Goodfellow, Percy Liang, al. Enabling certification of verification-agnosti networks via memory-efficiet semidefinite programming. arXiv preprint arXiv:2010. /645, 2020.
[15] Mahyar Fazlyab, Alexander Robey, Hamed Hassani, Manfred Morari, and George Pappas. Efficient and accurate estimation of lipschitz constants for deep neural networks. In Advances in Neural Information Processing Systems 32, pages 11423-11434, 2019.
[16] Aladin Virmaux and Kevin Scaman. Lipschitz regularity of deep neural networks: analysis and efficient estimation. In Advances in Neural Information Processing Systems 31, pages 3835-3844 2018
[17] Navid Hashemi, Justin Ruths, and Mahyar Fazlyab. Certifying incremental quadratic constraints for neural networks via convex optimization. December 2020.

---

[18] Matt Jordan and Alexandros G Dimakis. Exactly computing the local lipschitz constant of ReLU networks. March 2020.
[19] Rüdiger Ehlers. Formal verification of Piece- Wise linear Feed-Forwart neural networks. In Automated Technology for Verification and Analysis, pages 269-286. Springer International Publishing, 2017.
[20] J Zico Kolter and Eric Wong. Provable defenses against adversarial examples via the convex outer adversarial polytope. November 2017.
[21] Singh, Gagandeep, Gehr, Timon, Püschel, Markus, and Vechev, Martin. An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages, January 2019.
[22] Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel,, and Martin T Vechev. Fast and effective robustness certification. NeurlPS, 1(4):6, 2018.
[23] Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. Boosting robustness certification of neural networks. In International conference on learning representations, 2018.
[24] Krishnamurthy, Dvijotham, Robert Stanforth, Sven Gowal, Timothy Mann, and Pushmeet Kohli. dual approach to scalable verification of deep networks. March 2018.
[25] Rudy Bunel, Alessandro De Palma, Alban Desmaison, Krishnamurthy Dvijotham, Pushmeet Kohli, Philip Torr, and M Pawan Kumar. Lagrangian decomposition for neural network verification. In Jonas Peters and David Sontag, editors, Proceedings of the 36th Conference on Uncertainty in Artificial Intelligence (UAI), volume 124 of Proceedings of Machine Learning Research, pages 370-379. PMLR, 2020.
[26] Leonard Berrada, Sumanth Dathathri, Krishnamurthy, Dvijotham, Robert Stanforth, Rudy Bunel, Jonathan Uesato, Sven Gowal, and M Pawan Kumar. Verifying probabilistic specifications with functional lagrangians. February 2021.
[27] Shaoru Chen, Eric Wong, J Zico Kolter, and Mahyar Fazlyab. Deepsplit: Scalable verification of deep neural networks via operator splitting. arXiv preprint arXiv:2106.09117, 2021.
[28] 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. arXiv preprint vrXiv:2103.0665 2021.
[29] Huan Zhang, Tsui-Wei Weng, Pin- Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neu- ral network robustness certification with general activation functions. Advances in neural information processing systems, 31, 2018.
[30] Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev. Precise multi-neuron abstractions for neural network certification. arXiv e-prints, pages aixiv 2103, 2021.
[31] Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks. September 2018.
[32] Matthew Mirman, Timon Gehr, and Martin Vechev. Differentiable abstract interpretation for provably robust neural networks. Jennifer Dy and Andreas Krause, editors, Proceedings of the 35th International Conference on Machine Learning, volume 80 of Proceedings of Machine Learning Research, pages 3578-3586, Stockholmsmässsan, Stockholm Sweden, 2018. PMLR.
[33] Matt Jordan and Alex Dimakis. Provable lipschitz certification for generative models. In Pro- ceedings of the 38th International Conference on Machine Learning, volume 139 of Proceedings of Machine Learning Research, pages 5118551111 18-5126. PMLR, 2021.
[34] Diederik P Kingma and Jimmy Ba. Adam: A method for stochastic optimization. arXiv preprint arXiv.1412.6980, 2014.
12

---

[35] Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards deep learning models resistant to adversarial attacks. arXiv preprint arXiv:1706.066 2017.
[36] Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual, 2021. URL https:/// //ww gurobi com
Checklist
The checklist follows the references. Please read the checklist guidelines carefully for information on how to answer these questions. For each question, change the default [TODO] [Yes], [No] or [N/A]. You are strongly encouraged to include justification to your answer, either by referencing the appropriate section of your paper or providing brief inline description. For example:
Did you include the license to the code and datasets? [Yes] See Section ??.
Did you include the license to the code and datasets? [No] The code and the data are proprietary.
Did you include the license the code and datasets? [N/A]
Please do not modify the questions and only use the provided macros for your answers. Note that the Checklist section does not count towards the page limit. In your paper, please delete this instructions block and only keep the Checklist section heading above along with the questions/anssees below.
1. For all authors...
(a) Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope? [Yes]
(b) Did you describe the limitations of your work? [Yes] See Appendix
(c) Did you discuss any potential negative societal impacts of your work? [Yes] See
Appendix
(d) Have you read the ethics review guidelines and ensured that your paper conforms to them? [Yes]
2. If you are including theoretical results...
(a) Did you state the full set of assumptions of all theoretical results? [Yes]
(b) Did you include complete proofs of all theoretical results? [Yes] See Appendices
3. If you experiments..
(a) Did you include the code, data, and instructions needed to reproduce the main exper- imental results (either in the supplemental material or as a URL)? [Yes] Zipped in appendix
(b) Did you specify all the training details (e.g., data splits, hyperparameters, how they were chosen)? [Yes] Described in Appendix
(c) Did you report error bars (e.g.. with respect to the random seed after running experi- ments multiple times)? [No] Standard deviations for times, but n/a for CDF plots
(d) Did you include the total amount of compute and the type of resources used (e.g., type of GPUs, internal cluster, cloud provider)? [Yes] Compute environment delineated in appendix
4. If you are using existing assets (e.g., code, data, models) or curating/releasing new assets...
(a) If your work uses existing assets, did you cite the creators? [Yes] Models and choices of given proper credit
(b) Did you mention the license of the assets? [No]
(c) Did you include any new assets either the supplemental material or as URL? [No]
(d) Did you discuss whether and how consent was obtained from people whose data you're 're using/curating? [N/A]
(e) Did you discuss whether the data you are using/curating contains personally identifiable information or offensive content? [No] MNIST/CIFAR only
13

---

5. If you used crowdsourcing conducted research with human subjects...
(a) Did you include the full text of instructions given to participants and screenshots, applicable? [N/A]
(b) Did you describe any potential participant risks, with links Institutional Review Board (IRB) approvals, if applicable? [N/A]
(c) Did you include the estimated hourly wage paid to participants and the total amount spent on participant compensation? [N/A]
14


Reviews:
[{"review_id": "jp4UtRICOWR", "reviewer": "Reviewer_HtX9", "summary": "The paper proposes an approach for neural network verification that combines zonotopes and Lagrangian decomposition. This is done by considering zonotope domains in each subproblem of the Lagrangian decomposition. The paper shows that solving these subproblems under zonotope domains is NP-hard (unlike box domains), and thus proposes a technique to relax the domain to a more tractable set by partitioning coordinates. In particular, it considers 2-dimensional zonotopes which are shown to have good properties in terms of tractability. An extended version merges partitions together, using MIP to solve the problem. Both are shown to produce good bounds at a reasonable time frame compared to other verification approaches.", "questions": "Minor details to be addressed:\n\n* The definition of the notation $\\sigma$ (the ReLU operator) is missing.\n* Please include $z_B$ in (3a) in the minimization terms for clarity.\n* In line 284, BDD+ is referred to before it is defined in Section 6; add at least a citation and if possible a sentence explaining what it is (as in Section 6).\n* In the initialization phase, it is not clear what the \"very minor improvements to DeepZ\" are (at least not without looking at the reference). Could you clarify this in the text?\n* The main text only specifies the number of neurons for each network (e.g. MNIST-Deep). Given how dependent on depth verification methods are, at least include number of layers, and layer types if possible.\n* Typos: \"Lagangian\" in line 30, \"perfrom\" in line 326, \"bouds\" in line 346, \"slighctly\" in line 359.", "limitations": "Appendix B carefully describes the limitations of the work in many ways, which is very much appreciated. I see no other limitations that need to be mentioned.", "rating": 7, "confidence": 4, "soundness": 4, "presentation": 3, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Neural network verification is a widely studied area and the need for better algorithms is still important, as current relaxations do not scale well to the very large networks used in practice. This paper is a solid step towards that direction, combining two approaches in verification that were previously distinct, zonotope-based bounding and Lagrangian decomposition.\n\nThe paper starts off with the simple idea of using zonotope domains in the subproblems of Lagrangian decomposition, and winds up systematically producing interesting results and methods: it proves that these subproblems become NP-hard, finds a more tractable relaxation to solve the subproblems, and shows how to incorporate box bounds in the process. Although these results lean to the incremental side, I consider all of these to be valuable contributions to the area, and as far as I am aware I believe that these contributions are novel. Furthermore, the paper is overall well-written, but there are a few minor details that could be included in the main text here and there (see \"Questions\" section).\n\nWhile there is an overhead in considering zonotopes in Lagrangian decomposition, the computational results show that it can push the bound significantly compared to other incomplete verification algorithms. That said, one issue is that it is difficult to know whether this approach is worth it end-to-end as it does not compare with approaches tuned for similar solve times, but it could be viewed as a reasonable middle ground between cheap and expensive methods. Moreover, even if it is not immediately clear as to what situations one might prefer this approach, I can imagine future papers building on this idea as one can consider tighter domains within Lagrangian decomposition.\n\nOverall, while this work is incremental, it executes well in combining the two ideas from the literature, and I do not see any major concerns. Therefore, I recommend acceptance.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "bSGisz_ik-I", "reviewer": "Reviewer_ChY4", "summary": "The paper considers the ReLU-based neural network verification problem, where\nit builds on the Lagrangian relaxation of the corresponding optimisation\nproblem by approximating intermediate layer bounds with zonotopes, which can be\npartitioned when evaluating the dual with ReLU constraints. The approach is\nexperimentally evaluated and compared with the SoA on a number of networks\ntrained on the MNIST and CIFAR-10 datasets.\n", "questions": "Please see comment on Weaknesses.", "limitations": "These are sufficiently addressed.", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths\n\n- The method provides balances the strengths and weaknesses of fast but\n  imprecise incomplete neural network verification  and exact but slow complete\n  verification (for verification purposes this is useful in practice as the\n  method can be used after methods with less precision have failed and before\n  exact methods are used).\n\n- It so does by connecting Lagrangian decomposition with zonotope-based neural\n  network verification in a novel manner.\n\n- The exposition of this is well written and presented.\n\n- Good experimental evaluation.\n\nWeaknesses\n\n- Whilst the efficacy of the method relies on accounting of neuron interactions\n  in the dual evaluation, it is not compared with semidefinite programming\n  approaches that also account for these interactions.\n", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "PtQYh8RbcQ", "reviewer": "Reviewer_ogn5", "summary": "The paper proposes a solution to the problem of neural network verification based on dual Lagrangian optimization. The main insight here is bounding the range of dual variables using Zonotopes to capture inter-neuron dependencies not considered by prior work. However, using Zonotopes for Lagrangian optimization makes the optimization harder. To address this issue, the authors design new algorithms to evaluate the dual function efficiently. ", "questions": "* In terms of theoretical precision, how does the proposed approach compare with other incomplete verifiers such as PRIMA/beta-crown (when not run in complete mode). Are they incomparable? If yes, then it will be good to investigate other cases where the proposed approach gets better results than these baselines.\n\n* The statement \"unlike PRIMA, ZD can directly be plugged into branching frameworks.\" is not true as the recent work of https://openreview.net/forum?id=l_amHf1oaK uses PRIMA based constraints for branch and bounds.\n\n*  Have you experimented with higher dimensional Zonotopes (e.g., 3 or 4)? or it becomes not feasible beyond the 2D setting? if not, is it possible to maybe compute some sort of approximation (as PRIMA does for k-ReLU) in higher dimension to reduce the cost but still gaining precision?\n\n* In Fig. 5, why not change also the scale factor of the Box informed Zonotope as done in [23]? Does it interfere with the convergence of your method?\n\n* For handling the sigmoid activations, can a MILP approximation (as proposed in https://openreview.net/pdf?id=LQtlOn64EK6Y) be employed to convert the optimization defined over sigmoid functions to ReLU ones?\n\n* \"All prior dual approaches have chosen the sets $z_k$ to be axis-aligned hyperboxes\" however $\\beta$-CROWN is also dual based (as mentioned on line 370) and does not rely on hyperboxes?\n", "limitations": "The authors mention the limitations of their method. The paper does not make any contributions that can have a potential negative societal impact.", "rating": 7, "confidence": 5, "soundness": 3, "presentation": 4, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths:\n+ Neural network verification is a highly relevant problem for the NeurIPS audience. There have been several papers on the topic in recent years at NeurIPS.\n\n+ The writing is rigorous yet understandable. The authors do a great job of presenting their technical ideas at the right level of abstraction.\n\n+ The high-level idea of combining Zonotope analysis with dual Langrangian optimization for NN verification is novel and interesting. However, leveraging this insight to develop a scalable and precise verifier requires tackling several technical challenges. The authors develop solid algorithms to overcome these issues.\n\nWeaknesses:\n+ For neural network verifiers, the ultimate metric that matters are the number of verification instances verified. The results in Table 4 show that the method cannot outperform the state-of-the-art. Therefore the usefulness of the proposed approach is unclear.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "FE7DQI-Wlmk", "reviewer": "Reviewer_vLdB", "summary": "The authors present a novel algorithm to compute bounds on the values of neural network activations. \nBounding algorithms heavily rely on bounds on the network intermediate activations, which are represented as hyper-boxes and neglect interactions across the neurons in the same layer.\nLeveraging a modified version of a Lagrangian decomposition from the literature, the authors devise a technique to take zonotope constraints into account in the dual optimization, tightening the resulting bounds yet paying a price in terms of computational efficiency.", "questions": "- As commonly done in the related literature, the authors should evaluate their algorithm within BaB to test whether it still pays off for complete verification. \n\n- Run stronger incomplete verification baselines (e.g., alpha-CROWN on both intermediate bounds and output bounds, both via joint and sequential (yet parallel) optimization).\n\nI believe the paper is potentially of great interest to the community, and could greatly benefit from addressing the questions above.", "limitations": "Except those associated to the questions outlined above, the authors adequately address the limitations of their work.", "rating": 4, "confidence": 5, "soundness": 2, "presentation": 2, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "**Strengths.**\nThis is the first paper that employs zonotope domains for intermediate bounds in the context of neural network verification: the idea is definitely novel and interesting, and the authors provide non-trivial solutions to the technical problems associated to the formulation.\n\n**Weaknesses.**\nThe paper has two major weaknesses: one experimental, the other related to the presentation.\nThe experiments fail to show that \"ZonoDual outperforms the state-of-the-art baselines of the linear programming relaxation and the tightest dual verification methods, in terms of both the tightness of the bounds and runtime.\". First of all, the trade-offs of a bounding algorithm need to be assessed within complete verification, which allows to evaluate the tightness of the bounds against their time and memory cost in a fair manner. In Table 4, Beta-CROWN attains significantly tighter bounds in less time than ZD, hinting at disadvantageous speed-accuracy trade-offs.\nFurthermore, I am not convinced by the incomplete verification experiments. The authors fail to specify which intermediate bounds are employed for the baselines: I would assume bounds from the Kolter and Wong work, as in [9] and [25]. As shown by the authors, these bounds are necessarily looser than the zonotope domains (yet significantly cheaper to compute), so I believe this is not a fair comparison. Indeed, ZD is typically run for longer than some of the baselines, and zonotope intermediate domains are not guaranteed to be tighter than hyperboxes computed via CROWN or alpha-CROWN (or slope-optimized LiRPA). The authors should take this into account.\n\nFinally, I think the quality of the presentation would be improved if the authors focused less on the supposed dichotomy between primal and dual bounding algorithms (many dual algorithms are formulated from primal relaxations, such as [9] and [25], which they can potentially solve due to strong duality), and more on the fact that they propose to employ zonotope-based intermediate bounds, as opposed to hyper-boxes.\n\n\nLiRPA: https://arxiv.org/pdf/2002.12920.pdf\nAlpha-CROWN: https://openreview.net/pdf?id=nVZtXBI6LNn", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "-L00SBK4rpx", "reviewer": "Reviewer_6f9Q", "summary": "The paper aims at verify outputs of neural networks for a given input range. Based on a branch-and-bound strategy, the paper develops an approach to approximating bounds by solving a verification problem of 2-layer neural networks, which is a subproblem obtained by a branching procedure that performs Lagrange decomposition of an entire verification problem. A key idea of the approach is to use zonotopes, which are expressive and easy to handle computationally.  The experiments demonstrate the usefulness of the proposed approach.  The paper also conducted experiments to demonstrate the usefulness of the approach.", "questions": "Can the concerns and questions described as the weaknesses be addressed?", "limitations": "Limitations seem to be addressed adequately.", "rating": 6, "confidence": 2, "soundness": 1, "presentation": 1, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "### Strength\n- The interesting use of zonotopes for neural network verification.\n- The complexity for the computation with zonotopes are provable given.\n\n### Weakness\nThe presentation is hard to follow.  Specifically, I can't find the following in the paper.\n- It is not clear for me how to ensure correctness of the bounds provided by the proposed approach.\n- It is not clear how to read the figures and tables in the paper.  Thus, I can't check the claims in the paper is correct.\n- It is not clear whether the bounds the paper provides are tighter than those provided by the approach in [25] theoretically or experimentally.  If the latter, where is a formal claim and proof for it?\n- Why is Proposition 4.2 important?  In L160, the paper says \"The second proposition describes an improved pushforward operator that offers improvements against DeepZ\", but I'm not sure why Z' in the proposition is an improvement.\n\nThe following is minor.\n- What is \\sigma in (1c)?\n- Why is Wk, not Wk+1, used in (3c)?\n- What does \"the most negative\" mean in L252?\n\n### Post-Response\nSome of my concerns were addressed by the author response, so my score raised from 4 (borderline reject) to 6 (weak accept).", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}]

Author rebuttal:

Decision: Accept