PaperlayerView exact revision on arXiv

Source-linked AI summary

SoK: Certified Robustness for Deep Neural Networks

Linyi Li, Tao Xie, Bo Li

arXiv:2009.04131v9cs.LGcs.CRstat.ML

TL;DR

DNNs are vulnerable to adversarial attacks, creating safety concerns and motivating certified robustness research. This SoK systematizes verification and robust training approaches, benchmarks them across datasets, and identifies their strengths, limitations, connections, and future directions.

  • Problem

    DNNs can be misled by carefully crafted adversarial examples, creating safety concerns for applications such as autonomous driving.

  • Method

    The paper develops a taxonomy and synthesis of certified robustness verification and robust training approaches, supported by a comprehensive benchmark and unified evaluation platform.

  • Results

    Certified robustness has progressed substantially, but performance remains dataset- and threat-model-dependent, with certified accuracy exceeding 94% on MNIST at radius 0.3 while remaining much lower on CIFAR-10 and ImageNet.

  • Takeaways & Limitations

    The synthesis clarifies the strengths, limitations, and fundamental connections among certified approaches while highlighting theoretical barriers, practical challenges, and future research directions.

  • Takeaways & Limitations

    Certified approaches face scalability, tightness, architecture, threat-model, and numerical-soundness limitations across verification and training methods.

Abstract

from arXiv · show

Great advances in deep neural networks (DNNs) have led to state-of-the-art performance on a wide range of tasks. However, recent studies have shown that DNNs are vulnerable to adversarial attacks, which have brought great concerns when deploying these models to safety-critical applications such as autonomous driving. Different defense approaches have been proposed against adversarial attacks, including: a) empirical defenses, which can usually be adaptively attacked again without providing robustness certification; and b) certifiably robust approaches, which consist of robustness verification providing the lower bound of robust accuracy against any attacks under certain conditions and corresponding robust training approaches. In this paper, we systematize certifiably robust approaches and related practical and theoretical implications and findings. We also provide the first comprehensive benchmark on existing robustness verification and training approaches on different datasets. In particular, we 1) provide a taxonomy for the robustness verification and training approaches, as well as summarize the methodologies for representative algorithms, 2) reveal the characteristics, strengths, limitations, and fundamental connections among these approaches, 3) discuss current research progresses, theoretical barriers, main challenges, and future directions for certifiably robust approaches for DNNs, and 4) provide an open-sourced unified platform to evaluate 20+ representative certifiably robust approaches.

I. INTRODUCTION

DNNs are vulnerable to adversarial examples, motivating certifiable approaches that verify robustness bounds and train models to improve them. This SoK systematizes these approaches, benchmarks more than 20 methods, and provides practical guidance and research directions.

  • Adversarial examples can mislead DNNs, creating safety concerns for applications such as autonomous driving.
  • Empirical defenses may be adaptively defeated, motivating robustness verification and robust training with certified guarantees under perturbation constraints.Verification provides a certified lower bound of robustness, while robust training seeks to improve that bound.
  • The SoK introduces a first-principles taxonomy covering robustness verification and robust training approaches for DNNs.It summarizes representative methodologies and reveals their characteristics, strengths, limitations, and fundamental connections.
  • The authors benchmark over 20 verification and robust training approaches across datasets and models using an open-source unified toolbox.The benchmark is intended to enable quantitative comparison and support deployment decisions.
  • The paper discusses research progress, theoretical barriers, challenges, extensions to alternative threat and system models, and future directions.
  • The SoK serves ML researchers and practitioners by combining formal problem definitions, reference implementations, benchmarks, and guidance for selecting and evaluating certified defenses.

B. Threat Model

The paper focuses on white-box evasion attacks that generate bounded perturbations to change model predictions, and formalizes robustness verification as certifying positive class margins throughout a perturbation region. It distinguishes verification by completeness and determinism, while highlighting the scalability–tightness trade-off and the role of robust training.

  • Threat model: The threat model assumes a white-box adversary that knows the target model and generates an ℓp-bounded perturbation within radius ϵ.The perturbed input must cause the model to predict a label different from the true label.
  • Verification: Robustness verification certifies a lower bound on model performance against any adversary satisfying specified perturbation constraints.Verification approaches may target threats such as ℓ∞-bounded attacks.
  • Verification categories: A verification algorithm is complete when every unverified instance is guaranteed to contain an adversarial example; otherwise, it is incomplete.Deterministic verification guarantees rejection for non-robust inputs, whereas probabilistic verification provides that guarantee with probability at least 1 − α.
  • Verification objective: Robustness certification reduces to checking whether the minimum true-class margin M(y0, y′) remains positive for every competing label within the perturbation region.If M(y0, y′) > 0 for all y′ ≠ y0, the prediction remains y0 for every permitted perturbed input.
  • Core challenge: Complete verification is NP-Complete, while incomplete verification trades tightness for tractability, creating the central scalability–tightness challenge.The paper reports that robust training approaches aim to improve the guarantees that verification can certify.

III. TAXONOMY OF CERTIFIABLY ROBUST APPROACHES

The taxonomy organizes certifiably robust approaches by verification completeness, determinism, system model, and core methodology, while characterizing them by supported threats, scalability, and tightness. Its comparison shows that tight deterministic verification remains limited to CIFAR-10-sized general DNNs, whereas larger-scale methods are looser or specialized for smoothed models.

  • Taxonomy structure: The taxonomy first separates verification into complete versus incomplete approaches and then into deterministic versus probabilistic approaches.No complete probabilistic verification approach is currently included.
  • Taxonomy structure: Verification approaches are further categorized by system model and core methodology, while robust training approaches are organized alongside their corresponding verification approaches.The taxonomy links suitable verification methods to robust training categories.
  • Comparison criteria: Table I compares verification approaches by system model, supported ℓp adversaries, scalability, and verification tightness.Supported adversaries use checkmarks to distinguish well-supported, less-tight, and unsupported cases.
  • Comparison criteria: Scalability is measured by the largest demonstrated dataset certifiable at radius ϵ ≥1/255, with ImageNet indicating greater scale than MNIST.The paper also reports best-known time complexity for verifying an arbitrary input.
  • Observed trade-off: For general DNNs, complete or tight deterministic approaches handle only CIFAR-10-sized models, while larger ImageNet-scale verification currently requires looser or smoothed-DNN approaches.Smoothed-DNN approaches reach ImageNet scale but do not yet provide nontrivial verification against ℓ∞ adversaries.

IV. ROBUSTNESS VERIFICATION APPROACHES

The paper surveys complete robustness verification methods, including solver-based, simplex, and branch-and-bound approaches, and explains how they encode or decompose neural-network verification problems. These methods provide exact guarantees but face worst-case exponential complexity, with practical scalability depending strongly on model structure and certifiability-oriented training.

  • Complete verification: Complete verification approaches typically target ℓ∞ adversaries and feed-forward ReLU networks, whose verification problems have worst-case exponential time complexity.Some approaches nevertheless verify networks with several thousand neurons in practice.
  • Solver-based verification: Solver-based methods encode affine and ReLU network operations as constraints, using SMT or MILP solvers to obtain complete verification.SMT methods generally scale only to hundreds of neurons, while MILP can handle medium-sized CIFAR-10 models when networks favor certifiability.
  • Extended simplex method: The extended simplex method iteratively detects violated ReLU constraints and splits unresolved neurons into active and inactive subproblems.Each split produces subproblems that can be solved separately under corresponding ReLU constraints.
  • Branch-and-bound: Branch-and-bound combines incomplete bounds with branching: positive lower bounds certify, non-positive upper bounds reject, and unresolved cases are subdivided.The method exploits the piecewise-linear structure of ReLU networks and is the basis of leading verification tools such as α-β-CROWN.
  • Practical implications: α-β-CROWN can verify networks with up to 10^5 neurons within several minutes when models are trained to favor certifiability.Without such specialized training, complete verification can handle up to 10^4 neurons in the reported setting.
  • Research implications: Future work must improve complete-verification scalability while addressing solver encodings, branching heuristics, and floating-point unsoundness.The paper notes that unsoundness under floating-point arithmetic can be exploited to fool verifiers.

B. Incomplete Verification via Linear Relaxation

Linear-relaxation verification replaces DNN behavior with tractable over-approximations, trading scalability against bound tightness. These approaches range from highly scalable but loose interval propagation to tighter, less scalable multi-neuron relaxations.

  • Linear relaxation framework: Linear-relaxation methods over-approximate DNN behavior using ReLU polytopes and compute bounds for each neuron before verifying the resulting region.For unstable ReLUs, the polytope is defined by linear constraints using lower and upper preactivation bounds.
  • Linear inequality methods: IBP propagates interval bounds with computation comparable to model inference, making it highly scalable but often producing trivial bounds on ImageNet.The method uses four matrix-vector products per layer and is therefore suitable for large models, despite its looseness on standard networks.
  • Linear inequality methods: IBP is usually loose for normally trained networks, but IBP-trained models can achieve certified robustness close to the best linear-relaxation approaches.The paper attributes this improvement to training specifically designed around IBP bounds.
  • Multi-neuron relaxation: Linear inequalities cannot surpass the tightness of linear-programming verification, while multi-neuron relaxations were introduced to overcome this convex barrier.Multi-neuron methods jointly relax several ReLU inputs; K-RELU and PRIMA consider up to five inputs at once.
  • Practical implications: When complete verification is too large, linear relaxation is practical; however, it cannot certify nontrivial robustness for very deep networks with 10 or more layers.IBP is the most scalable and typically loosest option, whereas multi-neuron relaxation is tighter but less scalable.
  • Research implications: Future progress requires tighter, more scalable multi-neuron relaxations, efficient constraint-selection heuristics, and improved robust training.The paper identifies both rule-based and learning-based heuristics as promising directions.

C. Incomplete Verification via SDP

SDP-based verification encodes ReLU-related quadratic constraints as a semidefinite relaxation. It can produce relatively tight incomplete certificates, but its slow solving process currently limits practical scalability.

  • SDP formulation: VERIFY formulates incomplete robustness verification as a semidefinite program with a symmetric positive-semidefinite matrix as the decision variable.The matrix elements are subject to linear constraints.
  • SDP formulation: The SDP relaxation represents ReLU activations with P = vv^T, then drops the rank-one constraint and retains P ⪰ 0.This converts the relevant constraints into linear inequalities over matrix elements.
  • Practical implications: SDP verification is incomplete but empirically tighter than linear-programming and multi-neuron relaxation approaches.Its tightness is reported to fall between those two categories.
  • Practical implications: Verifying a thousand-neuron DNN with SDP can require several hours to one day, whereas complete and linear-relaxation methods may finish within minutes.The paper therefore recommends complete verification or linear relaxation instead of SDP at the current stage.
  • Research implications: SDP scalability remains the major research challenge, motivating more efficient relaxations and specialized solvers.The paper notes that a specialized first-order solver substantially improves scalability but that further improvements are needed.

D. Incomplete Verification via Lipschitz or Curvature Bounds

Incomplete verification derives certified robustness bounds from properties such as Lipschitz constants, smooth layers, curvature, or randomized smoothing. These approaches offer efficiency or broad architectural applicability, but their guarantees depend on perturbation norm, model structure, and certification tightness.

  • Lipschitz and curvature bounds: Lipschitz-based verification bounds output-margin changes using a network’s Lipschitz constant, thereby certifying robustness within a perturbation region.The bound can be computed from weight-matrix spectral norms, although global bounds are often too loose without regularization.
  • Lipschitz and curvature bounds: Global Lipschitz verification is efficient and scalable, but generally provides nontrivial certification only against ℓ2 adversaries.Finer-grained convolutional, local, or IBP-combined analyses can tighten the bound.
  • Lipschitz and curvature bounds: Smooth-layer methods construct layers with provable small Lipschitz constants, supporting certification against ℓ2 attacks and, with ℓ∞ neurons, ℓ∞ attacks.Orthogonal layers have Lipschitz constant 1, while effective training combined with ℓ∞ neurons can achieve state-of-the-art ℓ∞ certified robustness.
  • Lipschitz and curvature bounds: Curvature-based verification bounds second-order derivatives, but it cannot be applied to ReLU networks and supports only ℓ2 adversaries.It can verify high robustness for some robustly trained models on small datasets such as MNIST.
  • Probabilistic verification: Randomized smoothing adds noise and derives probabilistic guarantees from smoothed classifiers, typically using Monte Carlo estimation and hypothesis testing.Gaussian smoothing is common for ℓ2, while uniform smoothing is reported as significantly better for ℓ1 certification.
  • Probabilistic verification: First-order information tightens smoothed-model certification most visibly for ℓ1 adversaries, while further improvements require better information, sampling, distributions, and training.The cited discussion identifies these as open research directions for randomized smoothing.
  • Probabilistic verification: Probabilistic verification is strong against ℓ1 and ℓ2 adversaries and supports arbitrary architectures, but remains loose against ℓ∞ on ImageNet and adds inference and accuracy costs.Larger smoothing variance can enlarge certified radii while hurting clean accuracy, and high-dimensional inputs have small certified ℓ∞ radii.

V. ROBUST TRAINING APPROACHES

Robust training approaches improve the guarantees that verification methods can certify, but their effectiveness depends strongly on matching the model properties favored by the verifier. This creates a need for verification methods that are less dependent on specialized architectures or training outcomes.

  • Motivation and categories: Normally trained DNNs are usually non-robust, so robust training is used to improve the robustness guarantees that verification approaches can certify.Effective attacks can find adversarial examples with almost 100% probability against normally trained models.
  • Verification–training alignment: Verification methods favor particular model properties, such as tight linear relaxations for branch-and-bound and linear-relaxation verification.Models lacking these properties can make certification substantially slower or less effective.
  • Motivation and categories: Robust training approaches are divided into regularization-based, relaxation-based, and augmentation-based categories.These approaches can also enhance the model properties required by corresponding verification methods.
  • Verification–training alignment: Models trained for one robust verification approach often perform poorly under mismatched verification because they do not inherit the verifier’s desired properties.Randomized-smoothing training may produce accurate noisy predictions but unstable neurons and loose linear relaxations.
  • Open research goals: A key research goal is efficient complete verification that can handle empirically defended or robustly trained models without relying heavily on specific model properties.Existing complete methods can verify some PGD-trained models but remain limited to small models.
  • Open research goals: Certified robustness can be improved through tighter or more training-friendly relaxations and more effective robust-training methods.The paper identifies improvements on both the verification and training sides as complementary directions.

VI. BENCHMARK, LEADERBOARD, AND IMPLICATIONS

The paper introduces an open-source toolbox for systematically benchmarking more than 20 certifiably robust approaches. Benchmark results and a leaderboard are then used to outline practical implications for deployment.

  • Benchmark and leaderboard: The open-source toolbox benchmarks 20+ certifiably robust approaches.The benchmark covers representative verification and robust training approaches.
  • Benchmark and leaderboard: Benchmark results and the leaderboard are used to outline practical implications for deploying certifiably robust DNN approaches.The section connects quantitative evaluation with deployment-oriented analysis.

A. Benchmark Evaluation

The benchmark compares certified robustness across deterministic and probabilistic verification settings, models, datasets, adversaries, and training methods. Results show strong dependence on model scale, verification–training alignment, dataset difficulty, and threat model.

  • Certified accuracy measures the fraction of test samples verified robust against the corresponding (ℓp, ϵ)-adversary.
  • Complete verification performs best on relatively small models, whereas linear-relaxation verification generally performs best on larger models.Complete methods become too slow at larger scales, while other approaches can be too loose and yield almost 0% certified accuracy.
  • CROWN-IBP-trained models achieve high certified accuracy with IBP and CROWN, showing that robust training and verification approaches must be matched.
  • Probabilistic verification: Probabilistic verification performs best under ℓ1 and ℓ2 adversaries with Neyman–Pearson-based verification, but ℓ∞ certification becomes harder as data dimension increases.
  • 94% certified accuracy has been reached on MNIST for ℓ∞ radius 0.3, while CIFAR-10 and ImageNet remain substantially more difficult.CIFAR-10 reaches around 68% at radius 2/255 and 40.39% at radius 8/255; ImageNet reaches 42.2% for ℓ2 radius 2.0 and around 38% for ℓ∞ radius 1/255.
  • Practical implications: For practical deployment, recommended verification–training combinations depend on dataset size and adversary type, while model certification requires a verification method suited to model scale.The paper presents separate guidance for improving certified robustness and evaluating or certifying existing models.

VII. EXTENSIONS AND APPLICATIONS

The paper describes extensions of certified robustness beyond the standard (ℓp, ϵ)-adversary, feed-forward networks, and image classification. It also presents a unified abstraction-based view, practical barriers, and directions toward tighter and more scalable certification.

  • Extensions to threat models: Certified robustness methods have been extended to local, other, and global evasion threat models beyond the standard (ℓp, ϵ)-adversary.
  • Extensions to system models: Verification techniques developed for feed-forward ReLU networks have been generalized to recurrent networks, transformers, generative models, and ensembles.
  • Concrete applications: Certified robustness methods have also been applied to NLP, object detection, segmentation, point clouds, and speech recognition.
  • Unified view: A unified view treats verification approaches as abstractions of DNN behavior, with branching refining abstractions and relaxations bounding behavior over perturbation regions.
  • Challenges: Verification faces theoretical and practical barriers, including scalability, floating-point soundness, and protection of robust training against training-time attacks.
  • Future directions: Future directions include scalable and tighter verification, improved robust training theory, domain knowledge integration, and real-world deployment.

APPENDIX A SCALABILITY AND TIGHTNESS MEASUREMENTS

The appendix characterizes certified verification through computational scalability and relaxation tightness. Complete methods face exponential complexity, while linear and multi-neuron relaxations trade tractability against bound tightness.

  • Scalability: Complete verification approaches have exponential time complexity O(2^lw), reflecting theoretical scalability barriers.DNN inference is characterized separately with time complexity O(lw^2).
  • Threat-model geometry: An (ℓp, ϵ)-adversary searches an ℓp-bounded region centered at clean input x0, with ℓ1, ℓ2, and ℓ∞ regions differing geometrically.
  • ReLU relaxations: The tightest single-neuron ReLU polytope provides a tighter relaxation than looser single-neuron and alternative linear bounds.
  • Multi-neuron relaxation: Multi-neuron convex relaxation gives a tighter upper bound for z than single-ReLU polytope relaxation.
  • Linear bounds: FAST-LIN uses a parallel lower-bound line, whereas CROWN, DEEPPOLY, FROWN, and α-CROWN use adjustable or optimized lower-bound slopes.
  • Bound propagation: Layer-wise linear bounds are propagated through affine mappings and ReLU activations to bound the final model output over the perturbation region.

APPENDIX D ILLUSTRATION OF ROBUST TRAINING APPROACHES

The appendix links robust training objectives to the verification procedures used to certify models. Training can promote neuron stability, noise robustness, or certified performance, while the benchmark evaluates representative approaches under controlled time and model settings.

  • Regularization-based training: Regularization-based training can increase ReLU neuron stability, reducing the branching burden relevant to complete verification.
  • Smoothing-based training: Randomized-smoothing verification motivates noisy-input augmentation and consistency regularization during training.
  • Training combinations: Strategic regularization combined with augmentation and ensembles achieves state-of-the-art certified robustness against ℓ2 adversaries.
  • Experimental setup: The toolkit integrates authors’ implementations when available and otherwise optimizes implementations to match reported performance.
  • Benchmark design: The deterministic evaluation compares seven CIFAR-10 DNNs ranging from 50 to about 200,000 neurons under PGD and CROWN-IBP training.
  • Evaluation protocol: Evaluation samples 100 test examples per dataset and limits verification to 60 seconds per instance, counting timeouts as not verified.
  • Reported results: Table III reports certified accuracy for deterministic approaches, with additional results covering certified radius, running time, and MNIST.

B. Comparison of Probabilistic Verification

The section compares probabilistic certification for smoothed DNNs, including a double-sampling extension that uses information from an additional smoothing distribution. Under the stated evaluation protocol, this method achieves higher certified accuracy than classical Neyman–Pearson certification against ℓ∞ perturbations.

  • Evaluation protocol: The evaluation uses ResNet-110 and Wide ResNet 40-2, with 1,000 samples for top-label selection and 100,000 for certification.Certified accuracy is reported across radii, alongside benign accuracy, following the standard protocol.
  • Comparison design: The comparison includes probabilistic verification with different smoothing distributions and robust training approaches, with comparable values organized within groups in the probabilistic-results table.The models are trained and smoothed under varied settings, while comparisons are made within the table’s specified groups.
  • Method: The proposed extension samples smoothed-prediction statistics under the original distribution P and an additional distribution Q with a different variance.It therefore uses prediction-probability information under Q in addition to sampling information under P.
  • Results: The proposed method yields significantly higher certified accuracy for all evaluated models against ℓ∞-bounded perturbations.The reported improvement extends the tighter-certification finding beyond ℓ1 and ℓ2 adversaries to ℓ∞ adversaries.
Loading 2009.04131v9…