Source-linked AI summary
A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks
Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, Pengchuan Zhang
TL;DR
Tight robustness verification is difficult because exact methods are expensive and relaxed methods may leave substantial gaps. The paper unifies LP-relaxed verifiers, characterizes their optimal layer-wise relaxation, and tests that limit experimentally. Across varied networks and datasets, the optimal relaxation still does not substantially close the gaps to PGD or exact verification, indicating a barrier for methods in this framework.
Problem
The paper asks whether efficient layer-wise convex relaxations can provide tight neural-network robustness verification despite exact verification’s computational difficulty.
Method
The authors unify primal and dual LP-relaxed verifiers in a layer-wise convex framework and compute its optimal relaxation for ReLU networks.
Results
Across models, training methods, and MNIST and CIFAR-10, the optimal relaxation only slightly improves existing lower bounds and does not significantly close gaps to PGD or MILP.
Takeaways & Limitations
The results suggest an inherent barrier to tight verification for the large class of methods captured by the framework.
Takeaways & Limitations
The barrier applies only to methods described by the framework, which excludes SDP, local-Lipschitz, randomized-smoothing, and hybrid techniques.
Abstract
from arXiv · showhide
Verification of neural networks enables us to gauge their robustness against adversarial attacks. Verification algorithms fall into two categories: exact verifiers that run in exponential time and relaxed verifiers that are efficient but incomplete. In this paper, we unify all existing LP-relaxed verifiers, to the best of our knowledge, under a general convex relaxation framework. This framework works for neural networks with diverse architectures and nonlinearities and covers both primal and dual views of robustness verification. We further prove strong duality between the primal and dual problems under very mild conditions. Next, we perform large-scale experiments, amounting to more than 22 CPU-years, to obtain exact solution to the convex-relaxed problem that is optimal within our framework for ReLU networks. We find the exact solution does not significantly improve upon the gap between PGD and existing relaxed verifiers for various networks trained normally or robustly on MNIST and CIFAR datasets. Our results suggest there is an inherent barrier to tight verification for the large class of methods captured by our framework. We discuss possible causes of this barrier and potential future directions for bypassing it. Our code and trained models are available at http://github.com/Hadisalman/robust-verify-benchmark .
1 Introduction
The paper unifies existing relaxed robustness verifiers through a layer-wise convex relaxation framework and investigates whether its theoretical limit can yield tight verification.
- Existing robustness verifiers lower-bound a robustness objective using either primal or dual convex relaxations.
- The framework unifies these approaches and reveals their relationships.
- The optimal layer-wise convex relaxation defines a theoretical performance limit for methods within the framework.
- Extensive experiments with deep ReLU networks test whether faster and more accurate layer-wise relaxations can approach tight verification.
- Across models, training methods, and MNIST and CIFAR-10, PGD upper bounds are consistently 1.5 to 5 times larger for minimum l∞ adversarial distortion.
- The optimal relaxation does not significantly close the robust-error gap between PGD or MILP and Wong and Kolter’s verifier.
2 Preliminaries and Related Work
Neural-network verification includes exact methods that are difficult to scale and relaxed methods that trade completeness for computational efficiency. The paper places many primal and dual LP-relaxed approaches in one framework while identifying important exclusions.
- Exact verifiers typically use MILP or SMT solvers, but neural-network robustness verification is NP-complete and challenging to scale.
- Relaxed verifiers solve computationally efficient but incomplete versions of the verification problem.
- Primal view: Primal relaxations replace nonlinear activation constraints with linear inequalities, including abstract transformers, linear outer bounds, and interval bound propagation.
- Dual view: Dual approaches study either the dual of a relaxed problem or the dual of the original nonconvex verification problem.
- The framework unifies both primal and dual views for neural-network verification and clarifies their relationships.
- Scope: SDP, local-Lipschitz, randomized-smoothing, and hybrid exact-relaxed techniques are outside the paper’s focused framework.
3 Convex Relaxation from the Primal View
The primal formulation models neural networks with bounded preactivations and replaces nonlinear activation equalities by convex upper and lower constraints. Its optimal layer-wise relaxation uses convex hulls of individual nonlinear constraints, while linear bounds recover several existing verifiers.
- Problem setting: The problem setting assumes a convex input neighborhood and an L-layer feedforward neural network.
- Problem setting: The network formulation supports nonlinear activations such as ReLU, sigmoid-family functions, and pooling, with extensions to convolutional layers and skip connections.
- Examples: For ReLU and the step function, the optimal relaxations are expressed with 3 and 4 linear constraints, respectively.
- Convex relaxation: The primal relaxation replaces each nonlinear equality x^(l+1) = σ^(l)(z^(l)) with convex inequality constraints between lower and upper activation bounds.
- Convex relaxation: The feasible relaxed set is convex, and tighter valid preactivation bounds can narrow the optimization domain and improve relaxed solutions.
- Optimal relaxation: For ReLU, the optimal layer-wise relaxation is the convex hull of the individual nonlinear constraint under mild non-interactivity assumptions.
- Optimal relaxation: The paper distinguishes optimal relaxation of each nonlinear constraint from optimal relaxation of the original nonconvex feasible set.
- Linear bounds: Layer-by-layer propagation of one linear upper and lower bound recovers methods including Fast-Lin, DeepZ, Neurify, CROWN, and DeepPoly.
4 Convex Relaxation from the Dual View
The paper connects dual robustness verification to primal convex relaxations through a common framework. Strong duality and equivalence results show that the primal and dual formulations face the same relaxation barrier.
- Dual formulation: The dual view introduces dual variables through the Lagrangian of the convex-relaxed verification problem and connects it to the primal view.The dual variables are determined by backward propagation.
- Strong duality: Strong duality holds between the convex-relaxed primal problem and its dual under finite Lipschitz conditions, without assuming Slater’s condition.The nonlinear functions and their bounds need finite Lipschitz constants on each layer’s domain.
- Optimal dual relaxation: Taking the dual of the layer-wise convex-relaxed problem cannot improve the original relaxation, motivating the study of the Lagrangian dual of the original nonconvex problem.The latter formulation was first proposed by Dvijotham et al. [2018b].
- Equivalence: The dual of the optimal layer-wise convex-relaxed problem and the dual of the original problem provide the same lower bound.The equivalence is stated for the corresponding optimal dual relaxations.
- Barrier: Strong duality implies that the primal relaxation and both dual relaxations are blocked by the same barrier.For the listed activations, the primal and dual optimal bounds coincide.
- Existing algorithms: With linear relaxed bounds, greedy dual optimization recovers Wong and Kolter, Fast-Lin, and CROWN under different slope choices.The slope parameter determines which existing verifier is recovered.
5 Optimal LP-relaxed Verification
For ReLU networks, the framework’s tightest convex relaxation becomes an LP that can be solved exactly, enabling direct tests of the relaxation barrier. Experiments compare this optimum with greedy relaxations, PGD, and MILP-based verification.
- Scope: For ReLU networks, the framework’s convex-relaxed verification problem is an LP, and the paper studies its tightest achievable solution.The framework excludes the SDP relaxation of Raghunathan et al. [2018b].
- Conclusion: The framework subsumes existing layer-wise convex-relaxed verification algorithms except Raghunathan et al.’s SDP relaxation, and establishes a barrier for the included methods.For ReLU networks, the included methods correspond to existing LP-relaxed algorithms.
- Experimental comparison: The experiments evaluate LP-ALL, the tightest framework relaxation, against LP-GREEDY, LP-LAST, PGD, and MILP.LP-GREEDY uses heuristic dual bounds, while LP-LAST solves the final LP exactly with greedy preactivation bounds.
- Evaluation caveat: MILP comparisons use a 3600-second time limit, leaving gaps for ADV- and normally trained networks but matching bounds for LPD-trained networks.The reported MILP bounds therefore depend on whether the solver reaches its time limit.
- Exact optimization: Exact LP-ALL verification requires tight preactivation bounds for all non-final neurons followed by exact LP solutions for final-layer comparisons.The neuron-wise subproblems can be solved independently and in parallel.
6 Experiments
The experiments evaluate LP-ALL against existing relaxed, attack-based, and exact verification methods across ReLU networks, datasets, and training modes. LP-ALL improves over LP-GREEDY but generally leaves substantial gaps to PGD or exact results.
- Experimental setup: Experiments cover certified robust-error bounds and minimum adversarial-distortion bounds on MNIST and CIFAR-10.They use ReLU feedforward architectures trained normally, with PGD, or with LP-relaxed dual training.
- Experimental setup: 22 CPU-years of computation support large-scale comparisons across the evaluated networks.Experiments run on a cluster with 1000 CPU-nodes.
- Certified robust error: LP-ALL is tighter than LP-GREEDY in every robust-error case, but the improvement is insufficient to close gaps to PGD and MILP lower bounds for normally and adversarially trained networks.For LP-trained networks, LP-ALL improves only modestly at ϵ = 0.1; at larger ϵ, the absolute improvement is 4−7%.
- Minimum adversarial distortion: 1.5 to 5 times smaller certified distortion bounds occur than PGD upper bounds on MNIST for normally or adversarially trained networks.For LP-trained networks, the gap is below 1.5 times; on CIFAR-10, gaps range from 1.5 to 2 times across models.
- Minimum adversarial distortion: LP-LAST and LP-ALL do not improve enough over LP-GREEDY to close the PGD gap, including for randomly initialized networks.The distortion experiment evaluates only ten MNIST and CIFAR-10 samples because LP-ALL is expensive.
7 Conclusions and Discussions
The discussion identifies looseness sources within layer-wise convex relaxation and clarifies the framework’s scope. It also points to branch-and-bound and richer relaxations as possible ways around the barrier.
- Scope and barrier: The framework unifies prior LP-relaxed verifiers in primal and dual spaces, but its barrier applies only to methods describable within this framework.The paper distinguishes this framework from other potentially tighter convex relaxations and from SDP-based verification.
- Sources of looseness: Relaxing nonlinearities over box domains can lose within-layer coordinate correlations and produce looser bounds.The framework still uses bounds to capture correlations across later layers, but treats same-layer coordinates individually.
- Sources of looseness: Recursive bound computation accumulates gaps across layers, which can be problematic for very deep or recurrent networks.Earlier loose bounds make later-layer bounds looser.
- Sources of looseness: For ReLU networks, relaxing unstable neurons introduces additional looseness.The paper proposes strategically splitting unstable-neuron domains with branch-and-bound as one possible direction.
- Optimal layer relaxations: The single-neuron convex-hull relaxation has a simple analytic form for non-interactive layers, including entry-wise activations and non-overlapping MaxPool.Non-interactive means each output depends on a disjoint subset of input coordinates.
D Greedily solving the primal with linear bounds.
The primal method greedily propagates linear upper and lower bounds through network layers, connecting several existing verifiers within the convex-relaxation framework. Its efficiency comes from avoiding LP solves, while its bounds depend on layerwise relaxation choices.
- Bound propagation: Greedy primal solving forms linear bounds layer by layer and can continue propagation back to the input.Substitution through affine layers preserves linearity while collecting bias terms and adjusting coefficients by weight signs.
- Connections to existing methods: Fast-Lin, DeepZ, and Neurify use matching upper and lower slopes, producing a zonotope relaxation.CROWN and DeepPoly remove this shared-slope restriction and achieve tighter verification results than Fast-Lin and DeepZ.
- Bound propagation: The method’s final linear bounds directly bound network outputs over the perturbation neighborhood.The output objective can be treated as an additional linear layer.
- Efficiency: Bound propagation requires no LP solver and has quadratic time complexity in the number of layers.Bounds for earlier layers are computed before later layers, yielding O(l) work per layer.
- Connections to existing methods: CROWN and DeepPoly adapt linear bounds to minimize approximation error, whereas interval bound propagation decouples layers and gives looser bounds.The greedy primal and dual algorithms are closely connected through the dual of the relaxed problem.
- Connections to existing methods: The framework contains CROWN and Fast-Lin as special cases using one linear upper and one linear lower bound per constraint.CROWN allows different upper and lower slopes, unlike Fast-Lin.
- Primal-dual connection: The framework’s strong duality result links the primal convex relaxation to its dual formulation under mild conditions.The result is stated as strong duality with dual optimum attainment at least when ν > 0.
E.1 Cases where the Slater’s condition fails but strong duality holds true by Theorem 4.1
Theorem 4.1 establishes strong duality under finite-Lipschitz activation bounds even when Slater’s condition fails, including degenerate boundary cases. The proof uses Lipschitz continuity and perturbation analysis rather than relying on Slater’s condition.
- Theorem 4.1 guarantees strong duality for loose or tight activation bounds and finite-Lipschitz activations on those domains.The result applies beyond cases where Slater’s condition holds.
- Loose activation bounds can force feasible activations onto boundaries, causing Slater’s condition to fail.One example fixes the only feasible preactivation at -1, making the ReLU output uniquely zero.
- Later-layer activation bounds can similarly force earlier-layer feasible points onto nonlinear-constraint boundaries, producing another Slater failure.This situation can arise when branch-and-bound splits unstable neurons.
- The proof handles these edge cases by exploiting Lipschitz continuity of problem (C), with perturbation bounds propagated across layers.The analysis defines achievable activation sets recursively and bounds their distances through linear and nonlinear layers.
- The perturbation argument establishes the required bounds by induction across layers and then transfers them to the terminal optimization value.The proof separately treats infeasible and feasible perturbed problems.
- The duality analysis further rewrites dual objectives using activation bounds and convex-conjugate identities before equating the relevant primal and dual expressions.These transformations lead to the stated strong-duality result.
G.1 Some useful results to simplify the dual problems
The paper derives simplified dual formulations and identifies conditions under which convex-relaxed and original dual problems coincide or become easier to solve. It also presents a greedy approximation strategy and relates it to prior work.
- The dual of the convex-relaxed problem can be rewritten as an unconstrained optimization using a two-argument function gC.This formulation is introduced as a useful simplification for solving the dual problem.
- For the convex-relaxed and original nonconvex problems, the dual objectives are expressed using gC and gO under their respective definitions.The resulting forms isolate layerwise contributions through the activation functions and bounds.
- If a nonlinear neuron is effectively linear and non-interacting over the input domain, the convex-relaxed problem can be simplified by replacing its nonlinear constraint.The corresponding dual formulation admits the same simplification under the stated condition.
- A dual greedy algorithm approximately solves the dual by using optimal variables for stable neurons and closed-form suboptimal variables for unstable neurons.The resulting lower bound is summarized after combining these layerwise choices.
- The greedy algorithm recovers the method of Wong and Kolter (2018) under the paper’s notation.Their ν corresponds to µ, and their bν corresponds to λ.
- Strong duality permits choosing either primal or dual optimization; piecewise-linear bounds yield LPs, while non-piecewise-linear cases favor the unconstrained dual.The dual can also be stopped early to provide a lower bound.
I Additional Experimental Details
The experiments measure LP-ALL’s computational cost across architectures, training modes, datasets, and layers. Solve time grows with network size and depth because the LP gains decision variables and constraints.
- LP-ALL requires solving roughly 100k LPs for a 10k-neuron network evaluated on ten MNIST samples.The number of LPs scales with the number of neurons being verified.
- At an average of 10 seconds per LP, verifying one network can require roughly 1 million seconds, or about 11 days.The estimate motivates extensive parallelization.
- The experiments use a 1,000-CPU-node cluster because the full workload involves roughly 100 million jobs.Low scheduling latency is important because individual jobs take seconds.
- Dependence on architecture and training mode: LP solve time increases as networks become wider or deeper because the number of LP decision variables and constraints increases.Figures 5 and 6 average solve time over all neurons and ten samples on MNIST and CIFAR-10.
- Dependence on which layer we are solving for: LP solve time also increases for neurons in deeper layers of CIFAR-10 networks.Figure 7 reports average solve time per neuron and layer.
L.2 Results
Across ten-sample MNIST and CIFAR-10 evaluations, LP-ALL provides only modest improvement over cheaper relaxed verifiers and does not close the gap to PGD-based upper bounds.
- Tables 2 and 3 compare training modes, mean lower bounds from LP-GREEDY, LP-LAST, and LP-ALL, PGD upper bounds, and median percentage gaps.The comparison covers ten samples from MNIST and CIFAR-10.
- LP-GREEDY ≤ LP-LAST ≤ LP-ALL for the certified lower bounds on adversarial distortion.The ordering follows from progressively tighter relaxed procedures.
- LP-ALL and LP-LAST improve over LP-GREEDY, but the improvement is not significant and does not close the gap with PGD.Thus, solving the tighter relaxation does not substantially narrow the verification gap in these experiments.
M Results on Randomly Initialized Networks
On randomly initialized MNIST and CIFAR-10 networks, certified lower bounds on minimum adversarial distortion remain substantially below PGD’s upper bounds. More accurate LP relaxations provide little additional improvement.
- 2 to 3 times smaller: certified lower bounds on ε from LP-GREEDY, LP-LAST, and LP-ALL than PGD’s upper bound.This pattern holds for all networks and both datasets.
- The experiment reports certified bounds on minimum adversarial distortion ε for ten random MNIST test samples.
- The corresponding CIFAR-10 results report certified bounds on minimum adversarial distortion ε for ten random test samples.
- Table 4 covers MNIST and CIFAR-10 randomly initialized networks without training.