Robustness Verification for Classifier Ensembles^††thanks: Research funded by the project NWA.BIGDATA.2019.002: “EXoDuS - EXplainable Data Science” and the FWO G030020N project “SAILor”

Recent years have seen a rapid progress in machine learning (ML) with a strong impact to fields like autonomous systems, computer vision, or robotics. As a consequence, many systems employing ML show an increasing interaction with aspects of our everyday life, consider autonomous cars operating amongst pedestrians and bicycles. While studies indicate that self-driving cars, inherently relying on ML techniques, make around 80% fewer traffic mistakes than human drivers [19], verifiable safety remains a major open challenge [26, 13, 23, 5].

In the context of self-driving cars, for instance, certain camera data may contain noise that can be introduced randomly or actively via so-called adversarial attacks. We focus on the particular problem of such attacks in image classification. A successful attack perturbs the original image in a way such that a human does not recognize any difference while ML misclassifies the image. A measure of difference between the ground truth classification, for instance by a human, and a potentially perturbed ML classifier is referred as the loss.

A standard way to render image classification more robust against adversarial attacks is to employ a set of classifiers, also referred to as classifier ensembles [2, 20, 21, 3]. The underlying idea is to obscure the actual classifier from the attacker. One possible formalization of the competition between an adversarial attacker and the ensemble is that of a zero-sum game [20]: The attacker chooses first, the ensemble tries to react to the attack with minimal loss — that is, choosing a classifier that induces maximal classification accuracy.

In this setting, the attacker may need to use randomization to behave optimally (see Fig. 1, cf. [6]). Such an attack is called optimal if the expected loss is maximized regardless of the choice of classifier.

Inspired by previous approaches for single classifiers [15, 12], we develop a formal verification procedure that decides if a classifier ensemble is robust against any randomized attack. In particular, the formal problem is the following. Given a set of classifiers and a labelled data set, we want to find a probability distribution and a set of attacks that induce an optimal randomized attack. Akin to the setting in [20], one can provide thresholds on potential perturbations of data points and the minimum shift in classification values. Thereby, it may happen that no optimal attack exists, in which case we call the classifier ensemble robust. Our aim is the development of a principled and effective method that is able to either find the optimal attack or prove that the ensemble is robust with respect to the predefined thresholds.

To that end, we first establish a number of theoretical results. First, we show that the underlying formal problem is \NP-hard. Towards computational tractability, we also show that for an optimal attack there exists an upper bound on the number of attacks that are needed. Using these results, we provide an SMT encoding that computes suitable randomized attacks for a set of convolutional neural networks with ReLU activation functions and a labelled data set. In case there is no solution to that problem, the set of neural networks forms a robust classifier ensemble, see Fig. 2. Together with the state-of-the-art SMT solver Z3 [9], this encoding provides a complete method to solve the problem at hand. Yet, our experiments reveal that it scales only for small examples. We outline the necessary steps to formulate the problem as a mixed-integer linear programming (MILP), enabling the use of efficient optimization solvers like Gurobi [14].

In our experiments, we show the applicability of our approach by means of a benchmark set of binary classifiers, which were trained on the MNIST and German traffic sign datasets [10, 25].

Let $\mathbf{x}$ be a vector $(x_{1},\dots,x_{d})\in\mathbb{R}^{d}$. We write $\left\lVert\mathbf{x}\right\rVert_{1}$ for the “Manhattan norm” of $\mathbf{x}$, that is $\sum_{i=1}^{d}|\mathbf{x}_{i}|$.

We will make use of a partial inverse of the $\max$ function. Consider a totally ordered set $Y$ and a function $f\colon X\to Y$. Throughout this work we define the $\operatorname*{arg\,max}$ (arguments of the maxima) partial function as follows. For all $S\subseteq X$ we set $\operatorname*{arg\,max}_{s\in S}f(s):=m$ if $m$ is the unique element of $S$ such that $f(m)=\max_{s\in S}f(s)$. If more than one element of $S$ witnesses the maximum then $\operatorname*{arg\,max}_{s\in S}f(s)$ is undefined.

A probability distribution over a finite set $D$ is a function $\mu\colon D\rightarrow[0,\,1]\subseteq\mathbb{R}$ with $\sum_{x\in D}\mu(x)=1$. The set of all distributions on $D$ is $\mathit{Distr}(D)$.

We state the formal problem and provide the required notation. Recall that in our setting we assume to have an ensemble of classifiers $C\subseteq\mathbb{C}$. Such an ensemble is attacked by a set of attacks that are selected randomly.

We sometimes call the value $\mathbf{x}+{\delta}(\mathbf{x})$ the attack point. Note that the classifier $c$ is not perfect, that is, $c(\mathbf{x})\neq c_{t}(\mathbf{x})$ for some $\mathbf{x}\in X$, already a zero-attack ${\delta}(\mathbf{x})=0$ leads to a misclassification.

We extend deterministic attacks by means of probabilities.

In general, a loss function $\ell\colon\mathbb{C}\times\mathbb{R}^{d}\times\mathbb{R}^{d}\rightarrow\mathbb{R}$ describes the penalty incurred by a classifier with respect to a labelled data point and an attack. In this work, we will focus on the widely used zero-one loss.

In particular, the loss function yields one if the image of the classifier $c$ is undefined for the attack point $\mathbf{x}+{\delta}(\mathbf{x})$. Note furthermore that the loss is measured with respect to the ground truth classifier $c_{t}$. Thereby, the classifier $c$ and the zero function as deterministic attack do not necessarily induce a loss of zero with respect to $c_{t}$. This assumption is realistic as, while we expect classifiers to perform well with regard to the ground truth, we cannot assume perfect classification in realistic settings.

We now connect a randomized attack to an ensemble, that is, a finite set $C\subseteq\mathbb{C}$ of classifiers. In particular, we quantify the overall value a randomized attack induces with respect to the loss function and the ensemble.

This value is the minimum (over all classifiers) mean expected loss with respect to the randomized attack and the classifiers from $C$. An optimal adversarial attack against $C\subseteq\mathbb{C}$ with respect to a labelled data set $(X,c_{t})$ is a randomized attack which maximizes the value $\mathbf{Val}(A,\mathbb{P})$ in Equation (1).

We are now ready to formalize a notion of robustness in terms of $\varepsilon$-bounded attacks and a robustness bound $\alpha\in\mathbb{R}$, as proposed in [20] for a set of classifiers.

In other words, an $(\varepsilon,\alpha)$-robust ensemble is such that for all possible $\varepsilon$-bounded random attacks $(A,\mathbb{P})$, there is at least one classifier $c\in C$ from the ensemble such that $\sum_{\mathbf{x}\in X}\,\operatorname*{\mathbb{E}}_{{\delta}\sim\mathbb{P}}[\ell_{\mathrm{0-1}}(c,\mathbf{x},{\delta}(\mathbf{x}))]<\alpha|X|.$ Conversely, an ensemble is not $(\varepsilon,\alpha)$-robust if there is an $\varepsilon$-bounded randomized attack with a misclassification value of at least $\alpha$.

In this section we establish two key results that carry essential practical implication for our setting. First, we show that in order to obtain an optimal randomized attack, only a bounded number of deterministic attacks is needed.¹¹1An analogue of this property had already been observed by Perdomo and Singer in [20, Section 3] in the case when classifiers are chosen randomly. Thereby, we only need to take a bounded number of potential attacks into account in order to prove the $\alpha$-robustness of a set of classifiers and a given labelled data set. Second, we establish that our problem is in fact \NP-hard, justifying the use of SMT and MILP solvers to (1) compute any optimal randomized attack and, more importantly, to (2) prove robustness against any such attack.

In this section, we describe the main elements of our SMT and MILP encodings to compute (optimal) randomized attacks or prove the robustness of classifier ensembles. We start with a base encoding and will afterwards explain how to explicitly encode the classifiers and the loss function.

In the previous section, we showed that our problem of neural network robustness verification is \NP-hard. Meaningful comparison between approaches, therefore, needs to be experimental. To that end, we use classifiers trained on multiple image data sets and report on the comparison between the SMT and MILP encodings. In what follows, we analyze the running time behavior of the different verifiers, the generated attacks and the misclassification value for the given data points, and whether a set of classifiers is robust against predefined thresholds.

We presented a new method to formally verify the robustness or, vice versa, compute optimal attacks for an ensemble of classifiers. Despite the theoretical hardness, we were able to, in particular by using MILP-solving, provide results for meaningful benchmarks. In future work, we will render our method more scalable towards a standalone verification tool for neural network ensembles. Moreover, we will explore settings where we do not have white-box access to the classifiers and employ state-of-the-art classifier stealing methods.