Source-linked AI summary
Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound
Claudio Ferrari, Mark Niklas Muller, Nikola Jovanovic, Martin Vechev
TL;DR
Neural-network verification must combine precise multi-neuron relaxations with complete methods that remain effective on challenging networks. MN-BAB integrates multi-neuron constraints into BaB and uses a GPU-based dual optimizer. The evaluation reports new state-of-the-art results, including up to 28% certified-accuracy gains on challenging networks.
Problem
Multi-neuron convex relaxations are limited by completeness, while BaB with fast but imprecise bounds becomes less effective on larger, more challenging networks.
Source: §1 · p. 1Method
MN-BAB combines tight multi-neuron constraints with BaB and an efficient GPU-based dual method to reduce the number of subproblems.
Source: §1 · pp. 1–2Results
Takeaways & Limitations
MN-BAB is particularly effective on challenging networks with high natural accuracy and practical relevance.
Source: §6 · p. 9For exposition, the paper focuses on fully connected ReLU networks, although MN-BAB handles several other layer types and its approach applies to a wider range of activations.
Source: §2.1 · p. 2
Abstract
from arXiv · showhide
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.
1 INTRODUCTION
Deterministic verification must balance the precision of multi-neuron convex relaxations against the completeness of Branch-and-Bound (BaB), whose splits become less effective on larger, less regularized networks. MN-BAB combines multi-neuron constraints, BaB, and a GPU-based dual method, with branching heuristics designed to reduce verification work.
1 INTRODUCTION
- The work focuses on deterministic analysis of a given network, distinct from stochastic approaches that construct a robust model from a base classifier.Deterministic approaches are described as either complete or incomplete.Source: §1 · p. 1
- Multi-neuron convex relaxations capture neuron dependencies but are limited in precision, while BaB is complete yet becomes less effective as unstable activations make splits less useful.Traditional complete SMT and MILP approaches also face worst-case exponential complexity and may not compute sound bounds in reasonable time.Source: §1 · p. 1
- MN-BAB combines tight multi-neuron constraints with BaB and an efficient GPU-based dual method.The framework uses multi-neuron constraints proposed by Müller et al. (2022).Source: §1 · p. 1
- More precise bounds substantially reduce the number of costly domain splits, especially on larger, less regularized networks where extra splits yield diminishing returns.The work also introduces ACS, informed by multi-neuron constraints, and CAB, which accounts for the expected computational cost of a branching decision.Source: §1 · p. 2
- Up to 28% certified-accuracy gains on challenging networks are reported, alongside new branching heuristics and a GPU-based dual solver.The proposed heuristics include ACS, based on multi-neuron constraints, and CAB, which adjusts expected bound improvement for computational cost.Source: §1 · p. 2
2 BACKGROUND
The background defines the verification objective and the ReLU-network setting, then reviews BaB and convex relaxations for bounding that objective. It also introduces multi-neuron constraints and Lagrange multipliers as tools used by the method.
2.1 NEURAL NETWORK VERIFICATION
- Verification asks whether a network maps every input in a region to an output satisfying a linear property; the setup uses an ℓ∞-bounded region and ReLU networks.For exposition, the network is written with fully connected layers, though the method can handle convolutional, residual, batch-normalization, and average-pooling layers.Source: §2.1 · p. 2
- A linear output property can be encoded as an additional affine layer, reducing verification to proving a lower bound greater than zero; soundness excludes false positives, while completeness excludes false negatives.The text focuses on ReLU networks because BaB yields complete verifiers only for piecewise linear activations.Source: §2.1 · p. 2
2.2 BRANCH-AND-BOUND FOR VERIFICATION
- BaB alternates sound bounding with recursive domain splits, using a negative upper bound to find a counterexample and positive lower bounds to verify subdomains.A property is verified once every subdomain has a positive lower bound; ReLU phase splits are more efficient than splitting the high-dimensional input domain.Source: §2.2 · pp. 2–3
2.3 LINEAR CONSTRAINTS
- Stable ReLUs can be replaced by linear functions, while unstable ReLUs are approximated with a convex relaxation using single linear upper and lower bounds.The DEEPPOLY relaxation is illustrated for neuron-wise input bounds and a parameterized slope.Source: §2.3 · p. 3, Figure 1 · p. 3
2.4 MULTI-NEURON CONSTRAINTS
- Joint constraints over multiple ReLUs overcome the precision limit of neuron-wise convex relaxations by capturing interactions and tightening bounds.MN-BAB uses the multi-neuron constraints of Müller et al. (2022).Source: §2.4 · p. 3, Figure 2 · p. 3
2.5 CONSTRAINED OPTIMIZATION VIA LAGRANGE MULTIPLIERS
- Lagrange multipliers incorporate constraints into the optimization used to bound the objective.After optimization, a positive multiplier indicates a constraint that is active and satisfied with equality.Source: §2.5 · p. 3
3 A MULTI-NEURON RELAXATION BASED BAB FRAMEWORK
MN-BAB combines multi-neuron constraints with Branch-and-Bound, using optimized lower bounds and a branching method tailored to those constraints. The framework is shown to be sound and complete.
3.1 EFFICIENT MULTI-NEURON BOUNDING
- Backsubstitution derives lower bounds by recursively substituting layerwise linear bounds and enforcing multi-neuron constraints with Lagrange multipliers.The method also enforces single-neuron and split constraints during ReLU-layer backsubstitution.Source: §3.1 · p. 4
3.2 MULTI-NEURON CONSTRAINT GUIDED BRANCHING
- ACS scores neuron splits using multi-neuron constraint sensitivities for inputs and outputs, targeting nodes whose splits tighten high-sensitivity constraints.The scores can be computed without an additional backsubstitution pass.Source: §3.2 · p. 6
- CAB ranks splits by expected bound improvement per estimated computational cost, using floating-point operations as a local cost approximation.The approach can use any approximation of expected cost.Source: §3.2 · p. 6
3.3 SOUNDNESS AND COMPLETENESS
- MN-BAB is complete: after all ReLU nodes are split and split constraints enforced, a property holds iff exact bounds are positive on every subproblem.The BaB method is sound because its underlying bounding method is sound.Source: §3.3 · p. 6
4 EXPERIMENTAL EVALUATION
MN-BAB is evaluated against established benchmarks and on more challenging, higher-accuracy networks. Its strongest gains appear on harder problems, where multi-neuron constraints and branching heuristics reduce subproblems and verification time.
Experimental Setup
- The evaluation uses MNIST and CIFAR10 networks, including three adversarially trained residual networks, and compares MN-BAB with β-CROWN, OVAL, and ERAN.Experiments use a GPU-based PyTorch implementation and attempt to falsify each property with an adversarial attack before certification.Source: §4 · p. 7
Comparison to State-of-the-Art Methods
- On unsolved networks where MILP verification does not scale, MN-BAB consistently achieves the highest certified accuracy and has the lowest runtime on all but one.On established MNIST and the smallest CIFAR10 benchmark, ERAN verifies properties completely or almost completely in under 50 seconds per sample.Source: §4 · p. 7
Effectiveness of ACS Branching
- ACS reduces subproblems by one to two orders of magnitude and cuts average verification time by 12% on ResNet6-A and 21% on ResNet6-B.ACS uses fewer subproblems on most properties for ResNet6-A and all properties for ResNet6-B; FSB certifies 12% fewer samples than ACS on ResNet6-A.Source: Figure 4 · p. 8, §4 · pp. 8–9
Effectiveness of Multi-Neuron Constraints
- Two to three orders of magnitude fewer subproblems with MNCs on ResNet6-A and ResNet6-B, with up to 12% more verified samples and lower average certification times.The subproblem comparison measures the work needed to prove the same lower bound on the final objective.Source: Figure 3 · p. 8, §4 · p. 8
Effectiveness of Cost Adjusted Branching
- CAB makes every evaluated property faster with ACS, yielding an average speedup of around 50%.CAB is particularly effective with ACS scores and multi-neuron constraints, where bounding costs vary more significantly.Source: Figure 5 · p. 8, §4 · p. 9
Comparison to State-of-the-Art Methods
- 20% more samples verified and around 22% faster on ResNet6-A; on more heavily regularized ResNet6-B, MN-BAB verifies 6% more samples.On harder properties, using single-neuron constraints and BABSR takes up to 33 times longer.Source: §4 · p. 8, Figure 6 · p. 8
5 RELATED WORK
Prior work spans incomplete multi-neuron relaxations, complete solver-based verification, and BaB methods. Related work also develops varied branching heuristics, with cost-aware branching addressing a different consideration than bound improvement alone.
Neural Network Verification Beyond the Single Neuron Convex Barrier
- Incomplete methods use multi-neuron constraints to tighten convex relaxations, while SMT and MILP approaches do not scale beyond small networks.Bunel et al. (2020) formulated BaB for complete verification by recursively splitting problems into easier subproblems.Source: §5 · p. 9
- Related BaB verifiers differ in their constraints and optimization structure; Palma et al. (2021) uses multi-neuron constraints but each constraint includes only one output neuron.GPU-based BaB frameworks have also been proposed, including partially and fully GPU-based approaches.Source: §5 · p. 9
Branching
- Branching heuristics range from exhaustive strong branching to learned or efficiently approximated scores, filtered-smart-branching, and strategies that target unstable neurons.Some approaches approximate bound improvement, while others account for indirect effects or use a different branching objective.Source: §5 · p. 9
6 CONCLUSION
MN-BAB combines BaB with multi-neuron constraints, a branching heuristic, and a parallel-hardware dual solver. The evaluation finds it particularly effective on challenging networks with high natural accuracy and practical relevance.
6 CONCLUSION
- MN-BAB is a complete neural network verifier that combines BaB, tight multi-neuron constraints, a novel branching heuristic, and an efficient dual solver for parallel hardware.Source: §6 · p. 9
- The empirical evaluation finds MN-BAB particularly effective on challenging networks with high natural accuracy and practical relevance.Source: §6 · p. 9
- MN-BAB reaches a new state of the art in several settings.Source: §6 · p. 9
7 ETHICS STATEMENT
Robustness certification can support safer AI systems, but the authors note potential misuse and overreliance in safety-critical settings.
7 ETHICS STATEMENT
- Robustness certification methods can be used to support both ethical and malicious purposes.Source: §7 · p. 10
- Malicious actors could present the approach as sufficient for real-world robustness, potentially contributing to insufficient regulation in safety-critical domains.Source: §7 · p. 10
- The authors describe robustness certification as a step toward safer and more trustworthy AI systems, while noting it can amplify misuse.Source: §7 · p. 10
8 REPRODUCIBILITY STATEMENT
The authors describe how they plan to make the experiments reproducible, using publicly available datasets and fixed random seeds where possible.
8 REPRODUCIBILITY STATEMENT
- Code and trained networks required to reproduce the experiments are to be provided as supplementary material during review and released publicly upon publication.The authors also say they will provide instructions for running them.Source: §8 · p. 10
- All datasets used in the experiments are publicly available.Source: §8 · p. 10
- Random seeds are fixed where possible and provided in the supplementary material.Source: §8 · p. 10
A EXPERIMENT DETAILS
The experimental details specify per-sample timeouts and batch sizes, and describe an adversarial attack run before certification.
A EXPERIMENT DETAILS
- Timeouts for the first four networks were chosen to approximately match average runtimes reported by Wang et al. (2021).The stated aim was to facilitate comparability.Source: A EXPERIMENT DETAILS · p. 14
- Batch sizes for bounding vary with the layer where splitting occurs because memory requirements vary across split layers.Intermediate bounds for neurons before the split layer are kept fixed.Source: A EXPERIMENT DETAILS · p. 14
- Before certification, the verifier runs two targeted PGD attack versions toward all classes, each with five restarts and 50 steps.The attacks use margin loss or GAMA loss, with 10-step output diversification.Source: A EXPERIMENT DETAILS · p. 14
A.1 ARCHITECTURES
This appendix overviews the evaluated architectures and points to tables detailing the convolutional networks and ResNet variants.
A.1 ARCHITECTURES
- The evaluated architectures are overviewed, with MNIST and CIFAR10 convolutional networks detailed in Table 4 and ResNet6-A and ResNet6-B in Table 5.Source: §A.1 · p. 14
- Table 4 describes convolutional networks for CIFAR10 and MNIST, with each listed layer followed by an activation layer and the output layer omitted.Source: Table 4 · p. 14
- In Table 4 notation, CONV specifies output channels, kernel size, stride, and all-around zero padding.Source: Table 4 · p. 14
B SPLIT-COST COMPUTATION FOR CAB
CAB normalizes branching scores by an approximate split cost, estimated from the floating-point work required to recompute bounds after a split.
B SPLIT-COST COMPUTATION FOR CAB
- CAB divides an arbitrary branching heuristic's score by an approximate split cost, considering only the direct cost of the next branching step.The true cost also includes changes to cumulative cost over consecutive steps.Source: B SPLIT-COST COMPUTATION FOR CAB · p. 14
- The direct split cost is approximated by floating-point operations for recomputing intermediate bounds after the split layer.Only bounds for layers after the split are recomputed, because the approach enforces constraints on neurons preceding those in the bounding objective.Source: B SPLIT-COST COMPUTATION FOR CAB · pp. 14–15
- The cost of recomputing an intermediate node's lower or upper bound is estimated from the matrix sizes in its backsubstitution multiplications.Source: B SPLIT-COST COMPUTATION FOR CAB · p. 15
- A split at layer k sums backsubstitution costs across later layers, accounting for the number of nodes and recomputing both lower and upper bounds.The stated factor of 2 accounts for recomputing both bounds; each layer's cost is specified by its layer type.Source: B SPLIT-COST COMPUTATION FOR CAB · p. 15
- For a ReLU layer, the per-layer cost is the neuron count plus the number of multi-neuron constraints.Source: B SPLIT-COST COMPUTATION FOR CAB · p. 15
- For a linear layer, the per-layer cost is the number of elements in its weight matrix.Source: B SPLIT-COST COMPUTATION FOR CAB · p. 15
- For a convolutional layer, the per-layer cost is expressed using its output-channel count, kernel size, and stride.The passage's displayed expression is cj = djk2 j, where kj is the kernel size.Source: B SPLIT-COST COMPUTATION FOR CAB · p. 15