Year: 2021

Abstract:
State-of-the-art neural network verifiers are fundamentally based on one of two paradigms: encoding the whole problem via tight multi-neuron convex relaxations or applying a Branch-and-Bound (BaB) procedure which leverages imprecise but fast bounds on a large number of easier subproblems. The former can better capture complex multi-neuron dependencies but sacrifices completeness due to inherent precision limits of convex relaxations. The latter enables complete verification yet 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 and an efficient, GPU-based dual optimizer to drastically reduce the number of subproblems generated during the BaB process. An extensive evaluation demonstrates that our verifier achieves new state-of-the-art results 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.

heading: 1 INTRODUCTION
text: Recent years have witnessed substantial interest in new methods for certifying properties of neural networks, ranging from stochastic methods (Cohen et al., 2019) which construct a robust model from an underlying classifier to deterministic methods (Gehr et al., 2018; Katz et al., 2017; Xu et al., 2020a) that analyze a given network as is (the focus of our work).
Key challenge: Scalable and Precise Non-Linearity Handling Deterministic verification methods can be categorized as complete or incomplete. Recent incomplete verification methods based on propagating and refining a single convex region (Müller et al., 2021; Dathathri et al., 2020; Tjandraatmadja et al., 2020) are limited in precision due to fundamental constraints imposed by convex relaxations. Traditional complete verification approaches based on SMT solvers (Ehlers, 2017) or a single mixed-integer linear programming encoding of a property (Tjeng et al., 2017; 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 promising recent formulation in the form of a Branch-and-Bound approach (Bunel et al., 2020) has been popularized, yielding anytime-valid bounds, by recursively splitting the problem domain into easier subproblems and deriving bounds on each of these via cheap and less precise methods (Xu et al., 2020b; Wang et al., 2021; Palma et al., 2021; Henriksen & Lomuscio, 2021). This approach has proven effective on (smaller) networks where there are relatively few unstable activations and where splitting can yield substantial improvements. 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 make individual splits less effective (exacerbated by the relatively loose underlying bounding methods).
This work: Branch-and-Bound guided by Multi-Neuron Constraints In this work, we propose a new certification method and verifier, called Multi-Neuron Constraint Guided BaB (MN-BAB), which aims to combine the best of both worlds: it builds on the tight multi-neuron constraints proposed by Müller et al. (2021) and leverages these constraints within a BaB framework to yield an efficient, GPU based dual solver. The key benefit here lies in the fact that exploiting 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 benefit 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 <ANONYMIZED>.
Main Contributions:
• We present a novel verification framework, MN-BAB, which leverages tight multi-neuron constraints and a GPU-based dual solver in a BaB approach.
• We develop a novel branching heuristic based on information obtained from analyzing our multi-neuron constraints.
• We propose a new class of branching heuristics, applicable to all BaB-based verifiers, that correct the expected bound improvement of a 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 as much as 28% on challenging networks.

heading: 2 BACKGROUND
text: In this section, we review the necessary background underlying our method (discussed next).

heading: 2.1 NEURAL NETWORK VERIFICATION
text: The neural network verification problem can be defined as follows: given an input domainD ⊆ X , a network f : X → Y , and a linear property P ⊆ Y over the output neurons y ∈ Y , prove f(x) ∈ P, ∀x ∈ D. We instantiate this problem with the challenging `∞-norm bounded specifications and set D to the `∞ ball around an input point x0 of radius : D (x0) = {x | ||x− x0||∞ ≤ }. For ease of presentation, we consider neural networks of L fully connected layers with ReLU activation functions (we note that MN-BAB can handle a wide range of layers including convolutional, residual, batch-normalization, average-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 ReLU, Sigmoid, Tanh, MaxPool, and others. We denote the number of neurons in the ith layer as di and the corresponding weights and biases asW (i) ∈ Rdi×di−1 and b(i) ∈ Rdi for i ∈ {1, ..., L}. Further, the neural network is defined as f(x) := ẑ(L)(x) where ẑ(i)(x) :=W (i)z(i−1)(x) + b(i) and z(i)(x) := max(0, ẑ(i)(x)). For readability, the notation omits the dependency of intermediate activations on x.
Since we can encode any linear property over output neurons into an additional affine layer, we can simplify the general formulation f(x) ∈ P to f(x) > 0. The property can now be verified by proving that a lower bound is greater 0 via the following optimization problem:
min x∈D (x0)
f(x) = ẑ(L)
s.t. ẑ(i) =W (i)z(i−1) + b(i)
z(i) = max(0, ẑ(i))
(1)
A 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).

heading: 2.2 BRANCH-AND-BOUND FOR VERIFICATION
text: Bunel et al. (2020) successfully applied the Branch-and-Bound (BaB) approach (Land & Doig, 1960) to neural network verification. It consists of a bounding method that computes sound upper and lower bounds on the optimization objective of Eq. (1) and a branching method that recursively splits the problem into subproblems with added constraints, allowing for increasingly tighter bounds. If an upper bound < 0 is found, this represents an adversarial example and allows to terminate the procedure. If the obtained lower bound is> 0, the property is verified on the corresponding domain. If a lower bound > 0 is derived on all splits, the property is verified. An ideal splitting procedure
minimizes the total time required for bounding, which is often well approximated by the number of considered subproblems. A simple approach is to split the input domain, however, this is inefficient for high-dimensional input spaces. Splitting a ReLU activation node into its positive and negative phases has been shown to be far more efficient (Bunel et al., 2020) and ultimately yields a complete verifier (Wang et al., 2021). Hence, we focus solely on ReLU branching strategies.
2.3 LINEAR CONSTRAINTS
The key challenge in neural network verification Eq. (1) are the non-linear activations. Stable ReLUs, i.e., those which we can show to be always active (ẑ ≥ 0) or inactive (ẑ ≤ 0), can be replaced by a linear function. Unstable ReLUs, i.e. those that can be either active or inactive depending on the exact x ∈ D, have to be approximated using a convex relaxation of their´ input-output-set. We build on the convex relaxation introduced in DEEPPOLY (Singh et al., 2019b) and shown in Fig. 1. Its key property is the single linear upper and lower bound, which allows for efficient bound computation.
2.4 MULTI-NEURON CONSTRAINTS
All convex relaxations that consider ReLU neurons individually are fundamentally limited in their precision by the so-called (single-neuron) convex relaxation barrier (Salman et al., 2019). It can be overcome by considering multiple neurons jointly (Singh et al., 2019a; Tjandraatmadja et al., 2020; Müller et al., 2021; Palma et al., 2021) capturing interactions between these neurons to obtain tighter bounds, illustrated in Fig. 2. We leverage the multi-neuron constraints from Müller et al. (2021), expressed as a conjunction of linear constraints over the joint input and output space of a ReLU layer.

heading: 2.5 CONSTRAINED OPTIMIZATION VIA LAGRANGE MULTIPLIERS
text: To incorporate constraints into an optimization problem we use the technique of Lagrange multipliers. Given a constrained minimization problem minx f(x), s.t. g(x) ≤ 0, we can bound the objective function with:
min x f(x) ≥ min x max λ≥0 f(x) + λg(x)
If the constraint is satisfied strictly, i.e., g(x) < 0, we set λ = 0 to maximize the objective, else, i.e., g(x) ≥ 0, increasing λ would allow the objective to grow unboundedly, shifting the minimum over x until the constraint is satisfied. Hence, if λ > 0 after optimization, the constraint is active, i.e., it is actively enforced and currently satisfied with equality.

heading: 3 A MULTI-NEURON RELAXATION BASED BAB FRAMEWORK
text: In this section, we describe the two key components of MN-BAB: (i) an efficient bounding method leveraging multi-neuron constraints, and (ii) a branching method tailored to it.

heading: 3.1 EFFICIENT MULTI-NEURON BOUNDING
text: We build on the approach of Singh et al. (2019b), extended by Wang et al. (2021) of deriving a lower bound f as a function of the network inputs and a set of optimizable parameters. Crucially, we tighten these relatively loose bounds significantly by enforcing precise multi-neuron constraints via Lagrange multipliers. To enable this, we develop a method capable of integrating any linear constraint over arbitrary neurons anywhere in the network into the bounding objective. At a high
level, we derive linear upper and lower bounds of the form z(i) ≥ Az(i−1) + c for every layer’s output in terms of its inputs z(i−1). Then, starting with a linear expression in the last layer’s outputs z(L) that we aim to bound, we use the linear bounds derived above, to replace z(L) with symbolic bounds depending only on the previous layer’s values z(L−1). We proceed in this manner recursively, until we obtain an expression in terms of only the networks inputs. Below we describe this backsubstitution for ReLU and affine layers.
Affine Layer Assume any affine layer ẑ(i) = W(i)z(i−1)+b(i) and a lower bound f = â(i)ẑ(i)+ ĉ(i) with respect to its outputs. We then substitute the affine expression for ẑ(i) to obtain:
f = â(i)W(i)︸ ︷︷ ︸ a(i−1) z(i−1) + â(i)b(i) + ĉ(i)︸ ︷︷ ︸ c(i−1) = a(i−1)z(i−1) + c(i−1) (2)
ReLU Layer Let f = a(i)z(i) + c(i) be a lower bound with respect to the output of a ReLU layer z(i) = max(0, ẑ(i)) and l(i) and u(i) bounds on its input s.t. l(i) ≤ ẑ(i) ≤ u(i), obtained by recursively applying the bounding procedure or using a cheaper but less precise propagationbased bounding method (Singh et al., 2018; Gowal et al., 2018). The backsubstitution through a ReLU layer now consists of three distinct steps: 1) enforcing multi-neuron constraints, 2) enforcing neuron-wise relaxations, and 3) enforcing split constraints, which we describe in detail below.
Enforcing multi-neuron constraints We compute multi-neuron constraints as described in Müller et al. (2021), although our approach is applicable to any linear constraints in the input-output space of ReLU activations, written as: [
P (i) P̂ (i) −p(i) ] z(i)ẑ(i)
1  ≤ 0. (3) where ẑ(i) are the pre- and z(i) the post-activation values and P (i), P̂ (i), and −p(i) the constraint parameters. We enforce these constraints using Lagrange multipliers (see §2.5), yielding sound lower bounds for all γ ∈ (R≥0)ei , where ei denotes the number of multi-neuron constraints in layer i.
a(i)z(i) + c(i) ≥ max γ(i)≥0 a(i)z(i) + c(i) + γ(i)>(P (i)z(i) + P̂ (i)ẑ(i) +−pi)
= max γ(i)≥0 (a(i) + γ(i)>P (i))︸ ︷︷ ︸ a′(i) z(i) + γ(i)>P̂ (i)ẑ(i) + γ(i)>(−pi) + c(i)︸ ︷︷ ︸ c′(i)
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 α collected inD (see below):
max γ(i)≥0 a′(i)z(i) + c′(i) ≥ max 0≤α(i)≤1 γ(i)≥0 a′(i)(D(i)ẑ(i) + b(i)) + c′(i)
= max 0≤α(i)≤1 γ(i)≥0 a′(i)D(i)︸ ︷︷ ︸ a′′(i) ẑ(i) + a′(i)b(i) + c′(i)︸ ︷︷ ︸ c′′(i)
The intercept vector b and the diagonal slope matrixD are defined as:
Dj,j =  1 if lj ≥ 0 or node j is positively split 0 if uj ≤ 0 or node j is negatively split αj if lj < 0 < uj and aj ≥ 0 uj
uj−uj if lj < 0 < uj and aj < 0
bj = { − uj ljuj−lj if lj < 0 < uj and aj < 0 0 otherwise
Where we drop the layer index i for readability and αj is the lower bound slope parameter illustrated in Fig. 1. Note how, depending on whether the sensitivity a(i)j of f w.r.t. z (i) j has positive or negative sign, we substitute z(i)j for its lower or upper bound, respectively.
Enforcing split constraints We encode split constraints of the form ẑ(i)j ≥ 0 or ẑ (i) j ≤ 0 using the diagonal split matrix S as follows, again dropping the layer index i:
Sj,j =  −1 positive split: ẑj ≥ 0 1 negative split: ẑj < 0 0 no split
S(i)ẑ(i) ≤ 0
We again enforce these constraints using Lagrange multipliers:
max 0≤α(i)≤1 γ(i)≥0 a′′(i)ẑ(i) + c′′(i) ≥ max 0≤α(i)≤1 β(i)≥0 γ(i)≥0 (a′′(i) + β(i)>S(i))︸ ︷︷ ︸ a′′′(i) ẑ(i) + c′′(i)︸︷︷︸ c′′′(i)
Putting everything together, the backsubstitution operation through a ReLU layer is:
min x∈D a(i)z(i) + c(i) ≥ min x∈D max 0≤α(i)≤1 β(i)≥0 γ(i)≥0 ((a(i) + γ(i)>P (i))D(i) + β(i)>S(i) + γ(i)>P̂ (i))︸ ︷︷ ︸ â(i) ẑ(i)
+ (a(i) + γ(i)>P (i))′b(i) + γ(i)>-p(i) + c(i)︸ ︷︷ ︸ ĉ(i)
(4)
Full backsubstitution through all layers leads to an optimizable lower bound on f :
min x∈D f(x) ≥ min x∈D max 0≤α≤1 0≤β 0≤γ a(0)x+ c(0) ≥ max 0≤α≤1 0≤β 0≤γ min x∈D a(0)x+ c(0)
where the second inequality holds due to weak duality. We denote all α(i)j from every layer of the backsubstitution process with α and define β and γ analogously. The inner minimization over x has a closed form solution if D is an lp-ball of radius around x0, given by Hölder’s inequality:
max 0≤α≤1 0≤β 0≤γ min x∈D a(0)x+ c(0) ≥ max 0≤α≤1 0≤β 0≤γ a(0)x0 − ||a(0)>||q + c(0) (5)
where q is defined s.t. 1p + 1 q = 1. Since these bounds are sound for any 0 ≤ α ≤ 1, and β,γ ≥ 0, they can be tightened by using (projected) gradient ascent to optimize these parameters.
We compute all intermediate bounds using the same bounding procedure, leading to two full parameter 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 an upper bound on the minimum optimization objective precluding verification (f < 0) allows us to terminate the BaB process early. Propagating any input x ∈ D through the network yields a valid upper bound, hence, we propose to use the input that minimizes Eq. (5):
xi =
{ (x0)i + if a (0) i < 0
(x0)i − if a(0)i ≥ 0 .

heading: 3.2 MULTI-NEURON CONSTRAINT GUIDED BRANCHING
text: The general 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 choosing splits that minimize the number of required subproblems a key component of any BaB framework (Bunel et al., 2020). Typically, a score is assigned based on the expected bound improvement and the most promising split is chosen. Consequently, the better the actual bound improvement is captured, the better the resulting decision. Both the commonly used BABSR Bunel et al. (2020) and the more recent FSB De Palma et al. (2021) approximate improvements under a DEEPPOLY style backsubstitution procedure. As neither considers the impact of multi-neuron constraints at all, the scores they compute might not be suitable proxies for the bound improvements obtained with our method. To overcome this issue, we propose a novel branching heuristic, Active Constraint Score Branching (ACS), tailored to the multi-neuron constraints. Further, we introduce a branching heuristic framework which corrects the expected bound improvement with the potentially significantly varying expected computational cost.
Active Constraint Score Branching The value of a Lagrange parameter γ provides valuable information about the constraint it enforces. Concretely, γ > 0 indicates that a constraint is active, i.e., the optimal solution fulfills it with equality. Further, for a constraint g(x) ≤ 0, a larger ∂xγg(x) indicates a 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 γ>P and γ>P̂ , respectively, where P and P̂ are the multi-neuron constraint parameters. We then define our branching score for a neuron j in layer i as the sum over all sensitivities with respect to its input or output:
si,j = |γ(i)>P (i)|j + |γ(i)>P̂ (i)|j , (6) Intuitively, stabilizing 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 an additional backsubstitution pass.
Cost Adjusted Branching Any complete method will decide every property eventually. Hence its runtime is a key performance metric. Existing branching heuristics ignore this aspect and only consider the expected improvement in bound-tightness, but not the sometimes considerable differences 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 improvement 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 a 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-point operations required to compute the new bounds, refer to App. B for a more detailed description. However, any approximation of the expected cost can be used to instantiate CAB.
Enforcing splits Once the ReLU to split on has been determined, two subproblems are generated. One where a non-negative ẑ ≥ 0 and one where non-positive ẑ ≤ 0 pre-activation value have to be enforced. This is 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. ´

heading: 3.3 SOUNDNESS AND COMPLETENESS
text: 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. However, to actually obtain exact bounds all split constraints have to be enforced, requiring an optimal choice of β. This can be obtained as the fully split problem is convex and can hence be solved efficiently (Wang et al., 2021). Therefore, a property holds iff the exact bounds thus obtained are positive on all subproblems. We conclude that MN-BAB is a complete verifier.

heading: 4 EXPERIMENTAL EVALUATION
text: We now present an extensive evaluation of our method. First, and perhaps surprisingly, we find that existing MILP based verification tools (Singh et al., 2019c; Müller et al., 2021) are more effective in verifying robustness on many established benchmark networks than what is considered state-of-theart. This highlights that next-generation verifiers should focus on and be benchmarked using less regularized and more accurate networks. We take a step in this direction 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 a GPU based version of MN-BAB in PyTorch (Paszke et al., 2019). We 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 a wide range of networks (see Table 3 in App. A) on the MNIST (Deng, 2012) and CIFAR10 datasets (Krizhevsky et al., 2009). To this end, we also consider three new residual networks, ResNet6-A, ResNet6-B, and ResNet8-A. ResNet6-A and ResNet6-B have the same architecture but differ in regularization strength while ResNet8-A has an additional residual block. All three were trained with adversarial training (Madry et al., 2017) using PGD, the GAMA loss (Sriramanan et al., 2020) and MixUp data augmentation (Zhang et al., 2021). ResNet6-A and ResNet8-A were trained using 8-steps and = 4/255, whereas 20-steps and = 8/255 were used for ResNet6-B.We compare against β-CROWN (Wang et al., 2021), a BaB based state-of-the-art complete verifier, OVAL (Palma et al., 2021; De Palma et al., 2021; Bunel et al., 2020), a BaB framework based on a different class of multi-neuron constraints, and ERAN Singh et al. (2019c); Müller et al. (2021) 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 1, we compare the verified accuracy and runtime of MN-BAB with that of state-of-the-art tools ERAN, β-CROWN, and OVAL. Perhaps surprisingly, we find that both MNIST and the smallest CIFAR10 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, 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 runtime. On ConvSuper we were not able to find configurations for OVAL and β-CROWN that did not run out of memory. Comparing the BaB methods, we observe an overall trend that more precise but also expensive underlying bounding methods are most effective on larger networks, where additional splits are less efficient, and complex inter-neuron interactions can be captured by the precise multi-neuron constraints. On these networks, the more complex interactions also lead to more active MNCs and hence more informative ACS scores.
0.0 0.5 1.0 Quantile
100
101
102
103 Subproblem count ratio
mean
mean
ResNet6-A ResNet6-B
Figure 4: Ratio of subproblem required per property with BABSR and ACS.
Ablation Study To analyze the individual components of MN-BaB, we consider the weakly and heavily regularized ResNet6-A and ResNet6-B, respectively, with identical architecture. Concretely, we show the effect different bounding procedures and branching approaches have in the two settings in Table 2. As verified accuracy and mean runtime are very coarse performance metrics, we also analyze the ratio of runtimes and number of subproblems required for verification on a per-property level, filtering out those where both methods verify before any branching occurred (Figs. 3–5). Overall, we observe that the number of visited subproblems required for certification 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 an additional speed up of around 50%.
The trend of MN-BAB succeeding on more challenging networks is confirmed here. Leveraging Multi-Neuron Constraints (MNCs) enables us to verify 20% more samples while being around 22% faster (see Table 2) on ResNet6-A while on the more heavily regularized ResNet6-B we only verify 6% more samples. When analyzing on a per-property level, shown in Fig. 6, the trend is even more pronounced. For easy problems leveraging MNCs and ACS has little impact (points in the lower left-hand corner) however, 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).
Effectiveness of Multi-Neuron Constraints In Fig. 3, we show the ratio between the number of subproblems required to prove the same lower bound on the final objective (either 0, if both methods certify, or smaller of the two lower bounds at termination) 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 2).
Effectiveness of ACS Branching In Fig. 4, we show the ratio between the number of subproblems 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 on ResNet6-A and
ResNet6-B, respectively, leading to an additional reduction by between one and two orders of magnitude and showing the effectiveness of our novel ACS branching heuristic. Average verification times are reduced by 12% and 21% on ResNet6-A and ResNet6-B, respectively. Note that the relatively 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.
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.

heading: 5 RELATED WORK
text: Neural Network Verification Beyond the Single Neuron Convex Barrier After the so-called (Single Neuron) Convex Barrier has been described for incomplete relaxation-based methods by Salman et al. (2019), a range of approaches has been proposed that consider multiple neurons jointly to obtain tighter relaxations. Singh et al. (2019a); Müller et al. (2021) 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 at a time. While the two approaches are theoretically incomparable, the former yields empirically better results (Müller et al., 2021).
Early complete verification methods relied on off-the-shelf SMT (Katz et al., 2017; Ehlers, 2017) or MILP solvers (Dutta et al., 2018; Tjeng et al., 2017). 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 can show robustness. Since then, a range of partially (Xu et al., 2020b) or fully GPU-based (Wang et al., 2021; Palma et al., 2021) 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 to branch on next. Full strong branching (Applegate et al., 1995) exhaustively evaluates this for all possible branching decisions. However, this is intractable for all but the smallest networks. Lu & Kumar (2019) train a GNN to imitate the behavior of full strong branching at a fraction of the cost, but transferability remains an open question and collecting training data to imitate is extremely costly. Bunel et al. (2020) proposed an efficiently computable heuristic score, locally approximating the bound improvement of a branching decision using the method of Wong & Kolter (2018). Henriksen & Lomuscio (2021) 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. (2021) introduced filtered-smart-branching (FSB), using BaBSR to selected branching candidates and then computing a more accurate heuristic score only for the selected candidates. Instead of targeting the largest bound improvement, Kouvaros & Lomuscio (2021) aim to minimize the number of unstable neurons by splitting the ReLU node with the most other ReLU nodes depending on it.

heading: 6 CONCLUSION
text: We propose the complete neural network verifier MN-BAB. Building on the Branch-and-Bound methodology, MN-BAB leverages tight multi-neuron constraints, a novel branching heuristic and an efficient dual solver able to utilize massively parallel hardware accelerators to enable the verification of particularly challenging networks. Our thorough empirical evaluation shows how MN-BAB is particularly effective in verifying challenging networks with high natural accuracy and practical relevance, reaching a new state-of-the-art in several settings.

heading: 7 ETHICS STATEMENT
text: Most machine learning based systems can be both employed with ethical as well as malicious purposes. Methods such as ours that enable the certification of robustness properties of neural networks are a step towards more safe and trustworthy AI systems and can hence amplify any such usage. Further, malicious actors might aim to convince regulators that the proposed approach is sufficient to show robustness to perturbations encountered during real world application, which could lead to insufficient regulation in safety critical domains.

heading: 8 REPRODUCIBILITY STATEMENT
text: We will make all code and trained networks required to 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 in Section 4 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.

heading: A EXPERIMENT DETAILS
text: 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. (2021) facilitate comparability.
Since we keep intermediate bounds of neurons before the split layer fixed, as described in Section 3.2, the memory requirements for splitting at different layers can 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 a strong adversarial attack with the following parameters before attempting certification: We apply two targeted version (towards all classes) of PGD (Madry et al., 2017) using margin loss (Gowal et al., 2018) and GAMA loss (Sriramanan et al., 2020), both with 5 restarts, 50 steps, and 10 step output diversification (Tashiro et al., 2020).
A.1 ARCHITECTURES
In this section, we provide an overview over all the architectures evaluated in Section 4. The architecture of the convolutional networks for MNIST and CIFAR10 are detailed in Table 4. And the architecture of both ResNet6-A and ResNet6-B is given in Table 5

heading: B SPLIT-COST COMPUTATION FOR CAB
text: Recall that for CAB, we normalize the branching score obtained with an arbitrary branching heuristic with the (approximate) cost of 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 considering the former component.
We approximate this direct cost by the number of floating-point operations required to compute the new bounds. This is computed as the sum of floating-point operations required for bounding all intermediate bounds that are recomputed. Our bounding approach only enforces constraints
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 backsubstitution is just a 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 k of an L layer network and the cost of backsubstituion from layer i is Ci and the number of nodes is di, the final cost of the split is:
L∑ i=k+1 2diCi
Where the factor 2 comes from the fact that for intermediate bounds we need to recompute both lower and upper bounds. The cost Ci of a full backsubstitution from layer i can be computed as the sum over the cost of backsubstituting through all preceding layers Ci = ∑i−1 j=0 cj , where the cost for a single layer can be computed as follows:
• ReLU layer: cj = dj + pj , where pj is the number of prima constraints. • Linear layer: cj = #Wj , where #Wj is the number of elements in the weight matrix.
• Conv layer: cj = djk2j , where kj is the kernel size.

Review summaries:
The paper puts forward a method for the formal verification of ReLU-based neural networks. The method incorporates  previously developed multi-neuron relaxation and split constraints in a bound propagation algorithm which is used in a branch-and-bound procedure. Experimental results are reported that compare the procedure with related methods on a number of  MNIST and CIFAR10 models. Ablation studies are also carried out on ResNet6-A and ResNet6-B.

This paper deals with complete verification of neural network, based on a branch and bound framework.  It is essentially a combination of two recent papers: - 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. - 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.  The 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.  In addition to that, the paper also propose new branching heuristics: - Active Constraint Score Branching, which uses the lagrangian variables associated with the constraints of the multi-neuron relaxation to prioritize branching. - 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.  Experiments are ran on MNIST and CIFAR10  [1] Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Verification [2] PRIMA: Precise and General Neural Network Certification via Multi-Neuron Convex Relaxations

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.