SoK: Certified Robustness for Deep Neural Networks

I Introduction

Machine learning (ML) techniques, especially deep neural networks (DNNs), have been widely adopted in various applications, such as image classification and natural language processing . However, despite their wide applications, both traditional ML models and DNNs are shown vulnerable to adversarial evasion attacks where carefully crafted adversarial examples — inputs with adversarial perturbations — could mislead ML models to make arbitrarily incorrect predictions . The existence of adversarial attacks leads to great safety concerns for DNN-based applications, especially in safety-critical scenarios such as autonomous driving .

To defend against such attacks, there are several works proposed to empirically improve the robustness of DNNs . However, many of such defenses can be adaptively attacked again by sophisticated attackers . The everlasting competition between attackers and defenders motivates studies on the certifiably robust approaches for DNNs, which include both robustness verification and robust training approaches . The robustness verification approaches aim to evaluate DNN robustness by providing a theoretically certified lower bound of robustness under certain perturbation constraints; the corresponding robust training approaches aim to train DNNs to improve such lower bound.

In this paper, we aim to provide a taxonomy for existing certifiably robust approaches (i.e., robustness verification and robust training approaches) from the first principle, as well as a comprehensive benchmark on different datasets and models to enable the quantitative comparison for the community. Existing surveys discuss general attacks and defenses for traditional ML models and DNNs , but they mainly focus on empirical defenses without guarantees or some specific verification approaches. To the best of our knowledge, this is the first systematic taxonomy for the fast-developing certifiably robust approaches on DNNs against evasion attacks. The taxonomy reveals characteristics, strengths, limitations, and fundamental connections among these approaches.

To provide quantitative analysis for existing certifiably robust approaches, we develop an open-source unified toolbox for representative verification and training approaches. We benchmark over 20 verification and robust training approaches. As far as we know, it is the first large-scale benchmark for the certified robustness of DNNs. Based on the taxonomy, analysis, and benchmark of existing approaches, we further provide discussion and analysis on current research progresses, theoretical barriers, and several promising future directions. We also outline how to extend these approaches to alternative threat models and system models along with their applications.

This SoK is intended for both ML experts, who aim to develop and improve certifiably robust ML approaches, as well as practical users with a focus on applying certifiably robust approaches to different real-world ML applications. For ML experts, this SoK provides (1) systematic taxonomy to contextualize their works, (2) detailed explanation and analysis/comparison for representative certifiably robust approaches, and (3) discussion of research implications, including limitations, challenges, and future directions. For practical users, the SoK provides (1) formal problem definition of robustness verification, (2) comprehensive benchmark and reference implementations of representative approaches to ease the deployment, and (3) practical implications on how to select the most suitable defenses and how to evaluate existing defenses using certifiably robust approaches.

In taxonomizing and analyzing certifiably robust approaches for DNNs, we make the following contributions:

We provide a general problem definition for the robustness verification problem and the first systematic taxonomy of certifiably robust approaches for DNNs (Section III), including the robustness verification approaches (Section IV), and robust training approaches (Section V).

We conduct extensive quantitative comparisons The benchmark website with open-source toolbox, including full results are available at https://sokcertifiedrobustness.github.io.for different state-of-the-art approaches on robustness verification and robust training, leading to a benchmark and leaderboard, from which we summarize practical implications for deploying certifiably robust approaches (Section VI).

We provide an open-source unified evaluation toolbox for over $20$ verification and training approaches, which we believe will facilitate the development and evaluation of research on certified robustness for DNNs.

We discuss and analyze current research progresses, theoretical barriers, challenges, extensions, and further provide several potential future research directions (Sections VII and VIII).

II Preliminaries and Problem Setup

We focus on the certified robustness of DNNs for classification tasks for brevity and ease of exposition. Extensions to other system models and other tasks are discussed in Section VII.

An $l$-layer feed-forward ReLU network $f_{\theta}$ is defined as such:

In Table I, the “System Model” column lists some other system models which we will define when illustrating their corresponding verification approaches in Section IV.

II-B Threat Model

II-C Robustness Verification and Robust Training

We can also categorize the verification approaches into deterministic verification and probabilistic verification. When the given input is non-robust against the attack, deterministic verification is guaranteed to output “not verified”; and the probabilistic verification is guaranteed to output “not verified” with a certain probability (e.g., $99.9\%$) where the randomness is independent of the input. Formal definitions are as follows.

If we view “certifying a truly robust instance” as the true positive, then a robustness verification approach produces false positives with small (probabilistic) or zero (deterministic) probability, and complete verification produces no false negatives. If the verification cannot certify an instance, it is possible that either the instance is not robust or the verification approach is too loose to certify it. We can also view robustness verification from optimization perspective.

Intuitively, 1 searches for the minimum margin between the model confidence for the true class $y_{0}$ and any other class $y^{\prime}$. For any $y^{\prime}\neq y_{0}$, if we can certify ${\mathcal{M}}(y_{0},y^{\prime})>0$, the margin $f_{\theta}(x)_{y_{0}}-f_{\theta}(x)_{y^{\prime}}$ is always positive. Since the model will predict the class with the highest confidence, this means for any possible perturbed input $x\in B_{p,\epsilon}(x_{0})$, the predicted class is always $y_{0}$, and therefore the robustness is certified. Figure 1(b) illustrates this process.

The robustness verification then boils down to deciding whether ${\mathcal{M}}(y_{0},y^{\prime})>0$. If a procedure exactly solves 1, the corresponding verification approach is complete. If a procedure conservatively provides a lower bound of ${\mathcal{M}}$, the corresponding verification approach is usually incomplete.

Although complete verification sounds attractive, it is NP-Complete . This intrinsic barrier, which we identify as scalability challenge, impedes complete verification approaches from scaling up to common DNN sizes. To overcome this scalability challenge, incomplete verification is studied, aiming to solve the relaxed problem, i.e., computing the lower bound of ${\mathcal{M}}$ which is more tractable. However, the relaxations in existing approaches are typically too loose, which induces another problem identified as the tightness challenge. For example, the widely-used linear relaxations are shown significantly looser than complete verification in practice . Theoretically, if complete verification can certify robustness radius $\epsilon_{0}$, unless $\textsf{NP}=\textsf{P}$, there is no polynomial-time verification that can guarantee a constant fraction between its certified robustness radius and $\epsilon_{0}$ . The trade-off between scalability and tightness, i.e., either scalability or tightness can be achieved but not both, constitutes the main obstacle for robustness verification.

Robust training. Given the scalability and tightness challenges, vanilla DNNs are challenging to verify, where verification approaches either need a long running time or output trivial bounds. To enhance the certifiability, many robust training approaches are proposed, which are typically related to or derived from corresponding verification by optimizing verification-inspired regularization terms or injecting specific data augmentation during training. In practice, after robust training, the model usually achieves high certified robustness. Thus, robust training is a strong complement to robustness verification approaches.

Relationship with empirical attacks and defenses. Towards evaluating and improving DNN robustness, another active line of research is attacks and empirical defenses. Strong white-box attacks, such as CW attack , PGD attack , and AutoAttack , are widely used to evaluate DNN robustness (e.g., ). To improve model robustness against these attacks, many empirical defenses are proposed, such as adversarial training and TRADES . As illustrated in Figure 2, both attacks and verification approaches can be used to evaluate DNN robustness, but verification approaches can provide robustness guarantees against any possible future attacks; both empirical defenses and robust training approaches can improve DNN robustness, but empirical defenses aim to improve robustness against existing attacks and robust training approaches aim to improve robustness guarantees. We note that: (1) The strongest attack (which always discovers adversarial example if exists) is the strongest verification (complete verification). For robustness evaluation, attack and verification can be viewed as approaching from two sides (over-estimation and under-estimation) to the same goal (precise evaluation). (2) Complete verification approaches can be used to evaluate and compare empirical defenses on small models (not on large models due to scalability challenges). In practice, models trained with strong empirical defenses can be certified to have high robustness by complete verification . In contrast, most incomplete verification cannot certify high robustness for empirically defended models. More discussion is in Section V.

III Taxonomy of Certifiably Robust Approaches

In this section, we provide a comprehensive taxonomy of existing robustness verification and robust training approaches (Figure 3), and characterize their properties (Table I).

Taxonomy of robustness verification and robust training. In Figure 3, we present a taxonomy of existing robustness verification and robust training approaches. In the taxonomy, the first-level is “complete vs. incomplete”, and the second-level is “deterministic vs. probabilistic”. These concepts are as defined in Section II-A. Note that there is no complete and probabilistic verification approach yet. In the third-level, we categorize verification approaches based on the system model. Under the third level, we categorize verification approaches by their core methodologies. We will illustrate verification approaches in detail in Section IV. The robust training approaches are shown in orange. Based on their core methodologies, there are three categories: regularization-based, relaxation-based, and augmentation-based approaches. We will illustrate robust training approaches in detail in Section V.

IV Robustness Verification Approaches

We illustrate representative verification approaches in this section: complete verification (Section IV-A); incomplete verification, including linear relaxation-based (Section IV-B), SDP (Section IV-C), Lipschitz-/curvature-based (Section IV-D), and probabilistic approaches (Section IV-E). We conclude each subsection by highlighting the implications. We summarize practical and research implications in Sections VI-C and VIII respectively.

When a neuron $z$ is stable, it serves as a linear mapping $x\mapsto 0$ (inactive neuron) or $x\mapsto x$ (active neuron).

Another way is to encode the verification problem as a mixed-integer linear programming (MILP) problem. In MILP, the constraints are linear inequalities and the objective is a linear function. However, different from linear programming (LP), in MILP we can constrain some variables to take only integer values instead of real numbers. This additional expressive power allows MILP constraints to encode the non-linear ReLU operations and the whole DNN model . Thus, the verification problem can be precisely encoded as an MILP problem. By leveraging efficient MILP solvers such as Gurobi , MILP-based verification is feasible on medium-sized CIFAR-10 models if the model is specifically trained to favor certifiability . However, the naturally trained or empirically defended DNNs are still hard to verify by these approaches even on MNIST .

IV-A2 Extended Simplex Method [23, 47]

The DNN model is composed of affine transformations and ReLU operations which correspond to linear constraints and ReLU constraints respectively. When there are only linear constraints, the verification problem is a linear programming problem and can be effectively solved by the simplex method . In , the simplex method is extended to handle ReLU constraints. The core idea is to iteratively check whether the ReLU constraints are violated and fix them. If the violation cannot be easily fixed, we split the neuron into active and inactive and solve subproblems respectively.

IV-A3 Branch-and-Bound [48, 49, 50, 52, 53, 54, 37, 55, 73, 57, 26, 58, 60]

IV-B Incomplete Verification via Linear Relaxation

Due to the scalability barrier of complete verification, many incomplete verification approaches based on relaxations are proposed. Among them, linear relaxations are well studied. This category of verification approaches runs much faster and many can scale up to large ResNet models on Tiny ImageNet, which contain around $10^{5}$ neurons .

Linear relaxation based approaches rely on ReLU polytope, which we define below and illustrated in App. B-B.

These constraints define a region called ReLU polytope.

When both $l_{i,j}$ and $u_{i,j}$ are tight, the polytope is the tightest convex hull for this neuron. For stable ReLU, linear constraint $z_{i,j}=0$ or $z_{i,j}=\hat{z}_{i,j}$ defines its linear relaxation.

In general, all linear relaxation based approaches require computing $l_{i,j}$ and $u_{i,j}$ (see Definition 5) for each neuron $z_{i,j}$, then they compute an over-approximation bound ${\mathcal{S}}$ for the region $f_{\theta}\left(B_{p,\epsilon}(x_{0})\right)\mathrel{\mathop{\mathchar 58\relax}}=\{f_{\theta}(x)\mathrel{\mathop{\mathchar 58\relax}}\,x\in B_{p,\epsilon}(x_{0})\}$, i.e., ${\mathcal{S}}\supseteq f_{\theta}\left(B_{p,\epsilon}(x_{0})\right)$. ${\mathcal{S}}$ is described by linear constraints so that it is easy to verify whether all points in ${\mathcal{S}}$ lead to the true class $y_{0}$. If it is true, the region $f_{\theta}\left(B_{p,\epsilon}(x_{0})\right)$ is robust.

Based on Definition 5, we can directly use the polytope shown in Figure 6(a) in App. B-B as the relaxation for verification, which results in the approach named LP-full . In LP-full, $l$ and $u$ are computed layer by layer, the polytope relaxation (Definition 5) is then applied for each ReLU neuron, and finally, the verification is performed by solving the resulting linear programming (LP) problem. Due to the relaxation, we obtain a lower bound of ${\mathcal{M}}(y_{0},y^{\prime})$ in 1. Even though LPs can be solved in polynomial time, in practice, solving LP is still expensive. Applying LP-full on a typical model on CIFAR-10 for verifying a single instance takes several hours to several days . Moreover, although LP-full is the tightest verification using single neuron linear relaxations, compared with complete verification, the certified robustness radius $\epsilon$ is usually $1.5-5$ times smaller, which indicates the intrinsic tightness barrier of linear relaxations.

IV-B2 Linear Inequality [66, 69, 70, 61, 62, 63, 67, 64, 25, 39, 27, 71, 65, 38]

To circumvent solving expensive LP, further relaxations are applied, which can be divided into interval bound propagation (IBP), polyhedra abstraction, zonotope abstraction, and duality-based approaches.

Inteval bound propagation (IBP). A more straightforward and efficient but much looser approach comes from directly propagating $l$ and $u$ defined in Equation 2 through the layers of the given DNN model. Given perturbed input region $B_{p,\epsilon}(x_{0})$, for the first layer, we have $z_{1}=x\in[x_{0}-\epsilon,x_{0}+\epsilon]$. We let $[l_{1},u_{1}]$ to represent this numerical interval for the first layer $z_{1}$. Then, we derive $[l_{i+1},\,u_{i+1}]$ for layer $z_{i+1}$ from $[l_{i},\,u_{i}]$: If $l_{k}\leq z_{k}\leq u_{k}$, based on $\hat{z}_{k+1}={\bm{W}}_{k}z_{k}+b_{k}$, $\hat{z}_{k+1}$ can be bounded by $\hat{l}_{k+1}\leq\hat{z}_{k+1}\leq\hat{u}_{k+1}$ where

Through each layer, this bound propagation performs only four matrix-vector products, which are in the same order of model inference. As a result, the approach is very scalable for verifying large models on ImageNet, but on ImageNet it yields trivial bounds due to its looseness. The approach is called IBP or interval arithmetic .

As we will discuss in Section V, though for normal DNNs, IBP is usually loose. For the models that are specifically trained with IBP, IBP can verify close-to-best certified robustness among linear-relaxation-based approaches. Some work conjectures that IBP bound, though loose, is smoother than other linear relaxations and thus more suitable for training.

Polyhedra abstraction. The polyhedra abstraction based verification approaches, such as Fast-Lin , CROWN , and DeepPoly , replace the two lower bounds in the ReLU polytope shown in Equation 3 by a single lower bound, resulting in one lower and one upper bound for each neuron respectively. The idea is illustrated in Figures 6(b), 6(c) and 6(d) in App. B-B. The advantage of using a single linear lower bound is that: (1) the linear bounds can be propagated through layers efficiently instead of solving LP problem—the verification is more scalable than LP; and (2) linear bounds maintain interactions between different components to some degree—the verification is typically tighter than IBP. We call these approaches “polyhedra abstraction based” approaches since they essentially compute polyhedra domain abstraction interpretation for DNNs. We defer technical details along with the illustration of zonotope abstraction and duality-based approaches to App. C.

For all linear inequality based verification approaches, Salman et al prove the convex barrier: these approaches cannot be tighter than linear programming based approaches (introduced in Section IV-B1).

IV-B3 Multi-Neuron Relaxation [72, 73, 24, 74]

IV-C Incomplete Verification via SDP

Semidefinite programming (SDP) can be applied for incomplete verification: Verify formulates the robustness verification as an SDP problem, which is a convex optimization problem, where the decision variable is a symmetric and semi-positive matrix whose elements can be linearly constrained. The key formulation in Verify is

IV-D Incomplete Verification via Lipschitz or Curvature Bounds

Some verification approaches use the Lipschitz bound or curvature bound of DNN function $f_{\theta}$ to verify its robustness.

We can lower bound $f_{\theta}(x)_{y_{0}}-f_{\theta}(x)_{y^{\prime}}$ for any $x\in B_{p,\epsilon}(x_{0})$ given Lipschitz constant, and thus certify robustness .

IV-D2 Smooth Layers [85, 86, 87, 88, 89]

IV-D3 Curvature [90]

IV-E Incomplete Verification via Probabilistic Approaches

Besides deterministic verification, one recently emerging branch of studies proposes to add random noise to smooth the models, and thus derive the certified robustness for these smoothed models (See Definition 7). We call this line of work probabilistic robustness verification approaches or randomized smoothing based approaches since they provide probabilistic robustness guarantees and all existing probabilistic verification approaches are designed for smoothed models. Currently, only these verification approaches are scalable enough to certify nontrivial robustness on the large-scale ImageNet dataset.

The integral in Definition 7 cannot be exactly solved. Thus, instead, Monte-Carlo estimation and hypothesis testing are used to approximate the exact solution. As a result, the certification is probabilistic rather than deterministic (Definition 3).

A majority of verification approaches only use zeroth-order information of the smoothed classifier, i.e., the probabilities $\Pr_{\delta\sim\mu}[F(x_{0}+\delta)=y]$ for $y\in[C]$ where the clean input is $x_{0}$, to compute the robustness certification. Among these approaches, Neyman-Pearson based approaches are proved to be the tightest .

Given clean input $x_{0}$, when adding noise $\delta$, we suppose the model $F$ predicts true class $y_{0}$ with probability $P_{A}\mathrel{\mathop{\mathchar 58\relax}}=\Pr_{\delta\sim\mu}[F(x_{0}+\delta)=y_{0}]$ and runner-up class with $P_{B}\mathrel{\mathop{\mathchar 58\relax}}=\max_{y^{\prime}\in[C]\mathrel{\mathop{\mathchar 58\relax}}y^{\prime}\neq y_{0}}\Pr_{\delta\sim\mu}[F(x_{0}+\delta)=y^{\prime}]$. High-confidence intervals for $P_{A}$ and $P_{B}$ can be obtained with Monte-Carlo sampling. The high-level intuition for Neyman-Pearson based approaches is: if the attacker’s perturbed input $x$ is close to $x_{0}$, the distribution of $x+\delta$ would highly overlap the distribution of $x_{0}+\delta$ where $\delta\sim\mu$ is the added smoothing noise. Therefore, the corresponding $P_{A}^{\prime}$ and $P_{B}^{\prime}$ for perturbed input $x$ will not change too much from $P_{A}$ and $P_{B}$ for clean input $x_{0}$. That means, if there is a sufficient margin between $P_{A}$ and $P_{B}$, then $P_{A}^{\prime}$ will still be larger than $P_{B}^{\prime}$. Thus, the smoothed classifier will still predict $y_{0}$ for perturbed input $x$ according to Definition 7.

Formally, based on Neyman-Pearson lemma , one can derive a tight lower bound for $P_{A}^{\prime}$ and upper bound for $P_{B}^{\prime}$ given $P_{A}$, $P_{B}$, and input shift (i.e., $x-x_{0}$). Then, we solve the distance lower bound that guarantees $P_{A}^{\prime}>P_{B}^{\prime}$ to get robustness certification.

Using zeroth-order information, the robustness verification can also be derived from: (1) differential privacy (DP) where Gaussian and Laplace mechanisms in DP can induce certified robustness for models smoothed with Gaussian and Laplace distributions ; (2) Lipschitz bound ; (3) statistics view ; and (4) level-set method . These approaches derive looser or equivalently tight robustness certification as Neyman-Pearson based approaches.

IV-E2 Approaches with First-Order Information [99, 100]

IV-E3 Choice of Smoothing Distributions

To achieve satisfactory certified robustness, besides verification approaches, the choice of smoothing distribution is also important for these randomized smoothing based approaches.

The smoothing distributions can control trade-offs between certified robustness and accuracy, where distribution with larger variance can lead to a larger certified radius under the same $P_{A}$ and $P_{B}$, but hurts the clean accuracy since input signal is more severely corrupted by noise .

V Robust Training Approaches

Normally-trained DNNs are usually non-robust where effective attacks can find adversarial examples with almost 100% probability . To achieve high certified robustness, DNNs need to be trained with robust training approaches which aim to improve robustness guarantees, as illustrated in Figure 2.

Current robustness verification approaches usually favor certain properties of DNNs to achieve high certified robustness. For instance: (1) Branch-and-bound verification (Section IV-A3) uses incomplete verification such as linear relaxation to reduce explored branches and boost the certification efficiency so it favors DNNs whose linear relaxations are tight and for other DNNs the certification process is significantly slower . (2) Linear relaxation verification (Section IV-B) can certify only models whose specific linear relaxations are tight. (3) Lipschitz or curvature verification (Section IV-D) can certify only models where a small Lipschitz or curvature constant can be computed. (4) Verification for smoothed DNNs (Section IV-E) certifies larger radius for models with higher correct-prediction probability under noise. These favored properties are not directly promoted by standard training or empirical defenses. Therefore, to improve certified robustness, robust training approaches are proposed to promote these properties during training.

We divide existing robust training approaches into three categories: regularization-based, relaxation-based, and augmentation-based. We defer the illustration to App. D.

Discussion. Robust training approaches can improve model robustness and at the same time remarkably enhance desired properties of models for corresponding verification approaches. Thus, models trained with a robust training approach usually achieve much better certified robustness based on corresponding verification, as reflected by evaluation in Section VI-A.

Models trained by one robust training approach are often verified to have poor robustness by a mismatched verification approach (as shown in Section VI-A). This is because the models do not inherit the desired property of the verification. For example, models trained for randomized smoothing based approach can predict well for noisy input but may have many unstable neurons and loose linear relaxations, making them difficult to be verified by complete or linear relaxation verification. Models trained for linear relaxation are not specialized for predicting noisy input and are challenging for randomized smoothing based verification .

As a result, an important research goal is to develop verification that does not heavily rely on specific model properties so it can verify existing robustly trained or empirically defended models. Recently, some complete verification approaches are shown tractable for verifying empirically defensed (e.g., PGD adversarially trained ) models though they are still limited to small models. Thus, proposing more practically efficient complete verification approaches may be a viable path towards this goal. Another research goal is to improve certified robustness for a given task, by improving from both the verification side and the robust training side, such as tighter or more training-friendly relaxation , or more effective training methods , which we will discuss further in Section VIII.

VI Benchmark, Leaderboard, and Implications

In this section, we introduce an open-source toolbox to systematically benchmark $20+$ certifiably robust approaches. Based on benchmark results and the leaderboard on representative datasets, we outline practical implications for deploying certifiably robust approaches for DNNs.

We present the following evaluation: (1) for representative deterministic verification approaches, we compare their certified robustness over a diverse set of trained models of different scales; (2) for representative probabilistic verification approaches and their corresponding robust training approaches, we compare the best certified robustness they jointly achieve. We do such separation because deterministic and probabilistic certificates have different semantics and their supported system models are different. The evaluation is made possible by our open-source unified toolbox—a first toolkit integrating a wide range of verification approaches.

(1) On relatively small models, complete verification approaches can effectively verify robustness, thus they are the best choice. (2) On larger models, usually linear relaxation based verification approaches perform the best since the complete verification approaches are too slow and other approaches are too loose, yielding almost $0\%$ certified accuracy. However, linear relaxation based verification still cannot handle large DNNs and they are still too loose compared with the upper bound provided by PGD attack. (3) On robustly trained models, if the robust training approach is CROWN-IBP which is tailored for IBP and CROWN (two linear relaxation verification approaches), IBP and CROWN can certify high certified accuracy while others fail to certify. Indeed, robust training approaches can usually boost the certified accuracy but the models must be verified with corresponding verification approaches as discussed in Section V. (4) SDP approaches usually take too long and thus are less practical.

VI-A2 Findings from Comparing Probabilistic Verification Approaches

VI-B Leaderboard on Certified Robustness

What is the state-of-the-art certified accuracy achieved on representative datasets? Table II shows a leaderboard of certified accuracy under different settings from peer-reviewed publications till April 1, 2023. The high certified accuracy is jointly achieved by robust training (shown by reference bracket) and verification (shown by name).

VI-C Practical Implications

In practice, what are the most suitable certifiably robust approaches for users to deploy? Based on the benchmark results and the leaderboard, we present practical implications in Figure 4, where we envision two scenarios: 1) users want to improve certified robustness for their tasks at hand; 2) users want to evaluate or certify the robustness of given models.

When users want to evaluate or certify the robustness of certain models, they need to choose a suitable verification approach. Inspired by our benchmark, we present the implications in the lower part of Figure 4. For small and medium models trained by standard training or empirical defenses, the branch-and-bound based complete verification and multi-neuron relaxation verification can certify the robustness efficiently. Specifically, for small models, the solver-based (concretely, MILP-based) verification approaches can certify good robustness. But for large models, none of these methods can finish in a feasible time (one day per input). Therefore, we must use more efficient but loose verification such as IBP (Section IV-B2) and verification approaches for smoothed DNNs (Section IV-E), which usually yield trivial certified robustness radius and it is an active research area to make tighter verification approaches scalable for these large models. In addition, we find that the ranking of empirical defenses for small/medium models based on certified robustness is consistent with that evaluated by strong empirical attacks such as PGD . If models are trained by robust training approaches, as discussed in Section V, using the corresponding verification approaches targeted by the training approach would be the best choice.

VII Extensions and Applications

The methodologies derived from certifiably robust DNNs have recently been applied to much broader areas.

Extensions to diverse types of system models. There are efforts on generalizing existing DNN verification approaches to deal with more types of system models. For example: (1) Some approaches that are designed for feed-forward ReLU networks, such as linear relaxation based approaches, have been extended to support general DNNs , recurrent networks , transformers , generative models , and model ensembles . The main methodology is to derive the corresponding linear bounds for activation functions or attention mechanisms in these system models. Some complete verification approaches, e.g., branch-and-bound based ones , also support general DNNs. However, these complete verification approaches become incomplete when applied on general DNNs. (2) Verification approaches for Lipschitz-bounded networks and non-ReLU networks have not been generalized to other system models yet. (3) Verification approaches for smoothed DNNs typically need access to only the final prediction label, so they are applicable to any classification models. However, the model must follow the corresponding smoothing-based inference protocol. (4) There are also verification approaches for decision trees , decision stumps , nearest prototype classifiers , and logic ensembles . However, there is no verification and robust training approach that supports all these system models yet. This is because verification and robust training approaches need to exploit properties (piecewise linearity, Lipschitz bound, smoothness, etc) of specific system models to achieve certified robustness.

Certified robustness for concrete applications. Beyond the classification task, the discussed methodologies, such as linear relaxation and Neyman-Pearson approaches, have been extended to certify DNNs in many concrete applications. In natural language processing, extensions include certification for recurrent neural networks against embedding perturbations , word substitutions , and word transformations . Extensions have also been studied for object detection , segmentation , and point cloud models in computer vision, and speech recognition . Verification and robust training approaches have also been proposed for reinforcement learning .

VIII Insights, Challenges, and Future Directions

In this section, we summarize characteristics, strengths, limitations, and fundamental connections among certifiably robust approaches, then discuss barriers, main challenges, and future directions for DNN certification.

A unified view: characteristics, strengths, limitations, and connections of certifiably robust approaches. To reveal the fundamental connections, we adopt a unified view of robustness verification: all existing verification approaches provide an abstraction of given DNN models to verify the robustness. For example, the branch-and-bound verification views the model as the union of several sub-domains where the model output in each domain can be bounded, e.g., by linear inequalities. The branching process is essentially refining the abstraction by splitting sub-domains whose current abstractions are not precise enough. The linear relaxation based verification uses some linear constraints to abstract the possible behavior of the model in the whole perturbation region. The probabilistic verification uses the queried information, such as zeroth-order information, to abstract the model behavior. This view is closely related to the concept of abstract interpretation in traditional program analysis . Therefore, the scalability and tightness trade-off of verification mentioned in Section II-C is essentially the inherent trade-off between preciseness and efficiency of abstraction: more precise abstraction enables tighter robustness certification, whereas has higher time and space complexity. Thus, for a model that is not specifically trained, the most suitable verification approach is the most precise one that can be computed for this model size. Concrete approach selection guidelines are in Section VI-C. We note that, under this unified view, the favored properties of each verification (listed in Section V) are tight conditions of the corresponding abstraction domain. Thus, robust training approaches that promote these properties can boost verification tightness for the model to improve certified robustness. More concrete strengths and limitations of each verification are discussed in “practical implications” and “research implications” boxes in Section IV.

IX Conclusions

We presented an SoK for certifiably robust approaches for DNNs, including both robustness verification approaches and robust training approaches. We show characteristics, strengths, limitations, and fundamental connections among these approaches. Our discussion summarizes the current research status both theoretically and empirically, reveals limitations, and highlights future directions.

Acknowledgment

We would like to thank Xiangyu Qi for conducting the benchmark evaluation on some probabilistic verification approaches for smoothed DNNs. We thank Dr. Ce Zhang, Dr. Sasa Misailovic, and Dr. Gagandeep Singh for their thoughtful feedback. We also thank the support of NSF grant No.1910100, NSF CNS 2046726, C3 AI, the Alfred P. Sloan Foundation, and the AWS Research Awards.

References

Appendix A Scalability and Tightness Measurements

This appendix contains more discussion on the scalability and tightness characterization in Section III.

Deails on tightness ranks. For general DNNs, we rank the tightness from $T_{1}$ to $T_{7}$ where $T_{7}$ is the tightest. $T_{1}<T_{2}<T_{3}$ comes from benchmark results, $T_{3}<T_{4}<T_{5}$ comes from theoretical analyses , and $T_{5}<T_{6}$ and $T_{6}<T_{7}$ come from empirical observations in and respectively. For smoothed DNNs we rank the tightness from $ST_{1}$ to $ST_{4}$ based on existing theoretical analyses: $ST_{1}<ST_{2}$ comes from , $ST_{2}<ST_{3}$ comes from , and $ST_{3}<ST_{4}$ comes from .

Appendix B Omitted Illustrations

This appendix includes the omitted figure illustrations.

B-B ReLU Relaxation with Single Input Variable

B-C ReLU Relaxation with Multiple Input Variables

Appendix C Details on Linear Inequality Based Verification

This appendix entails the omitted details of linear inequality verification approaches introduced in Section IV-B2.

More details on polyhedra abstraction. Fast-Lin uses a parallel line as the lower bound as shown in Figure 6(b). CROWN and DeepPoly both support adjustable lower bound. They both use $y=\lambda x$ with adjustable $\lambda\in$ as the lower bound, while their heuristics for determining $\lambda$ are slightly different. FROWN and $\alpha$-CROWN deploy gradient-based optimization on lower bound slope $\lambda$ to improve tightness.

These approaches maintain the linear bound for each layer $k$ in the form of ${\bm{L}}_{k}x+b_{L,k}\leq z_{k}(x)\leq{\bm{U}}_{k}x+b_{U,k}$ for any $x\in B_{p,\epsilon}(x_{0})$. From the bound for layer $k$, we can deduct the bound after affine mapping $\hat{z}_{k+1}={\bm{W}}_{k}z_{k}+b_{k}$:

Zonotope abstraction. Zonotope is another type of over-approximation or abstract interpretation domain that can be propagated layer by layer efficiently . Zonotope abstraction has the same efficiency and slightly inferior tightness compared to polyhedra abstraction .

Duality-based approaches. Since the robustness verification can be viewed as an optimization problem (1), we can consider its Lagrangian dual problem. Especially, since 1 is a minimization problem, any feasible dual solution provides a valid lower bound of the primal problem and therefore a valid verification. Moreover, the dual problem is always convex . Typical duality-based approaches are WK , D-LP , PVT , and Lagrangian decomposition where WK is proved to share equivalent tightness with polyhedra abstraction approaches, and the others are proved to share equivalent tightness with linear programming based approaches .

Appendix D Illustration of Robust Training Approaches

Regularization-based training. For complete verification, Xiao et al find that the number of branches is upper bounded by the number of unstable neurons (see Definition 4) which motivates a regularization term to increase the ReLU neuron’s stability for training. For complete verification based on linear region traversal, we can train with a regularization term maximizing the margin to non-robust regions . The Lipschitz and curvature verification favor small Lipschitz constant and small curvature bounds respectively. Therefore, the corresponding robust training approaches explicitly penalize large Lipschitz or curvature bounds .

Relaxation-based training. For linear relaxation based verification approaches, models with tight linear relaxation bounds are favored. To train such models, corresponding robust training approaches usually use the computed bounds from linear relaxation as the training objective to explicitly improve the bound tightness. This idea is similar to the powerful empirical defense named adversarial training which uses effective attacks to approximately find “most adversarial” example $\max_{x\in B_{p,\epsilon}(x_{0})}{\mathcal{L}}(f_{\theta}(x),y_{0})$ and minimize model weights $\theta$ w.r.t. it. In relaxation-based training, instead, we compute an upper bound of $\max_{x\in B_{p,\epsilon}(x_{0})}{\mathcal{L}}(f_{\theta}(x),y_{0})$ and minimize it. The bound can be derived from IBP , polyhedra-based , zonotope-based , or duality-based verification . Some useful training tricks are: combining relaxation-based loss with standard loss to improve benign accuracy , applying relaxation on some layers but not all to balance benign accuracy and certified robustness , specialized weight initialization and training scheduling , and using reference space to guide the relaxation . An intriguing phenomenon of relaxation-based training is that tighter relaxation, when used as the training objective, may not lead to more certifiably robust models , while the loosest IBP relaxation can achieve almost the highest certified robustness. A conjecture is that tighter relaxation may lead to a less smooth loss landscape containing discontinuities or sensitive regions which poses challenges for gradient-based training . Theoretical understanding of relaxation-based training is still lacking. Note that solver based and branch-and-bound based complete verification usually use linear relaxations for bounding. Therefore, models trained with these relaxation-based training approaches can usually be efficiently certified by these complete verification approaches .

Appendix E Benchmark Evaluation Details

We present a thorough comparison of representative deterministic verification approaches in Table III.

Table III shows certified accuracy on CIFAR-10 for deterministic approaches. Each row corresponds to a verification approach, PGD attack, or clean accuracy. More results such as average certified robustness radius, average running time, and results on MNIST are on our website. Findings from our evaluation are discussed in Section VI-A.

E-B Comparison of Probabilistic Verification

We present a thorough comparison of representative probabilistic verification approaches for smoothed DNNs with different smoothing distributions and robust training approaches. We either fix the robust training part and vary the verification approaches or the other way around.

Evaluation protocol. We use ResNet-110 and Wide ResNet 40-2 as the model architecture. $n=1,000$ samples are used for selecting the top label; $N=100,000$ samples are used for certification. For all robust training approaches, we adopt default hyperparameters as reported in corresponding papers. The failure probability is set to $1-\alpha=.001$. We uniformly draw $500$ samples from the test set for evaluation. All the above settings follow common practice in .

Comparison results and discussion. We show results on CIFAR-10 in Table IV. Results on ImageNet can be found on our benchmark website. Findings from our evaluation are discussed in Section VI-A.

We extend the very recent double sampling randomized smoothing in to provide robustness certification for smoothed DNNs by sampling the statistics of the smoothed DNNs’ prediction using both the original smoothing distribution ${\mathcal{P}}$ and an additional smoothing distribution ${\mathcal{Q}}$ that shares the same form but a different variance from ${\mathcal{P}}$’s variance. Note that we leverage additional information—the prediction probability under ${\mathcal{Q}}$. In contrast, the zeroth-order methods only leverage the sampling probability information from ${\mathcal{P}}$. The extension methodology is listed in Appendix H.3 of .

Models. We train the models using both commonly-used Gaussian augmentation and state-of-the-art Consistency training . On all datasets, we use the default model structures and hyperparameters. All models are trained with the original smoothing distribution ${\mathcal{P}}$.

Baselines. We consider the Neyman-Pearson-based certification method as the baseline. For both baseline and our method, we set the certification confidence to be $1-2\alpha=99.8\%$. We use $10^{5}$ samples for estimating $P_{A}$ and $Q_{A}$ per instance. Note that Neyman-Pearson certification does not use the information from additional distribution and all $10^{5}$ samples are used to estimate the interval of $P_{A}$. In our method, we use $5\times 10^{4}$ samples to estimate the interval of $P_{A}$ and the rest $5\times 10^{4}$ samples for $Q_{A}$.

Metric. We uniformly draw $1000$ samples from the test set, and report the certified accuracy under each radius $r$ as defined in Equation 6. We also report the benign accuracy of the smoothed classifier. Both settings and the metric follow the standard evaluation protocol in literature .