Source-linked AI summary
A Dual Approach to Scalable Verification of Deep Networks
Krishnamurthy, Dvijotham, Robert Stanforth, Sven Gowal, Timothy Mann, Pushmeet Kohli
TL;DR
Formal verification of neural networks seeks provable input-output guarantees, but earlier methods were constrained by model scale, architecture, activation functions, or property complexity. The paper formulates verification as finding the largest property violation, bounds it through Lagrangian duality, and develops an anytime framework with specialized tightness guarantees. It extends verification across general feedforward models and input constraints and attains state-of-the-art verified bounds on MNIST and CIFAR-10, while verifiable-network training remains future work.
Problem
Formal verification needs to provide provable guarantees against any adversary, because standard testing and specific attack algorithms can yield incorrect robustness conclusions.
Method
The framework maximizes the property violation and uses Lagrangian relaxation and duality to compute tractable upper bounds, with an anytime optimization procedure.
Results
The approach applies to arbitrary feedforward architectures and activation functions, handles discrete and combinatorial input constraints, and attains state-of-the-art verified bounds on MNIST and CIFAR-10.
Takeaways & Limitations
Verification becomes practically scalable through unconstrained convex optimization and anytime computation, with provable tightness guarantees available for single-hidden-layer networks.
Takeaways & Limitations
The computed bounds can be loose because the underlying verification optimization is NP-hard, and the proposed extension to training verifiable networks is left for future work.
Abstract
from arXiv · showhide
This paper addresses the problem of formally verifying desirable properties of neural networks, i.e., obtaining provable guarantees that neural networks satisfy specifications relating their inputs and outputs (robustness to bounded norm adversarial perturbations, for example). Most previous work on this topic was limited in its applicability by the size of the network, network architecture and the complexity of properties to be verified. In contrast, our framework applies to a general class of activation functions and specifications on neural network inputs and outputs. We formulate verification as an optimization problem (seeking to find the largest violation of the specification) and solve a Lagrangian relaxation of the optimization problem to obtain an upper bound on the worst case violation of the specification being verified. Our approach is anytime i.e. it can be stopped at any time and a valid bound on the maximum violation can be obtained. We develop specialized verification algorithms with provable tightness guarantees under special assumptions and demonstrate the practical significance of our general verification approach on a variety of verification tasks.
1 INTRODUCTION
The paper targets provable neural-network guarantees beyond weak adversarial testing and prior scalability and architecture limits. It introduces a general, anytime verification framework and reports state-of-the-art verified bounds on MNIST and CIFAR-10.
- Motivation: Standard test-set accuracy and individual attack algorithms do not provide provable guarantees against stronger adversaries, motivating formal verification.Weak adversaries can produce incorrect robustness conclusions, while safety-critical domains require robustness within specified perturbation bounds.
- General framework: The optimization-and-duality framework applies to arbitrary feedforward architectures and activation functions, including discrete inputs and combinatorial constraints.It recovers earlier piecewise-linear results while extending verification to broader model and input classes.
- Scalability: The computation solves an unconstrained convex optimization problem whose size is linear in the number of neurons, and it is anytime.Stopping at any time yields a valid bound on the verification objective.
- Theoretical guarantees: Single-hidden-layer networks receive specialized verification algorithms with provable tightness guarantees.These guarantees address cases where general bounds may otherwise be loose.
- Empirical results: The approach attains state-of-the-art verified bounds on adversarial error rates for MNIST and CIFAR-10 image classifiers under infinity-norm perturbations.The reported result covers both datasets and the infinity-norm robustness setting.
2 Related Work
Prior verification and certifiable-training work used convex optimization, duality, or theoretical robustness analysis, but often imposed architectural or activation restrictions. This paper instead emphasizes extending verification applicability, while leaving verifiable-network training as future work.
- Certifiable training and verification: Earlier certifiable-training approaches construct verification bounds but are limited to particular activation-function classes or network architectures.Their goal is also to train networks that are easier to verify, unlike this paper’s focus on extending verification.
- Certifiable training and verification: The paper distinguishes its verification-extension goal from prior work that modifies network training to make models easier to verify.The authors note that their differentiable dual objective could support such training, but do not study that extension here.
- Theoretical analysis of robustness: Theoretical robustness studies analyze when adversarial examples arise for ReLU networks, under alternative assumptions, and for nearest-neighbor classifiers.These works provide robustness analysis rather than the paper’s general verification framework.
3 VERIFICATION AS OPTIMIZATION
The paper formulates neural-network verification as finding the largest violation of an input-output property, then uses duality to compute tractable upper bounds. This framework supports broad network and property classes, while specialized results characterize when verification is exact or has guaranteed approximation quality.
- Verification formulation: The framework assumes finite linear output constraints and bounded input sets whose linear optimization problems can be solved efficiently.The input sets may include convex sets and combinatorial structures such as spanning trees, graph cuts, and cardinality constraints.
- Verification formulation: Verification searches for the largest violation of an input-output property over a constrained input set and output constraints.A property is verified when the optimization value is below zero; multiple output constraints can be checked separately.
- Bounding the objective: A Lagrangian relaxation provides a valid upper bound on the nonconvex verification objective, and optimizing the relaxation is a convex problem.The bound is sound because feasible solutions of the original problem remain feasible in the relaxed problem and the added terms vanish there.
- Bounding the objective: The approach applies to arbitrary feedforward architectures and activation functions, and recovers prior results for piecewise linear activations.The paper contrasts its unconstrained dual formulation with an alternative that introduces nonconvexity through a backpropagation-like transformation.
- Theoretical guarantees: The bounds may be loose because the original verification problem is NP-hard, motivating theoretical guarantees for exact or approximate verification.Under special assumptions, small perturbation radii permit exact optimization, while a quadratic approximation differs from the original objective by at most κϵ3.
4 EXPERIMENTS
The experiments evaluate verification on image classification, adversarially trained models, GitHub classifier stability, and complex multi-input specifications. Across these tasks, the approach produces tight or improved bounds, including results beyond competing methods' architectural scope.
- Experimental tasks: The study evaluates image classification on MNIST and CIFAR-10, GitHub classifier stability, and more complex verification specifications.The image experiments use varying perturbation radii, while the GitHub task studies prediction switches over time.
- Image classification: For smooth activations, the approach computes nearly tight bounds up to 2 pixel units and significantly outperforms the SDP approach.The SDP method computes nontrivial bounds only for the smallest model with 20 hidden units.
- Adversarially trained models: Adversarially trained MNIST and CIFAR models are evaluated by comparing LBFGS-style attacks with verified upper bounds.The SDP comparison is omitted because these models are multilayer and the cited SDP approach does not apply.
- GitHub classifier stability: Figure 1 compares LBFGS attack lower bounds, the paper's verified upper bounds, and SDP verified upper bounds across networks.Dashed, solid, and dash-dot curves encode the three bound types, while colors distinguish networks.
- GitHub classifier stability: The GitHub experiment shows initially attackable predictions and tracks how the gap between the paper's bound and LBFGS attack evolves over time.The verification framework models target-class reachability at each timestep and uses dynamic programming to maximize switches.
- Complex specifications: On a two-digit MNIST sum task, the approach computes tight bounds on the maximum prediction-sum error for an adversarially trained sigmoid network.The attacker jointly chooses perturbations to both images and their sizes under a total perturbation constraint.
5 CONCLUSIONS
The paper presents a scalable verification framework for broad neural-network architectures, activation functions, and input constraints. Numerical studies and theoretical results support its practical performance and special-case tractability.
- The framework applies to arbitrary feedforward architectures and activation functions, while supporting more general input constraints such as cardinality constraints.Its verification procedure uses unconstrained convex optimization and anytime gradient-like steps.
- The paper proves, under special assumptions, the first known theorems showing that nonlinear neural networks can be verified tractably.The conclusion also reports numerical performance across several classes of verification tasks.
6.1 BOUND TIGHTENING
The bound-tightening procedure improves activation bounds and then reruns dual optimization to obtain tighter verification objectives. Its anytime property allows valid intermediate bounds at any stopping point.
- Interval arithmetic provides recursive bounds on intermediate neural activations, but these bounds can be loose.The method starts from input bounds and propagates them layer by layer.
- Dual relaxation can produce tighter upper bounds on activations, and any chosen dual variables yield a valid bound during computation.This anytime property permits stopping at any time while retaining valid bounds.
- Tightened activation bounds are propagated to preactivations and substituted into the verification relaxation to compute a tighter verification-objective upper bound.The procedure first tightens bounds for each layer and then reruns the dual optimization.
6.2 CONJUGATES OF TRANSFER FUNCTIONS
The framework bounds nonlinear transfer-function terms through tractable local optimization or domain decomposition. Finer decompositions yield arbitrarily tight upper bounds for general nonlinearities.
- Common transfer functions: The method computes the conjugate optimization g⋆ over an activation interval, analytically for common transfer functions when possible.For ReLUs, evaluating interval endpoints and zero suffices when zero lies inside the interval.
- Common transfer functions: For sigmoids, the optimum occurs at an interval boundary or at an interior point where the derivative of g vanishes.Interior candidates are retained only when they lie within the activation domain.
- Max-pooling: For max-pooling, the method optimizes separately for each component attaining the maximum and then takes the largest resulting value.The one-dimensional subproblem for each component can be solved by binary search.
- General nonlinearities: Independent optimization of the two terms in g gives weak bounds, while decomposing the input domain makes the bound tighter.The decomposition applies the relaxation separately over subintervals.
- General nonlinearities: As the domain decomposition becomes finer, with |a_i − b_i| → 0, the resulting upper bound on g becomes arbitrarily tight.This provides a limiting tightness guarantee for the decomposition-based bound.
6.3 OPTIMIZING OVER THE INPUT CONSTRAINTS
The framework optimizes its verification objective over input constraints, using closed-form solutions for common constraint sets. These include norm, combinatorial, and cardinality constraints.
- Norm constraints: For norm-bounded inputs, Hölder’s inequality yields an exact optimum involving the dual norm.The bound is attainable for an appropriate choice of x.
- Combinatorial objects: Linear objectives over spanning-tree constraints can be optimized efficiently using a maximum spanning tree algorithm.
- Cardinality constraints: Cardinality constraints restrict x to at most k nonzero elements, enabling optimization based on the relevant components of the objective vector.
6.4 PROOFS OF THEORETICAL RESULTS
The theoretical results establish hardness for sigmoid verification and characterize the relationship between the proposed dual formulation and existing ReLU linear-programming relaxations. Additional proofs bound smooth objectives and error terms under norm constraints.
- 6.4.1 NP-hardness: Verification with sigmoid activations and infinity-norm perturbations becomes a sigmoidal programming problem, which is NP-hard.
- 6.4.2 Proof of theorem 2: For ReLU networks, the dual objective matches the LP relaxation of Ehlers after maximizing over the relevant piecewise-linear cases.The derivation evaluates maxima at interval bounds or the breakpoint 0, then recovers the existing relaxation.
- 6.4.2 Proof of theorem 2: The resulting dual objective exactly matches the calculations from Section 3.3 for the piecewise-linear case.
- Smooth objectives: A smooth nonlinear objective can be efficiently optimized over a sufficiently small ball by bounding the Lipschitz constant of its derivative.The proof applies a theorem from Polyak to the derived derivative bound.
- Error bounds: Under an l2 input perturbation bound, each linear term is bounded using the corresponding row norm, and the aggregate error terms yield the stated result.