Training for Faster Adversarial Robustness Verification via Inducing ReLU Stability

Kai Y. Xiao; Vincent Tjeng; Nur Muhammad Shafiullah; Aleksander Madry

Source-linked AI summary

Training for Faster Adversarial Robustness Verification via Inducing ReLU Stability

Kai Y. Xiao, Vincent Tjeng, Nur Muhammad Shafiullah, Aleksander Madry

arXiv:1809.03008v3Sep 9, 2018cs.LGcs.CRcs.NEstat.ML

TL;DR

Exact neural-network verification can be intractably slow, motivating models that are both adversarially robust and easier to verify. The paper co-designs training and verification by inducing weight sparsity and ReLU stability, achieving substantially faster verification, including an additional 4–13x speedup, while supporting broad procedures and verifiers.

Problem
Exact verification formally proves robustness to small perturbations but is often computationally intractable for neural networks.
Method
The paper co-designs robust training with verification by inducing weight sparsity and ReLU stability, using regularization to reduce verifier complexity and branching.
Results
The techniques make exact verification significantly faster, with ReLU-stability regularization providing an additional 4–13x speedup while maintaining state-of-the-art MNIST accuracy and similar CIFAR improvements.
Takeaways & Limitations
Verification-aware training can produce robust networks that are easier to verify across training procedures and exact verification approaches.
Takeaways & Limitations
The methods focus on ℓ∞ norm-bounded perturbations, although the authors state they can apply to other ℓp norms and broader perturbation sets.

Abstract

from arXiv · show

We explore the concept of co-design in the context of neural network verification. Specifically, we aim to train deep neural networks that not only are robust to adversarial perturbations but also whose robustness can be verified more easily. To this end, we identify two properties of network models - weight sparsity and so-called ReLU stability - that turn out to significantly impact the complexity of the corresponding verification task. We demonstrate that improving weight sparsity alone already enables us to turn computationally intractable verification problems into tractable ones. Then, improving ReLU stability leads to an additional 4-13x speedup in verification times. An important feature of our methodology is its "universality," in the sense that it can be used with a broad range of training procedures and verification approaches.

1 INTRODUCTION

The paper proposes co-designing robust neural networks for easier exact verification by inducing weight sparsity and ReLU stability. These techniques substantially accelerate verification while preserving strong robustness results and broad compatibility with training and verification procedures.

Motivation: Exact verification formally proves that no small input perturbation causes misclassification, but existing methods can be computationally intractable.The paper identifies addressing this intractability as its primary goal.
Co-design: Training and verification are usually decoupled, but co-design aligns them by training models that are both robust and easy to exactly verify.This alignment is the foundation of the paper’s techniques.
Training objectives: Weight sparsity makes verification faster by reducing the number of variables in verifier formulations, including LP constraints.The paper uses methods such as ℓ1-regularization to induce sparsity.
Training objectives: ReLU stability reduces branching by encouraging each ReLU to remain always active or always inactive under input perturbations.The paper introduces a regularization technique specifically to induce this property.
Results: 4–13x faster verification follows from adding ReLU-stability regularization to sparse, adversarially trained networks, while maintaining state-of-the-art MNIST accuracy.Similar improvements are reported for exact verification of CIFAR models.
Universality: The methodology is designed to work with broad training procedures and current or future exact verifiers, especially LP/MILP-based methods.The training techniques improve the verifier’s input rather than depending on a particular verifier.

2 BACKGROUND AND RELATED WORK

Exact verification is relatively simple for linear networks but becomes difficult for ReLU networks because active and inactive cases require branching. Relaxation-based certification methods address inefficiency by solving an approximate verification problem instead.

Exact verification: For linear networks, exact verification can be performed relatively simply by solving a linear program.Nonlinear ReLUs make verification over all input perturbations more challenging.
Evaluation setting: A 120-second per-image time budget was used for verification experiments.
Exact verification: ReLUs may be active or inactive depending on the input, forcing exact verifiers to branch over separate cases.The number of cases can grow exponentially with the number of ReLUs, and exact verification is NP-complete.
Certification methods: Certification methods improve efficiency by solving a relaxation rather than directly solving the exact verification task.These relaxations are usually derived by overapproximating the adversarial polytope.
Related work: Interval bound propagation combined with MILP-based exact verification can produce provably robust networks.

3 TRAINING VERIFIABLE NETWORK MODELS

The paper co-designs training and verification by inducing weight sparsity and ReLU stability in robust networks, making exact verification substantially faster while preserving strong accuracy.

3.2 WEIGHT SPARSITY AND ITS IMPACT ON VERIFICATION SPEED: Weight sparsity improves exact verification because LP and MILP formulations benefit from fewer variables.The paper uses ℓ1-regularization and small-weight pruning to promote sparsity.
3.2 WEIGHT SPARSITY AND ITS IMPACT ON VERIFICATION SPEED: Adversarial training alone improves weight sparsity, but ℓ1-regularization and small-weight pruning further produce networks that are easier to verify.These methods were still necessary despite the sparsity induced by adversarial training.
3.3 RELU STABILITY: ReLU stability means a ReLU's activation sign remains unchanged for every allowed perturbation, eliminating the need to branch on that ReLU.Unstable ReLUs create the primary exact-verification bottleneck because branching over activation cases can grow exponentially.
3.3.1 A REGULARIZATION TECHNIQUE FOR INDUCING RELU STABILITY: RS LOSS: RS Loss uses smooth bounds-based regularization to reduce unstable ReLUs and thereby speed exact verification.The bounds are estimated with naive or improved interval arithmetic; improved interval arithmetic trades additional memory and training time for tighter estimates.
3.3.3 IMPACT OF RELU STABILITY IMPROVEMENTS ON VERIFICATION SPEED: 65x faster verification accompanied a reduction to 16% as many unstable ReLUs when RS Loss weight increased from 0 to 5e−4, with 1.00% lower test accuracy.Across MNIST perturbation sizes, RS Loss still produced a 4–13x speedup with less than 0.50% test-accuracy loss; CIFAR speedups were 1.6–3.7x.

4 EXPERIMENTS

The experiments compare networks trained with and without RS Loss against certifiable defenses, measuring standard, PGD adversarial, and provable adversarial accuracy. RS Loss improves verification speed while largely preserving test accuracy, with stronger speedups on MNIST than CIFAR-10.

Provable robustness: On MNIST, the method achieves significantly better provable adversarial accuracy than Wong et al. for ϵ = 0.3 and comparable accuracy for ϵ = 0.1.On CIFAR-10, its provable adversarial accuracy is slightly lower, possibly indicating that unstable ReLUs help learn a robust classifier.
Verification behavior: Verification reached the 120-second time limit more often on CIFAR-10, especially for less ReLU-stable control networks.The experiments used the exact verifier from Tjeng et al. and reported solve times rather than model-build times.
Experimental comparison: Table 3 compares test set, PGD adversarial, and provable adversarial accuracy for control, +RS, +RS (Large), and prior certifiable-defense models.The +RS (Large) provable accuracy is computed only on the first 1000 images because verification is slower on larger models.
Training and setup: The training setup used robust adversarial training, line-searched RS Loss weights, and the same convolutional architecture for ease of comparison.Improved interval arithmetic was used for +RS models, while +RS (Large) models used naive interval arithmetic because of memory constraints.

5 CONCLUSION

The conclusion presents co-design as a way to train robust networks that are also easier to verify. Weight sparsity improves tractability first, while ReLU stability provides an additional 4–13x verification speedup.

Conclusion: The paper’s co-design training methods emphasize verification during training and make verification of the trained models much faster.The approach targets both robustness and ease of exact verification.
ReLU stability: 4–13x additional speedup follows from improving ReLU stability after weight-sparsity regularization.The method introduces ReLU stability and regularizes networks to reduce verification branching.
Universality: The method is described as universal because it can be added to broad training procedures and should speed up exact verification, especially MILP-based methods.The conclusion frames this as a property of the methodology rather than a single training or verification pipeline.
Future directions: Future work could explore model-compression techniques and objectives beyond weight sparsity and ReLU stability to improve ease of verification.The authors hypothesize that their methods compress networks into more compact, simpler forms.
Weight sparsity: Natural regularization methods make exact verification significantly more tractable by improving weight sparsity.Weight sparsity reduces the number of variables in the verifier’s linear programs.

A.2 A BASIC IMPROVEMENT FOR INDUCING RELU STABILITY: RELU PRUNING

ReLU pruning removes units judged unnecessary or rarely used, aiming to improve ReLU stability without materially changing network behavior. The paper reports that removing some ReLUs does not hurt clean or PGD accuracy.

ReLU pruning: ReLU pruning removes ReLUs that are not necessary for the network’s behavior.The procedure is presented as a basic method for improving ReLU stability.
Pruning criterion: A ReLU active on every training image can be replaced by the identity function without changing behavior on those images.The analogous replacement for a ReLU inactive on every training image is the zero function.
Pruning criterion: ReLUs activated or inactivated on fewer than 10% of training examples were conservatively selected for pruning.The rationale is that rarely used ReLUs should only slightly change network behavior when removed.
Empirical effect: Removing some ReLUs does not hurt test set accuracy or accuracy against a PGD adversary.Figure 3 provides experimental evidence for this behavior on an adversarially trained MNIST model.

B ADVERSARIAL TRAINING AND WEIGHT SPARSITY

Adversarial training can promote weight sparsity, but efficient exact verification also requires handling ReLU branching. The paper develops interval-bound improvements that exploit stable ReLUs and propagate tighter bounds across layers.

Adversarial training and sparsity: Adversarial training limits perturbations through an ℓ1-related weight objective, which promotes weight sparsity in linear networks.For nonlinear networks, experiments also show improved weight sparsity, although adversarial training alone is insufficient for efficient exact verification.
Verification bottleneck: Exact verification becomes difficult because ReLUs may be active or inactive, forcing verifiers to branch over cases that can grow exponentially with the number of ReLUs.The paper notes that exact verification is NP-complete for these networks.
Naive interval arithmetic: Naive interval arithmetic computes each layer’s bounds from the previous layer’s bounds using upper and lower weights and activations.The bounds are efficient to compute but can become conservative for deeper networks.
Improved interval arithmetic: Improved interval arithmetic uses ReLUs known to be always active to cancel equivalent symbols from earlier layers and obtain tighter bounds.In the one-hidden-layer example, two always-active ReLUs allow the input terms to cancel, yielding exact output bounds 4 and 4.
Computational cost: Using information from all previous layers requires O(k) matrix-matrix multiplications for layer k and O(d^2) additional multiplications across a d-layer network.The method remains relatively efficient because it uses matrix multiplications rather than optimization solves.

C.3 EXPERIMENTAL RESULTS ON IMPROVED IA AND NAIVE IA

The section compares improved interval analysis (IA) and naive IA against exact verification for estimating unstable ReLUs in MNIST networks.

Improved IA estimates track exact-verifier counts quite well across layers.
Table 4 compares exact-verifier counts of unstable ReLUs with estimates from improved IA and naive IA.
The comparison covers control and “+RS” MNIST networks.

C.4 ON THE CONSERVATIVE NATURE OF IA BOUNDS

IA bounds are conservative, so unstable ReLUs are correctly identified while some stable ReLUs may be mislabeled and unnecessarily regularized. RS Loss reduces estimated instability while preserving similar accuracy.

Every unstable ReLU is correctly labeled as unstable by IA bounds, but stable ReLUs may be labeled unstable.
Table 5 reports these objectives for both 3-layer and 6-layer networks, with a small test-set-accuracy decrease.
RS Loss reduces the number of ReLUs labeled unstable while maintaining similar test set and PGD adversarial accuracy.
290.5 to 105.4 unstable-ReLU labels accompanied a 0.26% test-set-accuracy loss for MNIST at ϵ = 0.1.

D.1 NETWORK TRAINING DETAILS

The paper trains robust classifiers with adversarial training and evaluates exact verification using a MILP verifier whose build and solve stages have distinct computational dependencies.

D.1 NETWORK TRAINING DETAILS: Adversarial strength increases from 0.01 to ϵ during the first half of training and remains at ϵ thereafter.
D.1 NETWORK TRAINING DETAILS: The experiments use Adam with learning rate 1e−4, training MNIST for 70 epochs and CIFAR for 250 epochs.
D.1 NETWORK TRAINING DETAILS: RS Loss weights and ℓ1-regularization weights are selected by line search, with one RS Loss weight shared across ReLUs.
D.2 VERIFIER OVERVIEW: The MILP verifier first builds a model by computing ReLU bounds, then solves it with a MILP solver.
D.2 VERIFIER OVERVIEW: Model-build speed depends primarily on the bound-tightening algorithm, while solve speed depends strongly on unstable-ReLU and variable counts.
D.2 VERIFIER OVERVIEW: Some solves remain slow despite few binary variables, motivating further study of other network properties affecting MILP difficulty.

E FULL EXPERIMENTAL VERIFICATION RESULTS

The full-results table reports natural-improvement, control, and “+RS” networks, together with bounds and adversarial-accuracy evaluations of robustness.

Table 7 presents full results for natural improvements, control networks, and “+RS” networks.
The table includes two upper bounds and one lower bound because true adversarial accuracy cannot be determined.
Forty-step PGD adversarial accuracy and verifier outputs provide the reported upper bounds.

F DISCUSSION ON VERIFICATION AND CERTIFICATION

Exact verification provides accurate answers but can be extremely slow, whereas certification is faster but may miss some truly robust inputs. The paper addresses this tension by co-designing training and verification, using weight sparsity and ReLU stability to accelerate exact verification while retaining exactness.

Verification and certification: Certification methods solve easier relaxations, trading some provable robustness for faster results.They may fail to certify inputs that are actually robust, but quickly find or fail to find certificates.
Verification and certification: Exact verifiers return correct robustness answers given sufficient time, but can require many hours for one input.This makes exact verification computationally difficult even for relatively small networks.
Co-design: The paper co-designs robust training with MILP-based exact verification rather than treating training and verification as separate stages.Its training procedure uses standard robust adversarial training augmented to induce weight sparsity and ReLU stability.
Co-design: Weight sparsity accelerates exact verification by reducing the number of variables in the verifier's formulation.The paper reports that sparsity-inducing methods can make verification much faster than current methods.
ReLU stability: ReLU stability reduces branching because stable ReLUs need not be considered in both active and inactive cases.The same property can also tighten certification relaxations because unstable ReLUs are identified as their primary source of overapproximation.
Broader applicability: The proposed sparsity and stability techniques are intended to remain useful beyond adversarial-robustness verification for other network properties.The paper attributes this broader applicability to the same verification-complexity mechanisms.