Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound
Authors: Claudio Ferrari
Mark Niklas Mueller
Nikola Jovanović
Martin Vechev
Venue: ICLR 2022 Poster (2022)
Keywords: Certified Robustness
Branch-and-Bound
Convex Relaxation

Abstract: State-of-the-art neural network verifiers are fundamentally based on one of two paradigms: either encoding the whole verification problem via tight multi-neuron convex relaxations or applying a Branch-and-Bound (BaB) procedure leveraging imprecise but fast bounding methods on a large number of easier subproblems. The former can capture complex multi-neuron dependencies but sacrifices completeness due to the inherent limitations of convex relaxations. The latter enables complete verification but becomes increasingly ineffective on larger and more challenging networks. In this work, we present a novel complete verifier which combines the strengths of both paradigms: it leverages multi-neuron relaxations to drastically reduce the number of subproblems generated during the BaB process and an efficient GPU-based dual optimizer to solve the remaining ones. An extensive evaluation demonstrates that our verifier achieves a new state-of-the-art on both established benchmarks as well as networks with significantly higher accuracy than previously considered. The latter result (up to 28% certification gains) indicates meaningful progress towards creating verifiers that can handle practically relevant networks.

Published as a conference paper at ICLR 2022
COMPLETE VERIFICATION VIA MULTI-NEURON RELAXATION GUIDED BRANCH-AND-BOUNE
Claudio Ferrari, Mark Niklas Müller, Nikola Jovanović, Martin Vechev
Department of Computer Science, ETH Zurich, Switzerland (claudio. ferrari,
nikola. jovanovi,, partin..echevv wim.ee...cii......cchc..
ABSTRACT
Sfateoofthheart neural network verifiers fundamentally based of two paradigms: either encoding the whole verification problem via tight multi-neuron convex relaxations applying Branch-and-Boun imprecise but fast bounding methods on a large number of casier subproblems. The former can capture complex multi-ncuron dependencies but sacrifices com- pleteness due to the inherent limitations of convex relaxations. The latter en- ables complete verification but becomes increasingly ineffective on larger and more challenging networks. In this work, we present novel complete verifier which combines the strengths of both paradigms: it leverages multi-neuron re- laxations to drastically reduce the number of subproblems generated during the BaB process and an efficient GPU-based dual optimizer to solve the remaining state-
(BaB) procedure leveraging
ones. An extensive evaluation demonstrates that our verifier achieves of-the-art on both established benchmarks as well as networks with significantly higher accuracy than previously considered. The latter result (up 28% certi- fication gains) indicates meaningful progress towards creating verifiers that can handle practically relevant networks.
INTRODUCTION
Recent years have witnessed substantial interest in methods for certifying properties of neural net- works, ranging from stochastic approaches (Cohen et al. (219) which construct robust model from an underlying base classifier to deterministic ones (Gehr et al., 2018: Katz et al. 2017 Xu et al. 2020 that analyze given network is (the focus of our work).
Scalable and Precise Non-Linearity Handling Deterministic verification meth- ods can be categorized as complete or incomplete. Recent incomplete verification methods based on propagating and refining single convex region (Müller et al.)
Key Challenge:
et al. [2020] Tian-
draatmadja et al. 2020) are limited in precision due to fundamental constraints imposed by convex relaxations. Traditional complete verification approaches based on SMT solvers (Ehlers (017) or a single mixed-ine -ittegr linear programming encoding
property (Tjeng et al.) 2019] Katz et al, 2017) suffer from worst-case exponential complexity and are often unable to compute sound bounds in reasonable time-frames. To address this issue, a Branch-an saunch-and--ae Bound approach (Bunel et al., 2020) has been popularized recently: anytime-valid bounds computed by recursively splitting the prob- lem domain into easier subproblems and deriving bounds on each of these via cheap and less precise methods (Xu et al. 2021; Wang al., 2021 Palma al., 2021 Henriksen & Lomuscio 1021)
This approach has proven effective on (smaller l networks where there are relatively few unstable activations and splitting a problem simplifies it substantially. However, for larger networks or those not regularized to be amenable to certification this strategy becomes increasingly ineffective as the larger number of unstable activations makes individual splits less effective, which is exacerbated by the relatively loose underlying bounding methods.
This Work: Branch-and Bound guided by Multi-Neuron Constraints In this work, we propose novel certification method and verifier, called Multi-Neuron Constraint Guided BaB (MN-BABI BBBB,, which aims to combine the best of both worlds: it leverages the tight multi- constraints pro- posed by Müller al. (2022) within a BaB framework to yield efficient GPU-based dual method.

---

Published as a conference paper at ICLR 2022
The key insight is that the significantly increased precision of the underlying bounding method substantially reduces the number of domain splits (carrying exponential cost) required to certify a property. This improvement is especially pronounced for larger and less regularized networks where additional splits of the problem domain yield diminishing returns. We release all code and scripts to reproduce our experiments at httpp::/ggttubb.com wwwpttu......ettttteeeeeeeeeeeet wwwm//ttssrr/mnneeeee sri/mn-bal
Main Contributions:
We present novel verification framework, MN-BAB, which leverages tight multi-neuron constraints and a GPU-based dual solver in a BaB approach.
We develop novel branching heuristic, ACS, based on information obtained from analyz- ing our multi nulti-neuron constraints.
We propose a new class of branching heuristics, CAB, applicable to all BaB-based veri- fiers, that correct the expected bound improvement of branching decision for the incurred computational cost.
Our extensive empirical evaluation demonstrates that we improve on the state of the art in terms of certified accuracy by much as 28% on challenging networks.
2
BACKGROUND
In this section, we review the necessary background for our method (discussed next).
2.1 NEURAL NETWORK VERIFICATION
The neural network verification problem be defined as follows: given network f X' - y, an input region D C X, and a linear property P S y over the output neurons E V, prove fxx E P, Vo D. We instantiate this problem with the challenging for -norm bounded perturbations and set DD to the foo ball around an input point Zo of radius e: (xo) {x E X || æolloo S S]}.
For ease of presentation, we consider neural networks of L fully-connected layers with ReLU acti- vation functions (we note that MN-BAB can handle a wide range of layers including convolutional, residual, natth-normalization, and sverage-pooling layers). We focus on ReLU networks as the BaB framework only yields complete verifiers for piecewise linear activation functions but remark that our approach is applicable to a wide class of activations including ReI.U, Sigmoid, Tanh, MaxPool, and others. We denote the number of neurons in the 2th layer as d, and the corresponding weights and biases as (i) E RR dd:
xd; and (()) e R for E {1, .... L). Further, the neural network is defined
as f(x) == (x) where 200 (x) == (i-1) (x) + (() and z (+)) (x) = ma 2()) (x)). For readability, we omit the dependency of intermediate activations on ar.
Since we can encode any linear property over output neurons into an additional affine layer, we can simplify the general formulation fx) P to fxx > The property can now be verified by
proving that lower bound to the following optimization problem is greater 0:
min (mo)
(xx (T.)
s.t.
{ = (i)) 2((2 (i-1) + (())
(1)
z max(0, (
method is called sound if every property it proves actually holds (no false positives). A method is called complete if it can prove every property that actually holds (no false negatives).
2.2 BRANCH-AND- AND-D FOR VERIFICATION
Bunel et al. (2020) successfully applied the Branch-and-Bonl Bound (BaB) approach (lan 1960) to neural network verification. It consists of a bounding method that computes sound upper and lower bounds on the optimization objective of Eq. I and a branching method that recursively splits the problem into subproblems with added constraints, allowing for increasingly tighter bounds. If an upper bound (primal solution) < is found, this represents a counterexample and allows to terminate the proce- dure. If lower bound 0 is obtained, the property is verified the corresponding ssub))domain
2

---

Published as a conference paper at ICLR 2022
If lower bound > 0 is derived on all subdomains, the property is verified. An ideal splitting pro- cedure minimizes the total time required for bounding. which often well approximated by the number of considered subproblems. A simple approach is to split the imput domain, however, this is inefficient for high-dimensional input spaces. Splitring ReL. activation node into its positive and negative phases has been shown to be far more efficient (Bunel et al. (020) and ultimately yields complete verifier (Wang et al. 2021 Hence, we focus solely on ReLU branching strategies.
2.3 LINEAR CONSTRAINTS
max x))
The key challenge in neural network verification Eq. is handling the non-linear activations. Stable ReLUs, i.e., those which we can show to be always active (8 2 0) or in- active (2 < 0), can be replaced by linear functions. Unsta- ble ReLUs, ie.. those that can be either active or inactive depending the exact D, have to be approximated using a convex relaxation of their input- set. We build the convex relaxation introduced in DEEPPOLY Singh et al. (019b) and shown in Fig. [ Its key property the single linear upper and lower bound, which allows for efficient bound computation.
U - (x
uy
y/ our
Myr
Figure 1: Illustration of the DEEP- POLY relaxation of ReLU activation = max(æ, 0) given the neuron-wise bounds E [Lzy Uz] and parametrized by E [0, 1].
2.4 MULTI-NEURON CONSTRAINTS
All convex relaxations that consider ReLU neurons in- dividually are fundamentally limited in their precision by the so-called (single-ncuron) convex relaxation barrier (almmnn al., 2019). It be overcome by considering multiple neurons jointly (Singh et al.) 2019a Tjandraat- madja al. 2020 Müller et 2002 Palma al.) 2021),
2-neuron
single-neuron F9
B2
thereby capturing interactions between these neurons and obtaining tighter bounds, illustrated in Fig. 2 We leverage the multi-ncuron constraints from Müller et al. (2022), ex- pressed as a conjunction of linear constraints over the joint input and output space of ReLU layer.
Comparison of multi- neuron and single-neuron constraints projected into y2-2i -22 Space. Repro- duced from Müller et al. (022))
Figure 2:
2.5 CONSTRAINED OPTIMIZATION VIA LAGRANGE MULTTIP.IERS
To express constraints as part of the optimization problem, we use the technique of Lagrange mul- tipliers. Given a constrained minimization problem min& f fxx), s.t. g(æ) < O, we can bound the objective function with:
min f(x) 2 min max f(x) + \g A
If constraint is satisfied, i.e., g(x); < 0, A 0 maximizes the (inner) objective, else, i.e., g(x), 0, increasing A allows the objective grow unboundedly, shifting the minimum over æ until the constraint is satisfied. Hence, if X > 0 after optimization, the constraint is active, i.e., it is actively enforced and currently satisfied with equality.
A MULTI-NEURON RELAXATION BASED BAB FRAMEWORK
In this section, we describe the two key components of MN-BAB: (i) an efficient bounding method leveraging multi-neuron constraints, well as constrained optimization via lagrange multipliers (3.1 and (ii) a branching method tailored (32))
EFFICIENT MULTI-NEURON BOUNDING
We build on the approach of Singh al. (2019b), extended by Wang et al. (2021) of deriving lower bound if as a function the network inputs and set of optimizable parameters. Crucially, tighten these relatively loose bounds significantly by enforcing precise multi-neuron constraints
3

---

Published as a conference paper at ICLR 2022
via Lagrange multipliers. To enable this, we develop a method capable of integrating any linear constraint over arbitrary neurons anywhere the network into the optimization objective. At a high level, we derive linear upper and lower bounds of the form 2(() S az(1 + e for every layer's out- put in terms of its imputs (1 Then, starting with a linear expression in the last layer's outputs z(() which we aim to bound, use the linear bounds derived above, replace 2(4) with symbolic bounds depending only the previous layer's values 2( We proceed in this manner recur- sively until we obtain an expression only in terms of the networks inputs. Below, we describe this backsubstitution process for ReLU and affine layers.
Affine Layer Assume any affine layer ( w(0 + ( and lower bound f 20)) 200 with respect to its outputs. We then substitute the affine expression for g()) to obtain:
w( + b + a (i-1) 21 (i-1) (i-1)
a(i-1)
cb-11
ReLU Layer Let f al0)) e be a lower bound with respect to the output ReLU
layer 2 max(0, 2()) and ( and ( bounds its input s.t. ((t] 2(0) S n() obtained by recursively applying this bounding procedure or using a cheaper but less precise bounding method (Singh et al. (2018) Gowal et al. 2018). The backsubstirution through ReLU layer now consists of three distinct steps: I) enforcing multi-neuron constraints, 2) enforcing single-neuron constraints to replace the dependence on x1) by g((), and 3) enforcing split constraints, which we describe in detail below.
Enforcing Multi-Neuron Constraints We compute multi neurinneuron constraints as described in Müller al. (2022), although our approach is applicable to any linear constraints in the input-output space of ReLU activations, written as:
p(()
p(0)
-p(9]
S.
where 2(1) are the pre- and (0) the post-activation values and p(t), p(t), and 60 the constraint parameters. We enforce these constraints using Lagrange multipliers (see $2.5 yielding sound
lower bounds for all 7(0) (R20)<; where e; denotes the number of multi-neuron constraints in
layer i.
a + c!0) 2 max a (5) (1) + (()) + + ( + p(0)(0 (0)
70)20
max (a (+) p()) 21) (+) p(ù (0) (T) ( 7020
(1)
e((o)
Note that this approach can be easily extended to linear constraints over any activations in arbitrary layers if applied in the last affine layer at the very beginning of the backsubstitution process.
Enforcing Single-Neuron Constraints We now apply the single-neuron DEEPPOLY relaxation with parametrized slopes a collected D (see below):
max (60 (())2() + (6) > max 70
(
+ +b ) c00)
05a 91
())
0 200 + t (()
max 05a gl
7 20
a
en(()
The intercept vector b and the diagonal slope matrix D defined as:
if l 2 0 or node j is positively split
0
if uj S 0 or node j is negatively split
Dj.i
Oj
if l < 0 < uy and a₂ 2 0
M4
if l 0 < uy and a < 0
My
4

---

Published as a conference paper at ICLR 2022
= < u and ag
b2
otherwise
Where we drop the layer index for readability and 0j is the lower bound slope parameter illustrated in Fig. Note how, depending whether the sensitivity dj of [ w.r.t. =) has positive negative
sign, substitute z)
(6) for its lower upper bound, respectively.
Enforcing Split Constraints We encode split constraints of the form diagonal split matrix S as follows, again dropping the layer index i:
2) 2 or 2/ S
using the
positive split: 2 2
Sjo = 1
negative split: & < 0 no split
5( 50
We again enforce these constraints using Lagrange multipliers:
max a (())2(1 ((()) ( Ø1 70)
(a
(() + + s(i)) 200 )()))())))))))))))))))))))))))
d(()
max
(5a
3 20
a!!()
(02 20
Putting everything together, the backsubstitution operation through a ReLU layer is:
min a (+)) + c(t)) sED
min max ((a + (0) xED (5
(())pp p(() ( g ((1) 7 (1) pb(t) 2(0)
80220
a
20
+ (a + + p + ( (-) + c(
Full backsubstitution through all layers leads to an optimizable lower bound on
min f(x) 2 min max a (0) =DD
+ (0)
max min a (0) (0)
#ED 0
05 #ED
05B UST
050
05
(4)
where the second inequality holds due to weak duality. We denote all a from every layer of the backsubstitution process with a and define B3 and y analogously. The inner minimization over æ has closed form solution if D is an bp-ball of radius around æo. given by Hölder's inequality:
max min a (0) + (00) > max a (0) (0) - 1|a (U)T 11, (0) 05a51 aED
(5)
0sa<1
050
0
O
where q is defined s.t. + - 1. Since these bounds are sound for any S a I 1, and 3, 2 0, we tighten them by using (projected) gradient ascent to optimize these parameters.
We compute all intermediate bounds using the same bounding procedure, leading two full param- eter sets for every neuron in the network. To reduce memory requirements, we share parameter sets between all neurons in the same layer, but keep separate sets for upper and lower bounds.
Upper Bounding the Minimum Objective Showing upper bound the minimum optimiza- tion objective precluding verification (f < 0) allows us to terminate the BaB process early. Prop- agating any input æ D through the network yields valid upper bound, hence, we use the input that minimizes Eq. 5):
(2o); te if a < 0
(0)
2;
(2o);
if a; 2 0
(0)
5

---

Published as a conference paper at ICLR 2022
3.2 MULTI-NEURON CONSTRAINT GUIDED BRANCHING
Generally, the BaB approach is based on recursively splitting an optimization problem into easier subproblems to derive increasingly tighter bounds. However, the benefit of different splits can vary widely, making an effective branching heuristic which chooses splits that minimize the total number of required subproblems a key component of any BaB framework (Bunel et al.) 2020). Typically, a score is assigned based the expected bound improvement and the most promising split is chosen. Consequently, the better this score captures the actual bound improvement, the better the resulting decision. Both the commonly used BABSR (Bunel al.) 2020 and the more recent FSB (De Palma jet al. 2021) approximate improvements under a DEEPPOLY style backsubstitution procedure. As neither considers the impact of multi-neuron constraints, the scores they compute might not be suitable proxies for the bound improvements obtained with our method. To overcome this issue, we propose novel branching heuristic, Active Constraint Score Branching (ACS), considering multi-neuron constraints. Further, we introduce a branching heuristic framework which corrects the expected bound improvement with the potentially signifieantly varying expected computational cost.
Active Constraint Score Branching The value of a Lagrange parameter Y provides valuable in- formation about the constraint it enforces. Concretely, y > 0 indicates that constraint is active, ie.. the optimal solution fulfills it with equality. Further, for a constraint g(x) I 0, larger (g(() indicates larger sensitivity of the final bound to violations of this constraint. We compute this sensitivity for our multi-neuron constraints with respect to both ReLU outputs and inputs as y P and Y P. respectively, where P and P are the multi-neuron constraint parameters. We then define our branching score for a neuron j in layer as the sum over all sensitivities with respect to its input or output:
$. = by (0) pp + (6) (())p(())
(6)
Intuitively, splitting the node with the highest cumulative sensitivity makes its encoding exact and effectively tightens all of these high sensitivity constraints. We can efficiently compute those scores without additional backsubstitution pass.
Cost Adjusted Branching Any complete method will decide every property eventually, Hence, its runtime is key performance metric. Existing branching heuristics ignore this aspect and only consider the expected improvement in bound-tightness, but not the sometimes considerable differ- ences in computational cost. We propose Cost Adjusted Branching (CAB), scaling the expected bound improvement (approximated with the branching score) with the inverse of the cost expected for the split, and then picking the branching decision yielding the highest expected bound improve- ment per cost. The true cost of a split consists of the direct cost of the next branching step and the change of cumulative cost for all consecutive steps. We find local approximation considering just the former component, similar to only considering the one-step bound improvement, to be a good proxy. We approximate this direct cost by the number of floating- poiiin operations required to com- pute the new bounds, refer to App. B for a more detailed description. Note that any approximation of the expected cost can be used to instantiate CAB.
Enforcing Splits Once the ReLU node to split on has been determined, two subproblems are generated. One where non nen-negative 2 2 0 and one where non non-positive 2 < 0 pre-activation value has to be enforced. This accomplished by setting the corresponding entries in the split matrix S. used during the bounding process, to -1 and 1, respectively. As the intermediate bounds for all layers up to and including the one that was split remain unchanged, we do not recompute them.
3.3 SOUNDNESS AND COMPLETHNESS
The soundness of the BaB approach follows directly from the soundness of the underlying bounding method discussed in Section 3.1 To show completeness, it is sufficient to consider the limit case where all ReLU nodes are split and the network becomes linear, making DEEPPOLY relaxations exact. To also obtain exact bounds, all split constraints have to be enforced. This can be done by computing optimal / for the now convex optimization problem (Wang et al., 2021). It follows that a property holds if and only if the exact bounds thus obtained are positive on all subproblems. We conclude that MN- BAB is complete verifier.

---

Published as a conference paper at ICLR 2022
Table 1: Natural accuracy [%] (Acc.), verified accuracy [%] (Ver.) and its empirical upper bound [%] and average runtime [s] of the first 1000 images of the test set.
MN-BAB (ours) BABSR +CAB
MN-BAB (ours) ACS +CAB
Dataset
Model
Acc.
ERAN
OVAL
B CRowN
Upper Bound
Ver.
Time
Ver.
Time
Ver.
Time
Ver.
Time
Ver.
Time
MNIST
ConvSnall
98.0
0.12
73.2
38.4
69.8
26.2
71.6"
46
71.0
21.3
70.3
26.2
73.2
Conväig
0.30
78.6
6.0
77.71
78.3
20.8
77.2
ConvSuper
97.7
0.18
0.5
142.0
19.2
86.2
17.6
90.9
37.3
CIFARIO
ConvSnall
63,0
2/255
47.2
54.4
46.2
17.7
46.3
18
46.1
16.4
45.8
18.0
48.
ConvBig
63.1
2/255
48.2
128.1
50.6
42.0
50.31
55
49.4
49.5
51.5
37.0
55.0
ResNet6.A F
45.0
114.6
52.0
263.4
48.0
55.0
170.7
ResNet6-B 1
79.0
1/255
66.0
48.6
67.0
105.7
65.0
51.1
67.0
37.8
71.0
RosNe18-A
83.0
1/255
11.0
362.5
18.0
497.3
19.0
390.7
23.0
371.0
70.0
Errors prevent reporiing reliable numbers.. first 100 samples the set. -VVAL does not support ResNet architectures.
We repurt numbers from Wang al. Y2021]
Due to long runtimes, we evaluated only on the
4 EXPERIMENTAL EVALUATION
We now present an extensive evaluation of our method. First, and perhaps surprisingly, we find that existing MILP-based verification tools (Singh et al., 2019e] Müller al. (022) are more effective in verifying robustness on many established benchmark networks than what is considered state-of-the- art. This highlights that next-generation verifiers should focus on and be benchmarked using less regularized and more accurate networks. We take step in this direction by proposing and comparing on such networks, before analyzing the effectiveness of the different components of MN-BAB in an extensive ablation study.
Experimental Setup We implement GPU-based version of MN-BAB in PyTorrhh (Paszke et al. 2019) and evaluate all benchmarks using a single NVIDIA RTX 2080Ti, 64 GB of memory, and 16 CPU cores. We attempt to falsify every property with an adversarial attack, before beginning certification. For every subproblem, we first lower-bound the objective using DEEPPOLY and then compute refined bounds using the method described in 3
Benchmarks We benchmark MN-BAB on wide range of networks (see Table 3 in App. A on the MNIST (Deng) 2012) and CIFARIO datasets (Krizhevsky et al., 2009). We also consider three new residual networks, ResNet6-A, ResNet6 B, and ResNet8-A, AA. ResNet6-A A and ResNet6-B have the same architecture but differ in regularization strength while ResNet8-A A has an additional residual block. All three were trained with adversarial training (Madry et al. 2018 using PGD, the GAMA
loss (Sriramanan et al. 2020) and MixUp data augmentation (Zhang et al. 2021 ResNet6-A A and ResNet8 A were trained using 8-steps and 4/255, whereas 20-steps and c 8 /255 were used for ResNet6-B B. We compare against 3-CROWN (Wang et al. (002)) a based state-of-the- complete verifier, OVAL (Palma et al. 2021 De Palma al.] 2021 Bunel et al. 2020). a BaB frame- work based on a different class of multi-neuron constraints, and ERAN/Singh et al. (019c);; Müller al. (2022) combining the incomplete verifier PRIMA, whose tight multi-neuron constraints we leverage in our method, and a (partial) MILP encoding.
Comparison to State-of-the-Art Methods In Table I we compare the verified accuracy and run- time of MN-BAB with that of otate-of-the-art tools ERAN, 3-CROWN, and OVAL. Perhaps sur- prisingly, we find that both MNIST and the smallest CIFARIO benchmark network established over the last years (Singh et al. 2019b) can be verified completely or almost completely in less than 50s per sample using ERAN BRAN, making them less relevant as benchmarks for new verification tools. On these networks, all three BaB methods (including ours) are outperformed to a similar degree, with the reservation that we could not evaluate OVAL on MNIST ConvBig due to runtime errors. On the remaining unsolved networks where complete verification via a MILP encoding does not scale, MN-BAB consistently obtains the highest certified accuracy and for all but one also the lowest run- time. On ConvSuper we were not able to find configurations for OVAL and 3-CROWN that did not run out of memory. Comparing the BaB methods, we observe overall trend that more precise but also expensive underlying bounding methods are most effective on larger networks, where addi- tional splits are less efficient, and complex inter-neuron interactions multi-neuron constraints. On these networks, the more complex interactions also lead to more active Nulti-Neuron Constraints (MNCs) and hence more informative ACS scores.
be captured by the precise
7

---

Published as a conference paper at ICLR 2022
Subpeobken vount notio
Subproblers oolee count rulio
Time [ ICSICAB
10
10a
300
RowNeet-AA ReeNeeti D
10
10'
150-
10
ResNet6
10"
BesNett A ResNectiB
ResNetG-B
10
0.
1.0
0.5
1.
150
300
420
Quantile
Quartile
Time [s] ACS
Figure 3: Ratio of subprob- lems required per property without and with MNCs.
Figure 4:
Ratio of subprob- lems required per property with BABSR and ACS.
Figure 5: Effect of Cost Ad- justed Branching on mean verification time with ACS.
Ablation Study To analyze the indi- vidual components MN-BaB, we con- sider the weakly and heavily regular- ized ResNet6-A and ResNet6-B, B, respec- tively, with identical architecture. Con- cretely, we show the effect different bounding procedures and branching ap- proaches have in the two settings in Ta- ble[] As verified accuracy and mean run- time are very coarse performance metrics, we also analyze the ratio of runtimes and number of subproblems required for ification on a per-property level, filtering out those where both methods verify be- fore any branching occurred (Figs. 3 Overall, we observe that the number of visited subproblems required for certifica- tion can be reduced by two to three orders of magnitude by leveraging precise multi- neuron constraints and then again by another one to two orders of magnitude by our novel branching heuristic, ACS, Our cost-adjusted branching yields additional speed up of around 50%.
Table Verified accuracy [%] (Ver.) and avg. runtime [s] on the first 100 images of the test set for 1/255).
Upper
Branching Method
MN-BAB
Model
Acc.
MNCs
Bound
Time
ResNet6-A
75
No Branching
n10
30
No Branching
39
13.2
BABSR
247.1
BABSR +CAB
46
219.3
FSB
yes
45
239.7
yes
BABSR +CAB
48
202.7
ACS
yes
186.4
ACS +CAB
55
170.7
Reshet6-8
79
71
No Branching
58
0.7
No Branching
yes
BABSR
78.3
BABSR +CAB
63
64.9
FSB
yos
67.0
BABSR
63
63.5
BABSR +CAB
yos
51.1
ACS
65
52.0
ACS +CAB
yes
37.8
The trend MN-BAB succeeding on more challenging net- works is confirmed here. Leveraging MNCs enables us to ver-
Time (s] MNC ACS+CAB
300
RoaNet6.A
ify 20% more samples while being around 22% faster (see Ta-
ReaNetti
ble 2 on ResNet6-A A while the more heavily regularized ResNet6-B we only verify 6% more samples. When analyzing on per-property level, shown in Fig. 6 the trend is even more pronounced. For easy problems, leveraging MNCs and ACS has little impact (points the lower left-hand corner). How- ever, it completely dominates on the harder properties where only using single-neuron constraints and BABSR takes up to 33 times longer (points below the diagonal).
150 Time [+] wo. MNC BaBSR
Figure 6: Per property verification times using MN-BAB over those without MNCs and using BABSR.
Effectiveness of Multi-Neuron Constraints In Fig. 3 we show the ratio between the number of subproblems required to prove the same lower bound the final objective (either 0, if both methods certify, or the smaller of the two lower bounds at termina- tion) with and without MNCs over the quantile of properties for ResNet6-A (blue) and ResNet6-B (orange). We observe that using MNCs reduces the number of subproblems for both networks by between two and three orders of magnitude. Despite the higher per bounding-step cost, this leads to the use of MNCs increasing the number of verified samples by up to 12% while reducing average certification times (see Table
Effectiveness of ACS Branching In Fig. 4 show the ratio between the number of subprob- lems considered when using BABSR vs. ACS over the quantile of properties. We observe that ACS yields significantly fewer subproblems on most (75%) or all properties R and
8

---

Published as a conference paper at ICLR 2022
ResNet6 respectively, leading an additional reduction by between one and two orders of mag- nitude and showing the effectiveness of our novel ACS branching heuristic. Average verification times are reduced by 12% and 21% ResNet6- A and ResNet6 B, respectively. Note that the rel- atively small improvements in timings are due to timeouts for both methods yielding equally high runtimes which dominate the mean. FSB is consistently outperformed by ACS, certifying 12% less samples on ResNet6-A, A.
Effectiveness of Cost Adjusted Branching In Fig. 5 we show the per property verification times with ACS + CAB over those with ACS. Using CAB is faster (points below the dashed line) for all properties, sometimes significantly so, leading to an average speedup of around 50%. Analyzing the results in Table 2 we observe that CAB is particularly effective in combination with the ACS scores and multi-neuron constraints, where bounding costs vary more significantly.
RELATED WORK
Neural Network Verification Beyond the Single Neuron Convex Barrier After the so-called (Single Neuron) Convex Barrier has been described by SSalman et al.] (2199) for incomplete relaxation-based methods, a range of approaches has been proposed that consider multiple neu- rons jointly to obtain tighter relaxations. Singh et al. (2019a) and Müller et al. (2022) derive joint constraints over the input-output space of groups of neurons and refine their relaxation using the intersection of these constraints. Tjandraatmadja et al. (2020) merge the ReLU and preceding affine layer to consider multiple inputs but only one output time. While the two approaches are theo- retically incomparable, the former yields empirically better results (Müller et al.
2022
Early complete verification methods relied on off-the-shelff SMT (Katz et al. 2017 Ehlers 2017)
or MILP solvers (Dutta et al., 2018] Tieng et al.) (019). However, these methods do not scale beyond small networks. In order to overcome these limitations, [Bunel et al. (2020) formulated a BaB style framework for complete verification and showed it contains many previous methods as special cases. The basic idea is to recursively split the verification problem into easier subproblems on which cheap incomplete methods
show robustness. Since then, range of partially (Xu)
ctt al. (02I) or fully (Wang et al.) 2021; ;::1: Palma et al. [021] GPU-based BaB frameworks have been proposed. The most closely related, Palma et al. (2021) ,. leverages the multi-neuron constraints from Tjandraatmadja et al.) (2020) but yields an optimization problem of different structure, as constraints
only ever include single output neurons.
Branching Most ReLU branching methods proposed to date use the bound improvement of the two child subproblems as the metric to decide which node branch on next. Full strong branching (Applegate et al., 1995) exhaustively evaluates this for all possible branching decisions. However, this intractable for all but the smallest networks. Lu & Kumar (2020) train a GNN to imitate the behavior of full strong branching at a fraction of the cost, but transferability remains open question and collecting training data to imitate costly. Bunel et al. 2020) proposed an efficiently computable heuristic score, locally approximating the bound improvement of branching decision using the method of Wong & Kolter (2018). Henriksen
Lomuscio (202T) refine this approach by additionally approximating the indirect effect of the branching decision. however, this requires using two different bounding procedures. De Palma et al. (202T) introduced filtered-smart. branchinbnnn (FSB), using BaBSK select branching candidates and then computing more accurate heuristic score only for the selected candidates. Instead of targeting the largest bound improvement, Kouvaros & Lomuscio (2021) aim minimize the number of unstable neurons by splitting the ReLU node with the most other ReLU nodes depending on it.
6 CONCLUSION
We propose the complete neural network verifier MN-BAB. Building on the Branch-and- Bound methodology, MN leverages tight multi-neuron constraints, novel branching heuristic and an efficient dual solver, able to utilize massively parallel hardware accelerators, to enable the verifica- tion of particularly challenging networks. Our thorough empirical evaluation shows how is particularly effective in verifying challenging networks with high natural accuracy and practical relevance, reaching a new state-of-the the- in several settings.

---

Published as a conference paper at ICLR 2022
7 ETHICS STATEMENT
Most machine learning based systems can be both employed with ethical as well as malicious pur- poses. Methods such ours that enable the certification robustness properties of neural networks are a step towards more safe and trustworthy Al systems and can hence amplify any such usage. Further, malicious actors might aim to convince regulators that the proposed approach sufficient to show robustness to perturbations encountered during real world application, which could lead to insufficient regulation safety critical domains.
REPRODUCIBILITY STATEMENT
We will make all code and trained networks required reproduce our experiments available during the review process as supplementary material and provide instructions on how to run them. Upon publication, we will also release them publicly. We explain the basic experimental setup Section and provide more details in Section A All datasets used in the experiments are publicly available. Random seeds are fixed where possible and provided in the supplementary material.
10

---

Published as a conference paper at ICLR 2022
REFERENCES
An automatic method of solving discrete programming problems. Econometrica, 28(3), 1960. ISSN 00129682, 14680262.
David Applegate, Robert Bixby, Vašek Chvátal, and William Cook. Finding cuts in the tsp (a preliminary report). Technical report, Citeseer, 1995.
Rudy Bunel, P Mudigonda, liker Turkaslan, Torr, Jingyue Lu, and Pushmeet Kohli. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 21(2020), 2020.
Jeremy M. Cohen, Elan Rosenfeld, and J. Zico Kolter. Certified adversarial robustness via random- ized smoothing. In Proc. of ICML, volume 97, 2019.
Sumanth Dathathri, Krishnamurthy Dvijotham, Alexey Kurakin, Aditi Raghunathan, Jonathan Ue- sato, Rudy Bunel, Shreya Shankar, Jacob Steinhardt, Ian Goodfellow, Percy Liang, and Pushmeet Kohli. Enabling certification of verinsiation-agnosiic networks via memory-effiiient semidefinite programming. In Advances Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual, 2020.
Alessandro De Palma, Rudy Bunel, Alban Desmaison, Krishnamurthy Dvijotham, Pushmeet Kohli, Philip HS Torr, and Pawan Kumar, Improved branch and bound for neural network verification via lagrangian decomposition. ArXiv preprint, abs/2104.06718. 2021.
Li Deng. The mnist database of handwritten digit images for machine learning research. IEEE Signal Processing Magazine, 29(6), 2012.
Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari. Output range analysis for deep feedforward neural networks. In NASA Formal Methods Symposium. Springer, 2018.
Ruediger Ehlers. Formal verification of piece-wise linear feed forward neural networks. In Interna- tional Symposium on Automated Technology for Verification and Analysis. Springer, 2017.
Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Mar- tin Vechev. Ai2: Safety and robustness certification of neural networks with abstract interpreta- tion. In 2018 IEEE Symposium on Security and Privacy (SP). IEEE, 2018.
Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Ue- sato, Relja Arandjelovic. Timothy Mann, and Pushmeet Kohli. On the effectiveness of interval bound propagation for training verifiably robust models. ArXiv preprint, Abs/1810.12275, 2018.
Patrick Henriksen and Alessio Lomuscio. Deepsplit: An efficient splitting method for neural net- work verification via indirect effect analysis. In Proceedings of the 30th International Joint Con- ference on Artificial Intelligence (IJCA121), To appear, 2021.
Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In International Conference on Computer Aided Verification. Springer, 2017.
Panagiotis Kouvaros and Alessio Lomuscio. Towards scalable complete verification of relu neu- ral networks via dependency-based branching. In Proceedings the 30th International Joint Conference on Artificial Intelligence (ICCAI2I), To Appear, 2021.
Alex Krizhevsky, Geoffrey Hinton, et al. Learning multiple layers of features from tiny images. 2009.
Jingyue Lu and M. Pawan Kumar. Neural network branching for neural network verification. In Proc. of ICLR, 2020.
Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards deep learning models resistant adversarial attacks. In Proc. of ICLR, 2018.

---

Published as a conference paper at ICLR 2022
Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev. Prima: General and precise neural network certification via scalable convex hull approximations. Proc. ACM Program. Lang., 6(POPL), jan 2022. doi: 10.1145/3498704. URL https://doi.
org/10. 1145/3498704
Alessandro De Palma, Harkirat S. Behl, Rudy R. Bunel, Philip H. S. Torr, and M. Pawan Kumar. Scaling the convex barrier with active sets. In Proc. of ICLR, 2021.
Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Köpf, 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. Advances in Neural Information Processing Systems 32: Annual Con- ference Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada, 2019.
Hadi Salman, Greg Yang, Huan Zhang. Cho-Jui Hsieh, and Pengchuan Zhang. A convex relaxation barrier tight robustness verification of neural networks. In Advances Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurlPS 2019, December 8-14, 2019, Vancouver, BC, Canada, 2019.
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin T. Vechev. Fast and effective robustness certification. In Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada, 2018
Gagandeep Singh, Rupanshu Ganvir, Markus Püschel, and Martin T. Vechev. Beyond the single neu- ron convex barrier for neural network certification. Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurlPS 2019, December 8-14, 2019, Vancouver, BC, Canada, 2019a.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certi- fying neural networks. Proceedings of the ACM on Programming Languages, (PPPL), 2019b.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin T. Vechev. Boosting robustness certi- fication of neural networks. In Proc. of ICLR, 2019c.
Gaurang Sriramanan, Sravanti Addepalli, Arya Baburaj, and Venkatesh Babu R. Guided adversarial attack for evaluating and enhancing adversarial defenses. In Advances Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurlPS 2020, December 6-12, 2020, virtual, 2020.
Christian Tjandraatmadja, Ross Anderson, Joey Huchette, Will Ma, Krunal Patel, and Juan Pablo Vielma. The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification. In Advances in Neural Information Processing Systems 33: Anmual Con- ference Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual, 2020.
Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In Proc. of ICLR, 2019.
Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsich, and Zico Kolter. Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. In ICML. 202/ Workshop on Adversarial Machine Learning, 2021.
Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. In Proc. of ICML, volume 80, 2018
Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang. Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. In Advances in Neural Information Processing Systems 33: Annual Con- ference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6- 2020, virtual, 2020.
12

---

Published as a conference paper at ICLR 2022
Kaidi Xu, Huan Zhang, Shiqi Wang. Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsich. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In Proc. of ICLR, 2021.
Linjun Zhang, Zhun Deng, Kenji Kawaguchi, Amirata Ghorbani, and James Zou, How does mixup help with robustness and generalization? In Proc. of ICLR, 2021.
13

---

Published as a conference paper at ICLR 2022
Table Overview the experimental configuration for every network.
#Activation Layers
#Activation Nodes
Dataset
Model
Training
Timeout
Batch sizes
MNIST
ConvSmall I
NOR
360
[100, 200, 400] [2, 2, 4, 8, 12, 20] [1, 2, 2, 3, 4,
3
3 604
ConvBig
DiffAl
2000
6
34 688
ConvSuper
DiffAl
360
88 500
CIFARIO
ConvSmall
PGD
360
[100, 150, 250]
3
852
ConvBig
PGD
500
13, 6, 6, 8, 16]
6
62 464
ResNet6-A
PGD
600
[4, 4, 8, 12, 16, 100]
6
10 340
ResNet6-B
PGD
600
[4, 8, 32, 64, 128, 256]
6
10 340
ResNet8-A A
PGD
600
[2, 2, 2, 4, 8, 16, 32, 64]
11 364 8
A EXPERIMENT DETAILS
In Table 3 we show the per-sample timeout and the batch sizes that were used in the experiments. The timeouts for the first 4 networks were chosen to approximately match the average runtimes reported by Wang et al. (02T). to facilitate comparability.
Since we keep intermediate bounds of neurons before the split layer fixed, as described in Sec- tion 3.2 the memory requirements for splitting at different layers vary. We exploit this fact and choose batch sizes for our bounding procedure depending on the layer where the split occurred.
In order to falsify properties more quickly, we run strong adversarial attack with the following parameters before attempting certification: We apply two targeted versions (towards all classes) of PGD (Madry et al. 2018) using margin loss (Gowal al. 2018) and GAMA loss (Sriramanan al. both with restarts, 50 steps, and 10 step output diversification (?).
2020
A.1 ARCHITECTURES
In this section, provide an overview of all the architectures evaluated in Section The ar- chitectures of the convolutional networks for MNIST and CIFARIO are detailed in Table The architectures of both ResNet6-A A and ResNet6-B B are given Table
Table 4: Network architectures of the convolutional networks for CIFAR10 and MNIST. All layers listed below are followed by an activation layer. The output layer is omitted. 'CONY hxw/s/p' corresponds to 2D convolution with output channels, an hxw w kernel size, stride of in both dimensions, and an all-around zero padding of p.
ConvSmall
ConvBig
ConvSuper
CONY 16 4x4/2/
CONY 32 3x1//11
CONY 32 3x.11100
CoNv 32 4x4/2A1
CONV 32 4x2///1
CoNY 32 4x4///00
FC
CONY 64 3x//1/1
CoNY 64 3x3/1/0
CONV 64 4x4/2/1
CONV 4x111/I
FC 512
FC 512
FC 512
FC 512
B PPLIT-COST COMPUTATION FOR CAB
Recall that for CAB, we normalize the branching score obtained with arbitrary branching heuris- tie with the (approximate) cost the corresponding split. The true cost of a split consists of the direct cost of the next branching step and the change of cumulative cost for all consecutive steps. As a local approximation, we just consider the former component.
We approximate this direct cost by the number of floating-pot point operations required to compute the new bounds. This computed as the sum of floating-poin operations required for bounding all intermediate bounds that recomputed. Our bounding approach only enforces constraints
14

---

Published as a conference paper at ICLR 2022
Table Network architecture of the ResNet6 and ResNet8. All layers listed below are followed by ReLU activation layer, except if they are followed by a RESADD layer. The output layer is omitted. 'CONV hxw/s/p' corresponds to 2D convolution with output channels, hxw kernel size, stride of in both dimensions, and an all-around zero padding of
ResNet6
ResNet8
CONV 3x3/1/1
CONV 16 x
CONY 1/20
CONY 32 3x33/11
CONY 1x/0
CONY 3x32/11
CONY 32 3x3/1/
CONY 32 3x3/1/1
RESADD
RESADD
CONY
CONY 64 3x3/2/1
CONV 1x1/200
CONY 3x3//11
CONV 64 3x3/111
CONY 64 3
RESADD
RESADD
FC 100
CONV 128 1/2/000
CONY 128 3/21
CONV 128 3x1/
RESADD
FC 100
on neurons preceding the neurons included in the bounding objective. Hence, we only recompute intermediate bounds for layers after the layer where the split occurs, as discussed in $3.2
To compute the cost of recomputing the lower (or upper) bound of one intermediate node, we add up all floating point operations needed to perform the backsubstitution described in $3.1] As backsub- stitution is just series of matrix multiplications, the number of required floating point operations can be deduced from the sizes of the multiplied matrices.
Thus if we split on layer & of an L layer network and the cost of backsubstituion from layer is C; and the number of nodes is di, the final cost of the split is:
2d,C.
4=++1
Where the factor 2 comes from the fact that for intermediate bounds we need to recompute both lower and upper bounds. The cost C, of full backsubstitution from layer i can be computed as the sum over the cost of backsubstituting through all preceding layers C, = Σj Cj. where the cost for a single layer can be computed as follows:
ReLU layer: Gj = dj + Pj. where Pj is the number of multi-neuron constraints.
Linear layer: Cj # W, where #W, is the number of elements in the weight matrix.
Conv layer: Gj dj dzk3. where kj the kernel size.
15


Reviews:
[{"review_id": "qNifCh8XgU6", "reviewer": "Reviewer_3m7j", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "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": "# Strengths of the paper:\nThe paper is easy to follow, and provide clear attributions of the ideas it is based on, citing the relevant works. The approach suggested makes sense and the authors have indicated that they will release the code to reproduce their results.\nThe empirical results that are included are useful to assess how much methods like beta crown can be extended to tighter relaxations.\n\n# Clarification needed\n## Q1: Clarification about Cost Adjusted Branching\nThe description of CAB is that it \"scales the expected bound improvement with the inverse of the cost expected for the split\".\nThere is no description about how \"the expected bound improvement\" is computed. If this the score given by a method like \"Active Constraint Score Branching\" or BABSR, I think it's inaccurate to call it like this.\nThere should be a clarification as to why different branching decisions have \"considerable differences in computational cost\". Is it simply because branching a \"late\" layer requires to recompute less intermediate bounds? This is unclear because nowhere is described what exactly you compute at each level (you could decide to tighten intermediate bounds based on the new branching constraints, even if they appear before the branching constraint)\n\n## Q2: Experimental evaluation not supporting the claim\nThe last contribution listed is that the authors \"improve on the state-of-the-art in terms of certified accuracy by as much as 26% while being 30% faster\". This numbers come from the experiments that are listed in Table 2, but this is only a comparison to different ablated version of the authors method. I understand that beta-crown would be equivalent to (BaBSR, no MNC) but this is still missing a comparison to other methods that use tighter relaxation than single neuron relaxation. Even if beta-crown and OVAL do not support residual connections, why not train a larger CNN if the issues of the models of table 1 is that the network are too easy?\nSimilarly, the only baseline used for Branching method proposed is BaBSR, while something like Filtered Smart Branching (FSB) could have been tested (the authors mention that method in their related works)\n\nWhen compared against strong baselines (Table 1), the improvements of the method proposed are significantly lower.\n\nIn addition, is there a reason why for Table 1, the branching is BaBSR+CAB for all but one of the networks, rather than ACS + CAB, given than ACS is one of the paper's contribution?\n\nThere is also the additional problems of comparing different branch and bound verifiers on only two numbers. With branch and bound verifiers, It is always possible to obtain higher verified accuracy if you are willing to trade off time (just do more branching steps). Comparing two methods based on only the verified accuracy and the time it took means that there is only a partial view and the result might depend on some settings with regards to termination. Why not follow the usual method of drawing cactus plots as is common in complete verification paper?\n\n# Small questions:\n- SQ1: Why is the verification attempt on MNIST in Table 1 given for eps=0.120? I am familiar with seeing verification for eps=0.1 or eps=0.3. Is there a motivation for departing from standard benchmarks?\n", "summary_of_the_paper": "This paper deals with complete verification of neural network, based on a branch and bound framework.\n\nIt is essentially a combination of two recent papers:\n- Beta-crown[1], which optimizes with first order methods the bounds obtained by LIRPA type bounds. Additional constraints on the network activations (such as the ones resulting from branching) are included through lagrange multipliers and optimized over.\n- Prima[2], which derives linear constraints to impose on the activation of the network to obtain tighter relaxations. These constraints comes from the fact that you can obtain a tighter convex hull by relaxing a group of neurons together, rather than relaxing each neuron independently. In the Prima paper, the constraints are simply encoded into an off-the-shelf LP solver.\n\nThe main contribution of this paper comes from adding the linear constraints that comes from the Prima relaxation (using Lagrange multiplier) to the problem optimized by Beta-crown.\n\nIn addition to that, the paper also propose new branching heuristics:\n- Active Constraint Score Branching, which uses the lagrangian variables associated with the constraints of the multi-neuron relaxation to prioritize branching.\n- Cost Adjusted Branching, which aim to correct the score of the branching heuristic based on the expected computational cost induced by each possible branching choice.\n\nExperiments are ran on MNIST and CIFAR10\n\n[1] Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Verification\n[2] PRIMA: Precise and General Neural Network Certification via Multi-Neuron Convex Relaxations", "summary_of_the_review": "This paper combines existing techniques to improve the performance of complete verifiers. The contributions to the bounding process (incorporating the additional constraints with Lagrange multipliers) are relatively minor. The improvements to the branching procedure are interesting but should be clarified further.\nIt is however disappointing that the empirical evaluation has several weaknesses, mainly due to the lack of comparing to strong baselines.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "Not applicable"}, "extra_text": {}}, {"review_id": "cMklKwO3Wl5", "reviewer": "Reviewer_gB2C", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "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": "Strengths:\n\n- Previously multi-neuron relaxations have shown to be instrumental in going beyond smaller networks [1][2]. Combining this in branch-and-bound framework is a novel idea that could potentially lead to interesting future work.\n- Branching decisions are important in a BaB setting [5], the authors present interesting proposals (ACS + CAB) for both effective and efficient branching. Previous branching heuristics make branching decisions on expected bound improvements. Since MN-BaB operates on multi-neuron relaxations, branching heuristic ACS is presented that factors the improvements by multi-neuron relaxations into consideration.  CAB (cost-adjusted branching) postulates that runtime is a key factor in branching decisions for complete verifiers, hence proposing to do the branching decision as a function of expected bound improvement per cost instead of just expected bound improvement.\n- The ablation studies show each system component is beneficial (Figure 3, 4, 5) and contributes to the overall improvements (Figure 6).\n\nWeakness\n- Experimental evaluation of the framework seems non-exhaustive and missing comparisons to important baselines (see more details below), making it hard to place MN-BaB (this paper) alongside the literature. \n\nReg. experimental evaluation:\n\nTable 1: The authors claim that three out of the four networks are well-solved by previous methods and are less relevant, while for the fourth one, they perform the best. I have a few reservations:\n\n- For the first three rows, it seems like MN-BaB isn’t the most effective and efficient method and for the fourth row the margin seems too small to claim “outperformance” -- hence more evaluation or analysis might be needed to better understand the behaviour. \n- A possible remedy to this: Seems like there’s some promise in larger networks. Previous works have also considered ConvSuper [6], networks larger than ConvBig. Did the authors try to evaluate these benchmarks? What were the results?\n- Another remedy for better understanding: Previous works [1][2][6][7][10][11][12] have all considered a larger set of benchmarks including more kinds of conv networks + FFNNs. I already mentioned conv networks above but the method presented seems to work for feed-forward networks (FFNNs) too but no evaluation is presented. Maybe because of space constraints and/or the argument that ERAN can already do very well. But it would be a good idea to have the results in the paper (or appendix) for a more holistic picture. While Beta-CROWN might not work for MLPs but comparisons to other baselines (including other variants of CROWN) would be useful.  \n- Reg. branching for MN-BaB: It’s unclear why three out of the four rows use BaBSR branching and the last one uses ACS. Was only the best performing branching heuristic reported? Since ACS is stated as one of the main contributions of the paper too, it would be good to see a breakdown of ACS vs. BaBSR for at least all these four benchmarks otherwise the MN-BaB results are not generated from a consistent set of options.\n- Fixes needed (at minimum, the difficulty of fix in brackets):\n            * ACS+CAB reporting for all benchmarks. (easy fix)\n            * One larger conv network eval to claim “outperformance”. (medium fix)\n- Fixes needed (ideally)\n            * A couple of FFNNs evaluation for comparison with ERAN/OVAL. (larger change, can reuse numbers from PRIMA paper) \n\n\nTable 2: The authors claim that their methods work on more challenging less regularized networks. This section is important and interesting and highlights how each component of the system contributes to the final results. My primary concern is that this experiment is in isolation and not placed well with the rest of the related works:\n- For ResNet-6-A and ResNet-6-B: Was ERAN run since it can handle ResNets? What were the results? I agree OVAL does not support residual architectures. But other variants of CROWN that do support ResNet architectures and have a public implementation of the same [7][8][9], could have been evaluated (with alpha-beta-CROWN being the current best option). \n- I raise this issue because the paper seems to claim “26% more samples while being around 30% faster” in multiple places but this seems to be on only one network (ResNet-6-A) against only one (weak) baseline for current SOTA (BaBSR). Comparing multiple benchmarks to a few relevant tools (at least one) would be a rigorous way to compute the performance improvements esp. since Table 1 is not shedding a lot of light.\n- Fixes needed (at minimum, the difficulty of fix in brackets):\n           * Report ERAN and a CROWN-variant (alpha-beta-CROWN is open-source, all options here [7][8][9]) in the table (medium change).\n           * Fix the improvement claims to be relative to SOTA (best tool), averaged over all networks instead of just one. (easy change)\n\nA suggestion regarding clarity: Section 2.3 briefly mentions two cases of unstable & stable ReLUs and different convex relaxations. This could be elaborated on some more, particularly on how it is incorporated and affects future decision choices. \n\nMinor comments: Page 5: Enforcing split constraitns → Enforcing split constraints\n\nFinally out of personal curiosity, it seems like the Beta-CROWN results in Table 1. were directly pulled from the paper [10]. Could the authors point me to the table/graph they referred to? Asking as I couldn’t find it myself. \n\n\n- [1] PRIMA: Precise and General Neural Network Certification via Multi-Neuron Convex Relaxations. Müller et. al.\n- [2] Beyond the Single Neuron Convex Barrier for Neural Network Certification. Singh et. al.\n- [3] Branch and Bound for Piecewise Linear Neural Network Verification. Bunel et. al. \n- [4] Scaling the Conve Barrier with Active Sets. De Palma et. al. \n- [5] Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition. De Palma et.al.\n- [6] An Abstract Domain for Certifying Neural Networks. Singh et.al. \n- [7] alpha-beta-CROWN: https://github.com/huanzhang12/alpha-beta-CROWN \n- [8] auto_LiRPA: https://github.com/KaidiXu/auto_LiRPA \n- [9] CROWN-IBP: https://github.com/huanzhang12/CROWN-IBP\n- [10] Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Verification. Wang et.al.\n- [11] Automatic perturbation analysis for scalable certified robustness and beyond. Xu et.al.\n- [12] Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers. Xu et.al.\n", "summary_of_the_paper": "The paper presents a novel framework for neural network verification by combining two popular paradigms in literature: tight multi-neuron relaxations [1][2] and branch-and-bound [3][4][5]. The benefit of such a framework is combing the best of both paradigms by improving the bounding method (multi-neuron relaxations) in a Branch-and-Bound framework resulting in scalability and completeness. Additionally, the authors also present a branching heuristic that can leverage their multi-neuron setup and propose a computation cost-adjusted branching to obtain decreased runtimes. They validate their hypothesis by comparing it to state-of-the-art verification tools and verifying established convolution network benchmarks for MNIST & CIFAR-10. They also present ablation studies for various features on two larger ResNet architectures showing how each system component contributes to improved results. \n", "summary_of_the_review": "In conclusion, I feel the paper presents an interesting idea but needs a more thorough evaluation and comparisons to related works to justify the claims made. Hence,  the current submission is marginally below the acceptance threshold for ICLR.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "2: Several of the paper’s claims are incorrect or not well-supported.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "ZcEIqUk0Kih", "reviewer": "Reviewer_Ns4C", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "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": "The method proposed  comprises (i) the integration of  multi-neuron relaxation\nconstraints  into a  bound propagation algorithm; (ii) the integration of ReLU\nsplit constraints in said algorithm; (iii) the active constraint score and\ncost-adjusted branching heuristics. Part (i) was previously developed and used\nin a bound propagation-based tool (Eran). Part (ii) was previously developed\nand used in a similar framework to the one in present paper (Wang et al.,\n2021).  Therefore the novel contribution of the paper are the branching\nheuristics.  These are however straightforward thereby (in my view) not\nmeriting an ICLR publication from a technical point of view.\n\nConcerning the empirical evaluation, the paper carries out extensive ablation\nstudies whereby the effectiveness of the different constrains and heuristics\nused is shown. It is definitely nice to see that these work in the context of\nbranch-and-bound. The comparison with related work is in my view weak however.\nFirst, out of the four networks used, the present method marginally wins only\nin two them in terms of average runtime and marginally wins only in one of them\nin terms of verified accuracy. Whilst the authors claim that the efficacy of\ntheir method is better observed in bigger networks, they do not include\ncomparisons with related tools on bigger networks. I think that the inclusion\nof these in future revisions of the paper would significantly strengthen the\nevaluation section.\n\nOverall the paper is very well written; it was a joy to read. Some minor\ncomments:\n\n- I did not find clear how the number of floating-point operations in the\n  computation of the bounds is calculated in the cost-adjusted branching\n  heuristic. In particular, how does this vary with different splits?\n\n- Page 2. greater 0 -> greater than 0.\nkkk", "summary_of_the_paper": "The paper puts forward a method for the formal verification of ReLU-based\nneural networks. The method incorporates  previously developed multi-neuron\nrelaxation and split constraints in a bound propagation algorithm which is used\nin a branch-and-bound procedure. Experimental results are reported that compare\nthe procedure with related methods on a number of  MNIST and CIFAR10 models.\nAblation studies are also carried out on ResNet6-A and ResNet6-B.", "summary_of_the_review": "Whilst the paper introduces some novel branching heuristics for the complete\nverification of ReLU neural networks via branch-and-bound, the overall\ncontribution lacks in my opinion the sufficient novelty to merit an ICLR\npublication. I think that  the authors should include additional empirical\ncomparisons with related tools on bigger networks and consider submitting a\ntool paper in a top venue.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "DzD773BuMM", "reviewer": "Reviewer_WZm2", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "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": "In general I like the directions that this paper is taking to push the state-of-the-art of neural network verification. The contributions are novel to my knowledge. The encoding of the verification problem using Lagrange multipliers looks sound. The two ideas on branching heuristics are also interesting. After reading the previous sections, I expect the experimental evaluation to demonstrate two points: \n1) the GPU-based dual algorithm is better than an (almost equivalent) MILP-encoding;\n2) ACS and CAB are competitive with SOTA branching heuristics. \n\nThe experiment on ResNets suggest does seem to show that CAB is beneficial for both BABSR and ACS.  However, I'm not fully convinced of the efficacy of the rest of the proposed techniques. My concerns and questions are listed below:\n1. In Table 1, why does MB-BAB use different branching heuristics for different networks? Maybe show the numbers of BABSR+CAB and ACS+CAB in two different columns? \n2. Table 1 suggests that ERAN (PRIMA + MILP-encoding) solves the most instances overall, while being slower on only 1 network. To draw the conclusion that Gurobi (with 16 cpus) is less scalable than a GPU-based procedure on the verification problem (which is the motivation of the proposed encoding of the verification problem), more experiments are needed than a single perturbation bound and a single network.\n3. In Table 2, why is \"DeepPoly only\" instead of \"PRIMA only\" (or kReLU only) used as a filter for easy verification problem.\n4. What are the number of ReLUs in the ResNet architecture and in the ConvBig/Small networks? I saw the concrete architectures in the Appendix but since the motivation for excluding ERAN from Table 2 is the claim that MILP-encoding is less scalable than the GPU-based approach on larger models, the architecture information (or at least the number of ReLUs) seems to be relevant enough to be put in the main paper.\n5. There are more recent branching heuristics than BABSR as mentioned in the related work. It would strengthen the paper to use one of those (e.g., FSB) as the baseline.\n\nOverall, while I find the proposed techniques promising, a more thorough evaluation is needed to show their benefits.\n\nMinor comments:\n- Typo: page 5: Enforcing split constraitns\n- Figures 5, 6 are compressed in a way that favors the proposed techniques. Maybe present it with the same width and height?", "summary_of_the_paper": "The paper introduces a complete verification procedure that 1) encodes PRIMA constraints as a Lagrangian function, which admits GPU-based algorithm; 2) uses the values of the Lagrange parameter to guide the branching (ACS); and 3) regularizes the branching score with the estimated cost for a split.", "summary_of_the_review": "Promising verification procedure, but a more thorough evaluation is needed.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "2: Several of the paper’s claims are incorrect or not well-supported.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "26zE3FmfV98", "reviewer": "Reviewer_qGFq", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "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": "The paper is clearly written, with a clean, linear presentation of the method and its derivation. The \"novelty\" of the work is somewhat incremental, but the new methods show their efficacy, and the paper is a worthy contribution to the literature.\n\n* I wish that the authors spent more time describing the work of Muller et al that they build on for the multi-neuron constraint generation. Consider adding a brief discussion.\n* p2: To what extent is your framework \"applicable\" to network with Sigmoid and Tanh activations? If it involves approximating the nonlinear activations, is it still sound and exact?\n* p2: I think you need to add a \"sound\" to \"A method is called complete if...\"?\n* p3: \"we derive linear upper and lower bounds of the form z^i >= Az^(i-1) + c for each...\". This seems like it's only lower bounds?\n* p6: Is \"noisy proxies\" the right choice of words?\n* p8: Is there a fundamental reason beta-Crown and Oval don't support ResNet, or is it simply a matter of implementation? What about ERAN?\n* The authors mention a \"GPU-based dual optimizer\" in the abstract and introduction, but there is no explicit mention of GPU compatibility of the method in the body of the paper. Can the authors clarify?", "summary_of_the_paper": "This paper presents a branch-and-bound algorithm for neural network verification that uses a dualized variant of an existing approach for generating multi-neuron relaxations. Computational results are presented showcasing the quality of the verification bounds, and the scalability of the method.", "summary_of_the_review": "The paper presents its new idea cleanly, and the improvements appear substantial enough for publication.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}]

Author rebuttal:

Meta-review: The authors improve upon existing algorithms for complete neural network verification by combining recent advances in bounding algorithms (better bounding algorithms under branching constraints and relaxations involving multiple neurons) and developing novel branching heuristics. They show the efficacy of their method on a number of rigorous experiments, outperforming SOTA solvers for neural network verification on several benchmark datasets.

All reviewers agree that the paper makes valuable contributions and minor concerns were addressed adequately during the rebuttal phase. Hence I recommend that the paper be accepted.
Decision: Accept (Poster)