PaperlayerView exact revision on arXiv

Source-linked AI summary

Towards Fast Computation of Certified Robustness for ReLU Networks

Tsui-Wei Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Duane Boning, Inderjit S. Dhillon, Luca Daniel

arXiv:1804.09699v4stat.MLcs.CRcs.CVcs.LG

TL;DR

ReLU-network robustness verification is NP-complete, and existing certified lower bounds can be too slow or too loose. The paper develops Fast-Lin and Fast-Lip, which exploit ReLU structure to compute certified lower bounds efficiently. The methods achieve comparable quality to exact or LP-based approaches with substantially lower runtime, while approximate ℓ1 robustness verification remains hard.

  • Problem

    Exact ReLU-network robustness verification is NP-complete, while available certified lower-bound methods can be time-consuming or too loose to be useful.

  • Method

    Fast-Lin bounds ReLU units with linear functions, while Fast-Lip bounds the network's local Lipschitz constant to obtain certified lower bounds.

  • Results

    Fast-Lin and Fast-Lip achieve similar quality to LP-based methods with 33–14,000 times greater speedups, and are over 10,000 times faster than Reluplex while remaining within a 2–3X gap on small networks.

  • Takeaways & Limitations

    The methods provide practical certified robustness bounds for ReLU networks up to 7 layers or more than 10,000 neurons, while exact approximation remains computationally hard.

  • Takeaways & Limitations

    The activation-bound formulation assumes inputs lie in a bounded ℓp-norm perturbation ball and uses bounded pre-ReLU activation intervals.

Abstract

from arXiv · show

Verifying the robustness property of a general Rectified Linear Unit (ReLU) network is an NP-complete problem [Katz, Barrett, Dill, Julian and Kochenderfer CAV17]. Although finding the exact minimum adversarial distortion is hard, giving a certified lower bound of the minimum distortion is possible. Current available methods of computing such a bound are either time-consuming or delivering low quality bounds that are too loose to be useful. In this paper, we exploit the special structure of ReLU networks and provide two computationally efficient algorithms Fast-Lin and Fast-Lip that are able to certify non-trivial lower bounds of minimum distortions, by bounding the ReLU units with appropriate linear functions Fast-Lin, or by bounding the local Lipschitz constant Fast-Lip. Experiments show that (1) our proposed methods deliver bounds close to (the gap is 2-3X) exact minimum distortion found by Reluplex in small MNIST networks while our algorithms are more than 10,000 times faster; (2) our methods deliver similar quality of bounds (the gap is within 35% and usually around 10%; sometimes our bounds are even better) for larger networks compared to the methods based on solving linear programming problems but our algorithms are 33-14,000 times faster; (3) our method is capable of solving large MNIST and CIFAR networks up to 7 layers with more than 10,000 neurons within tens of seconds on a single CPU core. In addition, we show that, in fact, there is no polynomial time algorithm that can approximately find the minimum $\ell_1$ adversarial distortion of a ReLU network with a $0.99\ln n$ approximation ratio unless $\mathsf{NP}$=$\mathsf{P}$, where $n$ is the number of neurons in the network.

1. Introduction

Verifying ReLU-network robustness is computationally hard, while existing certified bounds are either loose or costly. The paper introduces Fast-Lin and Fast-Lip to compute tighter certified lower bounds efficiently.

  • Motivation: Adversarial examples threaten DNN applications in mission-critical settings, while existing defenses lack reliable theoretical robustness guarantees.Examples include security cameras, self-driving cars, and aircraft control systems.
  • Verification challenge: Robustness verification seeks the largest neighborhood around x0 that cannot change the classifier decision, but exact verification is NP-complete.Reluplex uses global optimization and bisection but is computationally infeasible even for small MNIST classifiers.
  • Certified bounds: Certified lower bounds guarantee robustness within a perturbation radius, but prior approaches are either restricted, uncertified, or potentially trivial.CLEVER applies to large networks but estimates the bound without certificates; the desired bound should be non-trivial and close to r0.
  • Paper approach: Fast-Lin and Fast-Lip exploit ReLU structure through linear unit approximations and local Lipschitz bounds to compute tighter, guaranteed robustness lower bounds.The methods are designed to improve substantially over loose operator-norm-based bounds.
  • Reported contribution: The proposed methods are at least four orders of magnitude faster than exact distortion search and can bound networks with up to 7 layers or over 10,000 neurons within a minute.Their bounds are reported as closer to adversarial-example upper bounds than per-layer operator-norm bounds.

2. Background and related work

Prior verification methods provide exact guarantees but scale poorly, whereas norm-based bounds are efficient but often too loose. The paper also frames approximate robustness verification as a computational-hardness question.

  • Exact verification: MILP, Reluplex, and Planet encode ReLU activation states to perform formal verification and can find exact minimum adversarial distortions.Their NP-hard underlying problem limits these approaches to very small networks.
  • Efficient bounds: Operator-norm products provide lower bounds for ReLU networks, but the bounds are usually too loose to be useful in practice.Local-Lipschitz approaches can be tighter but earlier work required one hidden layer and continuously differentiable activations.
  • Approximation hardness: The paper asks whether polynomial-time algorithms can produce certified approximation guarantees for minimum adversarial distortion.The approximation ratio is allowed to increase with the number of neurons n.
  • Complexity context: Tensor-rank hardness results illustrate that NP-hardness can be strengthened beyond ruling out polynomial-time algorithms to exclude sub-exponential algorithms under stronger assumptions.The discussion distinguishes NP ≠ P from the Exponential Time Hypothesis.

3. Robustness guarantees for ReLU networks

The section establishes both a hardness boundary for approximating minimum adversarial distortion and efficient certified lower bounds for ReLU networks. Fast-Lin derives analytic output bounds from linear ReLU approximations, while Fast-Lip bounds the local Lipschitz constant.

  • Hardness of approximation: Unless P = NP, no polynomial-time algorithm gives a (1 −o(1)) ln n-approximation for ℓ1 ReLU robustness verification with n neurons.The result follows from a reduction based on SET-COVER inapproximability.
  • Activation patterns: ReLU neurons are partitioned by activation status into always-active, always-inactive, and potentially switching categories under an ℓp perturbation ball.These categories determine which neurons can be removed and which require linear upper and lower bounds.
  • Fast-Lin: Fast-Lin replaces uncertain ReLU activations with sign-aware linear upper and lower bounds to derive explicit bounds on network outputs.The construction uses activation matrices and equivalent bias terms recursively across layers.
  • Certified bounds: Theorem 3.5 and Corollary 3.7 provide explicit closed-form output bounds and analytic certified lower bounds for general ℓp perturbations.These bounds are computed without optimization solvers, enabling efficient robustness certification.
  • Efficiency: Computing the bounds has polynomial-time complexity, with the main cost being formation of A(0), comparable to forward propagation.This contrasts with SMT- and MIO-based approaches whose time complexity is exponential.
  • Fast-Lip: Fast-Lip computes certified lower bounds by upper bounding the local Lipschitz constant using activation-pattern matrices.The method rewrites each layer using a diagonal matrix encoding neuron activation status.

4. Experiments

Experiments compare Fast-Lin and Fast-Lip with optimization, verification, attack, and estimation methods across toy and large networks. The proposed certificates remain close to stronger references while substantially reducing computation time and can evaluate defended models.

  • Experimental setup: Fast-Lin and Fast-Lip are evaluated against LP, LP-Full, Reluplex, Op-norm, CLEVER, and attack methods on toy and large networks.The experiments cover 2–3-layer toy MNIST networks and larger networks with 2–7 layers and 1024 or 2048 nodes per layer.
  • Results: 2–3-layer toy MNIST networks show certified bounds within 2–3X of Reluplex’s exact minimum distortion, with more than 10,000× speedup.Reluplex is feasible only for networks with fewer than 100 MNIST neurons.
  • Results: Fast-Lin and Fast-Lip achieve gaps within 35%, usually around 10%, of LP-based bounds while running 33–14,000 times faster.The LP-based methods are infeasible for networks with more than 4,000 neurons.
  • Results: For larger and deeper networks, the proposed methods still provide non-trivial lower bounds relative to attack-derived upper bounds.The large-network comparisons include models with 2–7 layers and 1024 or 2048 nodes per layer.
  • Defended networks: For defended networks, especially adversarially trained models, the methods produce significantly larger bounds and can evaluate defending techniques.Table 2 compares lower bounds for models using defensive distillation and adversarial training.

5. Conclusions

The paper concludes that Fast-Lin and Fast-Lip provide efficient certified robustness bounds for ReLU networks, while its hardness analysis addresses approximate minimum-distortion computation. The methods achieve similar quality to LP-based approaches at much lower cost, and future work targets convolutional layers and larger networks.

  • Contributions: Fast-Lin and Fast-Lip exploit ReLU structure to compute certified lower bounds for robustness verification.Fast-Lin uses linear approximation of ReLU units, while Fast-Lip bounds the local Lipschitz constant.
  • Conclusions: The algorithms are at least two orders of magnitude faster than LP-based methods while obtaining similar-quality solutions.Their bounds are also much better than previously proposed operator-norm-based bounds.
  • Future work: Future work includes extending the algorithms to convolutional layers and evaluating large networks such as ResNet on ImageNet.The current methods compute bounds layer by layer without solving integer or linear programming problems or their duals.
  • Hardness analysis: The hardness analysis shows that approximate robustness verification can be connected to approximate set cover through lower-bound and upper-bound transformations.The reduction framework defines ROBUST-NET and relates an approximate oracle’s output to a certified lower bound.
  • Hardness analysis: ROBUST-NET(R) asks whether a perturbation within ℓ1 radius r can change the network output, while approximate ROBUST-NET distinguishes radius r from αr.The real-input problem uses F(x) ≤ 0 and asks whether some y with ∥x − y∥1 ≤ r has F(y) > 0.
  • Hardness analysis: A polynomial-time algorithm for approximate ROBUST-NET would yield a lower bound with a guaranteed approximation ratio, which is the target of the hardness argument.Dividing the approximate oracle’s upper-bound answer by α produces a certified lower bound.

A.2. Background of the PCP theorem

The PCP theorem is presented as the foundational tool for proving computational hardness of approximation. Its formulation uses tests with constant-size queries and distinguishes satisfiable formulas from unsatisfiable ones through completeness and soundness.

  • PCP theorem: The PCP theorem is described as a cornerstone of computational hardness-of-approximation theory.The section places PCP reductions in the context of proving inapproximability results.
  • PCP theorem: Given a SAT formula, the theorem constructs a set of tests in polynomial time, with each test querying a constant number of proof bits.Each test accepts or rejects based on the queried bits.
  • Completeness and soundness: In the completeness case, satisfiability implies that some proof makes all tests accept the formula.This is the theorem’s positive-case guarantee.
  • Completeness and soundness: In the soundness case, unsatisfiability prevents any proof from making the tests accept beyond the theorem’s stated threshold.The supplied statement introduces this negative-case guarantee but is truncated before its numerical threshold.

A.3. Warm-up

The warm-up reduction encodes SET-COVER choices as binary inputs to a ReLU network. Completeness and soundness transfer cover-size conditions into perturbation-radius conditions, yielding logarithmic approximation hardness for ROBUST-NET(B).

  • Reduction: The boolean-input hardness proof reduces SET-COVER to ROBUST-NET(B), using a construction that is intended to be simpler than the real-input case.ROBUST-NET(B) uses ReLU networks with binary inputs and outputs.
  • Network construction: The reduction creates one input node per set, one hidden node per universe element, and an output node connected through the hidden nodes.Connections encode whether a set contains a given element.
  • Network construction: Each hidden activation indicates whether at least one selected set covers its corresponding universe element.The construction uses the indicator sets T_i and a thresholded sum of selected-set inputs.
  • Network semantics: A binary input y represents the selected sets through y_j = 1, and the output is positive exactly when the selected sets form a set cover.The number of selected sets equals the ℓ1 distance from the all-zero input.
  • Completeness and soundness: Completeness maps a set cover of size at most r to a perturbation within ℓ1 radius r that makes the network output positive.This establishes the YES direction of the reduction.
  • Completeness and soundness: Soundness maps the absence of a cover of size at most αr to non-positivity throughout the radius-αr neighborhood.Together with the approximation-hardness theorem, these claims complete the reduction.

A.4. Main result

The proof reduces set cover to ℓ1 robustness, showing that sufficiently small adversarial perturbations correspond to set covers and establishing logarithmic approximation hardness.

  • Unless NP = P, no polynomial-time algorithm gives a (1 − o(1)) ln n-approximation for ROBUST-NET(R) with n hidden nodes.
  • The construction creates input nodes for sets, hidden nodes for set activations and covered elements, and an output node aggregating element nodes.
  • A set cover of size at most r yields an adversarial point within ℓ1 distance r that makes the output positive.
  • If every set cover has size greater than αr, perturbations of size at most αr(1 − 1/d) cannot make the output positive.
  • Assuming ETH, no 2^o(n^c)-time algorithm achieves the same approximation ratio for ROBUST-NET.

B. Proof of Theorem 3.5

The proof constructs explicit layer-wise upper and lower functions by propagating linear ReLU bounds through the network, using weight signs to select appropriate bounds.

  • Given pre-ReLU activation bounds, the proof derives explicit upper and lower functions for every output of an m-layer ReLU network.
  • The upper-bound derivation recursively rewrites layer computations as matrix-vector products and propagates the bound backward through preceding layers.
  • For uncertain ReLUs, linear upper and lower bounds use the same slope, allowing shared matrix computations for both network bounds.
  • Weight signs determine whether each neuron's upper or lower linear approximation contributes to the resulting output bound.
  • The lower-bound construction follows the upper-bound procedure while replacing the corresponding coefficient and bias terms for negative weights.

C. Proof of Corollary 3.7

The proof converts perturbations around x0 into normalized variables and uses dual-norm relationships to derive the certified lower-bound expression.

  • The variable substitution y := x − x0 transforms perturbations into normalized points satisfying y ∈ B_p(0, 1).
  • The derivation replaces the relevant maximization term with its dual-norm expression, using the fact that ℓq is dual to ℓp.
  • A common matrix term is isolated during the derivation to obtain the final certified-bound formula.

D. Algorithms

The paper presents Fast-Lin and Fast-Lip as complete procedures: Fast-Lin propagates linear ReLU bounds, while Fast-Lip bounds a local Lipschitz constant.

  • Fast-Lin: Fast-Lin computes layer-wise lower and upper ReLU bounds and uses binary search on ε to return a certified lower bound βL.
  • Fast-Lin: Fast-Lin constructs diagonal slope matrices from layer bounds and recursively propagates affine coefficients through the network.
  • Fast-Lip: Fast-Lip replaces the final-layer weights with a row vector, propagates gradient bounds, and returns a lower bound based on the resulting local Lipschitz estimate.
  • Fast-Lip: The gradient-norm construction separates always-active and uncertain neurons before applying norm subadditivity.
  • Fast-Lip: Including all uncertain neurons yields an applicable Lipschitz upper bound but can make the resulting robustness certificate less tight.

F.1. Methods

The paper compares Fast-Lin and Fast-Lip with exact, optimization-based, attack-based, and Lipschitz-based robustness methods. The proposed methods exploit ReLU structure to provide certified bounds efficiently, with experiments covering networks up to seven layers and over 10,000 neurons.

  • Proposed methods: Fast-Lin directly bounds network outputs using linear upper and lower bounds for ReLU units.It computes hidden-layer bounds through linear ReLU approximations.
  • Proposed methods: Fast-Lip computes certified robustness lower bounds by bounding the network’s local Lipschitz constant.Unlike global operator-norm bounds, it uses local network behavior.
  • Compared methods: Reluplex finds the true minimum adversarial distortion but is computationally expensive and limited to small networks.It uses satisfiability modulo theory with ReLU-specific constraints.
  • Compared methods: LP and LP-Full provide relaxed lower bounds by solving linear programming problems, with LP-Full solving relaxed problems at every layer.The LP variants are used as baselines for Fast-Lin and Fast-Lip.
  • Compared methods: CLEVER estimates a lower bound through local Lipschitz estimation but does not provide certification.Attack methods instead provide valid upper bounds from successful adversarial examples.
  • Experimental setup: Experiments evaluate MNIST and CIFAR MLPs with up to seven layers or over 10,000 hidden neurons in single-threaded CPU settings.The implementation uses Python with NumPy and Numba, while LP baselines use Gurobi.

F.3. Discussions

Experiments show that Fast-Lin and Fast-Lip provide useful certified bounds across small and large networks while substantially reducing computation. The methods also quantify robustness changes from defensive training techniques.

  • Small networks: Fast-Lin’s lower bounds are within 2–3X of Reluplex’s true minimum distortion on small MNIST networks.Reluplex could be used only for two- and three-layer networks with 20 hidden neurons per layer.
  • Large networks: Fast-Lin and Fast-Lip are significantly faster than LP on larger networks and can verify networks that LP cannot feasibly solve.Fast-Lin remains close to LP on smaller models, while Fast-Lip can outperform it in some shallow p = 1 settings.
  • Large networks: Fast-Lin scales better than Fast-Lip in deeper networks, where uncertain activations make Fast-Lip more pessimistic.Fast-Lip nevertheless outperforms the global operator-norm bound as depth increases.
  • Defensive techniques: Both defensive distillation and adversarial training increase computed robustness lower bounds, with adversarial training significantly more effective.Fast-Lin’s bounds are close to the target robustness guarantee ϵ = 0.3.
  • Table F.1: Table F.1 compares certified bounds, estimated bounds, exact distortion, and attack upper bounds on small two- and three-layer MNIST networks.Its purpose is to assess closeness to Reluplex while contrasting computationally expensive alternatives.
  • Table F.2: Table F.2 compares lower and upper bounds on two- to seven-layer networks with 1,024 or 2,048 nodes per layer.LP-Full and Reluplex are computationally infeasible for the reported larger networks.
Loading 1804.09699v4…