DeepSafe: A Data-driven Approach for Checking
Adversarial Robustness in Neural Networks
Divya Gopinath1 , Guy Katz2 , Corina S. Păsăreanu1 , and Clark Barrett2
1

arXiv:1710.00486v1 [cs.NE] 2 Oct 2017

Carnegie Mellon University Silicon Valley
divgml@gmail.com,
corina.pasareanu@west.cmu.edu, corina.s.pasareanu@nasa.gov
2
Stanford University
guyk@cs.stanford.edu, barrett@cs.stanford.edu

Abstract. Deep neural networks have become widely used, obtaining remarkable results in domains such as computer vision, speech recognition, natural language processing, audio recognition, social network filtering, machine translation, and bio-informatics, where they have produced results comparable to human
experts. However, these networks can be easily “fooled” by adversarial perturbations: minimal changes to correctly-classified inputs, that cause the network
to misclassify them. This phenomenon represents a concern for both safety and
security, but it is currently unclear how to measure a network’s robustness against
such perturbations. Existing techniques are limited to checking robustness around
a few individual input points, providing only very limited guarantees. We propose
a novel approach for automatically identifying safe regions of the input space,
within which the network is robust against adversarial perturbations. The approach is data-guided, relying on clustering to identify well-defined geometric
regions as candidate safe regions. We then utilize verification techniques to confirm that these regions are safe or to provide counter-examples showing that they
are not safe. We also introduce the notion of targeted robustness which, for a
given target label and region, ensures that a NN does not map any input in the
region to the target label. We evaluated our technique on the MNIST dataset and
on a neural network implementation of a controller for the next-generation Airborne Collision Avoidance System for unmanned aircraft (ACAS Xu). For these
networks, our approach identified multiple regions which were completely safe
as well as some which were only safe for specific labels. It also discovered several
adversarial perturbations of interest.

1

Introduction

In recent years, advances in deep neural networks (NN) have enabled the representation
and modeling of complex non-linear relationships. In this paper, we study a common
use of NN as classifiers that take in complex, high dimensional input, pass it through
multiple layers of transformations, and finally assign to it a specific output label or class.
Such classifiers have been used in a variety of applications, including pattern analysis,
image classification, speech and audio recognition, and self-driving cars; it is expected
that this trend will continue and intensify, with neural networks also being integrated
into safety-critical systems which require high assurance guarantees.

While the usefulness of neural networks is evident, it has been observed that stateof-the-art networks are highly vulnerable to adversarial perturbations: given a correctlyclassified input x, it is possible to find a new input x0 that is very similar to x but is assigned a different label [20]. For instance, in image-recognition networks it is possible
to add a small amount of noise (undetectable by the human eye) to an image and change
how it is classified by the network.
Worse still, adversarial examples have also been found to transfer across networks,
making it possible to attack networks in a black-box fashion, without access to their
weights. Recent work has demonstrated that such attacks can be carried out in practice [13]. Vulnerability of neural networks to adversarial perturbations is thus a safety
and security concern, and it is essential to explore systematic methods for evaluating
and improving the robustness of neural networks against such attacks.
To date, researchers have mostly focused on efficiently finding adversarial perturbations around select individual input points. The problem is typically cast as an optimization problem: for a given network F and an input x, find an x0 for which F (x0 ) 6= F (x)
while minimizing kx − x0 k. In other words, the goal is to find an input x0 as close
as possible to x such that x0 and x are labeled differently. Finding the optimal solution
for this optimization problem is computationally difficult, and so various approximation
approaches have been proposed. Some approaches are gradient based [6,7,20], whereas
others use optimization techniques [3]. There are also techniques that focus on generating targeted attacks: adversarial perturbations that result in the network classifying the
perturbed input with a specific target label [6, 7, 20].
These various approaches for finding adversarial perturbations have successfully
demonstrated the weakness of many state-of-the-art networks; however, because these
approaches operate on individual input points, it is unclear how to apply them to large
input domains, unless one does a brute-force enumeration of all input values which
is infeasible for most input domains. Furthermore, because they are inherently incomplete, these techniques do not provide any robustness guarantees when they fail to find
an adversarial input. Orthogonal approaches have also been proposed for training networks that are robust against adversarial perturbations, but these, too, provide no formal
assurances [16].
Formal methods provide a promising way for providing such guarantees. Recent
approaches tackle neural network verification [8, 11] by casting it as an SMT solving
problem. Although typically slower than the aforementioned techniques, verification
can provide sound assurances that no adversarial examples exist within a given input
domain. Still, these techniques do not provide any guidance on how to select meaningful
regions within which the network is expected to behave consistently. And although
it is possible to formulate a naive notion of global robustness, ∀x, x0 . kx − x0 k <
 =⇒ F (x0 ) = F (x), which checks that any two points that are similar (within a
small acceptable ) have the same label, this is not only inefficient to check but also
fails to hold for points on legitimate boundaries between regions.
Recent work uses Reluplex to check a more refined version of local and global
robustness, where the confidence score of the lables of close inputs is checked to be
within an acceptable parameter [12]. While this can potentially handle situations where

the inputs are on the boundaries, it still requires manually finding the regions in which
this check is likely to hold.
Our approach. We propose a novel technique, DeepSafe, for formally evaluating the
robustness of deep neural networks. The key notion underlying our approach is the use
of a data-guided methodology to determine regions that are likely to be safe (instead of
focusing on individual points). This enables characterizing the behavior of the network
over partitions of the input space, which in turn makes the network’s behavior amenable
to analysis and verification.
Our technique can automatically perform the following steps: (i) we propose a novel
clustering algorithm to automatically partition the input domain into regions in which
points are likely to have the same true label; (ii) these regions are then checked for
robustness using an existing verification tool; (iii) the verification checks targeted robustness which, given a specific incorrect label, guarantees that no input in the region
is mapped by the NN to that label; (iv) for each region, the result of the targeted verification is either that the NN is safe (i.e. no points within the region are mapped to
the target label), or, if it is not, an adversarial example demonstrating that it is unsafe;
(v) robustness against all target labels (other than the correct label) indicates that the region is completely safe and all points within the region are mapped to the same correct
label.
Thus, we decompose the robustness requirement for a NN into a number of local
proof obligations, one set for each region. Our approach provides several benefits: we
discover input regions that are likely to be robust (this is akin to finding likely invariants
in program analysis) which are then candidates for the safety checks; if a region is
found to be safe, we provide guarantees w.r.t all points within that region, not just for
individual points as in previous techniques; and the discovered regions can improve the
scalability of formal NN verification by focusing the search for adversarial examples
only on the input space defined by a region. Note also that the regions can be used to
improve the scalability of the above-mentioned approximate techniques (e.g gradient
descent methods) by similarly restricting the search to the input points confined by the
region.
As the usual notion of safety might be too strong for many NNs, we introduce the
concept of targeted robustness, analogous to targeted adversarial perturbations [6,7,20].
A region of the input space that is safe w.r.t. a specific target label indicates that within
that region, the network is guaranteed to be robust against misclassification to the specific target label. Therefore, even if in that region the network is not completely robust
against adversarial perturbations, we give guarantees that it is safe against specific targeted attacks. As a simple example consider a NN used for perception in an autonomous
car that classifies the images of a semaphore as red, green or yellow. We may want to
guarantee that the NN will never classify the image of a green light as a red light and
vice versa but it may be tolerable to misclassify a green light as yellow, while still
avoiding traffic violations.
The contributions of our approach are as follows:
1. Label-guided clustering: We present a clustering technique which is guided by
the labels of the training data. This technique is an extension of the standard, un-

supervised clustering algorithm kMeans [10] which we modified for our purposes.
The output of the technique is a set of dense clusters within the input space, each of
which contains training inputs that are close to each other (with respect to a given
distance metric) and are known to share the same output label.
2. Well-defined safe regions: Each cluster defines a subset of the inputs, a finite number of which belong to the training data. The key point is that the network is expected to display consistent behavior (i.e., assign the same label) over the entire
cluster. Hence, the clusters can be considered as safe regions in which adversarial perturbations should not exist, backed by a data-guided rationale. Therefore,
searching for adversarial perturbations within the cluster-based safe regions has a
higher chance of producing valid examples, i.e. inputs whose misclassification is
considered erroneous network behavior. The size, location and boundaries of the
clusters, which depend on the distribution of the training data can help guide the
search: for instance, it often does not make sense to search for adversarial perturbations of inputs that lie on the boundaries between clusters belonging to different
labels, as adversarial perturbations in those areas are likely to constitute acceptable
network behavior.
3. Scalable verification: Within each cluster, we use formal verification to prove that
the network is robust or find adversarial perturbations. The verification of even
simple neural networks is an NP-complete problem [11], and is very difficult in
practice. Focusing on clusters means that verification is applied to small input domains, making it more feasible and rendering the approach as a whole more scalable. Further, the verification of separate clusters can be done in parallel, increasing
scalability even further.
4. Targeted robustness: Our approach focuses on determining targeted safe regions,
analogous to targeted adversarial perturbations. A region of the input space that is
safe w.r.t. a specific target label indicates that within that region, the network is
guaranteed to not map any input to the specific target label. Therefore, even if the
network is not completely robust against adversarial perturbations, we are able to
give guarantees that it is safe against specific targeted attacks.
Our proposed basic approach can have additional, interesting applications. For example, clusters can be used in additional forms of analysis, e.g. in determining whether
the network is particularly susceptible to specific kinds of perturbations in certain regions of the input space. Also, the clustering approach is black-box in the sense that it
relies solely on the data distribution to determine the safe regions (and not on the network parameters). Consequently, it is applicable to a wide range of networks with various topologies and architectures. Finally, as we later demonstrate, it is straightforward
to incorporate into the approach user-specific information (domain-specific constraints)
regarding which adversarial perturbations can be encountered in practice. This helps
guide the search towards finding valid perturbations.
The remainder of this paper is organized as follows. In Section 2, we provide the
needed background on clustering, neural networks, and neural network verification. In
Section 3, we describe in detail the steps of our clustering-based approach, followed by
an evaluation in Section 4. The possible limitations of our approach are discussed in
Section 5. Related work is then discussed in Section 6, and we conclude in Section 7.

2
2.1

Background
Clustering

Clustering is an approach used to divide a population of data-points into groups called
clusters, such that the data-points in each cluster are more similar (with respect to some
metric) to other points in the same cluster than to the rest of data-points.
Here we focus on a particularly popular clustering algorithm called kMeans [10]
(although our approach could be implemented using different clustering algorithms as
well). Given a set of n data-points {x1 , . . . , xn } and k as the desired number of clusters,
the algorithm partitions the points into k clusters, such that the variance (also referred
to as “within cluster sum of squares”) within each cluster is minimal. The metric used
to calculate the distance between points is customizable, and is typically the Euclidean
distance (L2 norm) or the Manhattan distance (L1 norm). For points x1 = hx11 , . . . , x1n i
and x2 = hx21 , . . . , x2n i these are defined as:
v
u n
n
X
uX
1
2
(1)
kx1 − x2 kL1 =
|xi − xi |,
kx1 − x2 kL2 = t (x1i − x2i )2
i=1

i=1

The kMeans clustering is an iterative refinement algorithm which starts with k random points considered as the means (the centroids) of k clusters. Each iteration then
comprises mainly of two steps: (i) assign each data-point to the cluster whose centroid
is closest to it with respect to the chosen distance metric; and (ii) re-calculate the new
means of the clusters, which will serve as the new centroids. The iterations continue
until the assignment of data-points to clusters does not change. This indicates that the
clusters satisfy the constraint that the variance within the cluster is minimal, and that
the data-points within each cluster are closer to each other than to points outside the
cluster.
2.2

Neural Networks

Neural networks and deep belief networks have been used in pattern analysis, image
classification, speech/audio recognition, perception modules in self-driving cars so on.
Typically, the objects in such domains are high dimensional and the number of classes
that the objects need to be classified into is also high — and so the classification functions tend to be highly non-linear over the input space. Deep learning operates with the
underlying rationale that groups of input parameters could be merged to derive higher
level abstract features, which enable the discovery of a more linear and continuous classification function. Neural networks are often used as classifiers, meaning they assign to
each input an output label/class. A neural network F can thus be regarded as a function
that assigns to input x an output label y, denoted as F (x) = y.
Internally, a neural networks is comprised of multiple layers of nodes called neurons, where each node refines and extracts information from values computed by nodes
in the previous layer. A typical 3 layer neural network would consist of the following;
the first layer is the input layer, which takes in the input variables (also called features) x1 , x2 , . . . , xn . The second layer is a hidden layer: each of its neurons computes

a weighted sum of the input variables using a unique weight vector and a bias value, and
then applies a non-linear activation function to the result. The last layer is the output
layer, which uses the softmax function to make a decision on the class for the input,
based on the values computed by the previous layer.
2.3

Neural Network Verification

Neural networks are trained and tested on finite sets of inputs and outputs and are then
expected to generalize well to previously-unseen inputs. While this seems to work in
many cases, when the network in question is designed to be part of a safety-critical system, we may wish to verify formally that certain properties hold for any possible input.
Traditional verification techniques often cannot directly be applied to neural networks,
and this has sparked a line of work focused on transforming the problem into a format
more amenable to existing tools such as LP and SMT solvers [4, 8, 18, 19].
While our approach is general in the sense that it could be coupled with any verification technique, for evaluation purposes we used the recently-proposed Reluplex
approach [11]. Reluplex is a sound and complete simplex-based verification procedure,
specifically tailored to achieve scalability on deep neural networks. Intuitively, the algorithm operates by eagerly solving the linear constraints posed by the neural network’s
weighted sums, while attempting to satisfy the non-linear constraints posed by its activation functions in a lazy manner. This often allows Reluplex to safely disregard many
of these non-linear constraints, which is where the bulk of the problem’s complexity
stems from. Reluplex has been used in evaluating techniques for finding and defending against adversarial perturbations [2], and it has also been successfully applied to
a real-world family of deep neural networks, designed to operate as controllers in the
next-generation Airborne Collision Avoidance System for unmanned aircraft (ACAS
Xu) [11].

3

The DeepSafe Approach

In this section we describe in greater detail the steps of our proposed approach: (i) clustering of training inputs; (ii) cluster analysis; (iii) cluster verification; and (iv) processing of possible adversarial examples.
3.1

Clustering of Training Inputs

Fig. 2. a) Original clusters with k=2, b) Clusters with modified kMeans

for xn = 1 : nn(1)
function rep = next_fun_acas(p)
Zn = Yn(Yn(:,7) == Un(xn,1),1:6);
movefile(’count.csv’,’countin.csv’);
Bn = unique(Zn(:,6));
n1in = importdata("countin.csv");
n0n = size(Bn);
m = size(n1in);
wn = xn + cnt;
rep = 0;
if (n0n(1,1) > 1)
for sn = 1 : m(1)
rep = 1;
num = n1in(sn,1);
csvwrite("cluster"+num2str(wn)
lo = "cluster"+ num2str(num)
+ ".csv",Zn);
+".csv";
n1n(1,1) = wn;
ln = "clusterin"+num2str(num)
n1n(1,2) = n0n(1,1);
+".csv";
dlmwrite("count.csv",n1n,
loc = char(lo);
’-append’,’delimiter’,’,’);
lnc = char(ln);
else
movefile(loc,lnc);
sn = Un(xn,1);
end
csvwrite("clusterFinal"+num2str(wn)
cnt = 0;
+ "_" + num2str(p)+".csv",C(sn,:));
for yn = 1 : m(1)
dlmwrite("clusterFinal"+num2str(wn)
X = importdata("clusterin"+
+ "_" + num2str(p)+".csv",Zn,
num2str(n1in(yn,1))+".csv");
’-append’,’delimiter’,’,’);
[idx,C] = kmeans(X,n1in(yn,2),
end
’Distance’,’sqeuclidean’);
end
Xn = [X,idx];
cnt = wn;
Yn = sortrows(Xn,7);
end end
Un = unique(Yn(:,7));
nn = size(Un);

Fig. 1. MATLAB code for modified kMeans clustering.

In our approach, we use the kMeans clustering algorithm (see Section 2.1) to perform
clustering over the training inputs. By training inputs, we mean all inputs whose correct
labels or output classes are known: this includes the training, validation, and test sets.
We note that our technique works even in the absence of the training data, e.g. by
applying the clustering to a set of randomly generated inputs that are labeled according
to a given trained network. The user will then need to check that the labels are valid.
The kMeans approach is typically an unsupervised technique, meaning that clustering is based purely on the similarity of the data-points themselves, and does not depend
on their labels. Here, however, we use the labels to guide the clustering algorithm into
generating clusters that have consistent labeling (in addition to containing points that
are similar to each other). The modified clustering algorithm starts by setting the number of clusters k, which is an input to the kMeans algorithm, to be equal to the number
of unique labels. Once the clusters are obtained, we check whether each cluster contains only inputs with the same label. kMeans is then applied again on each cluster that
is found to contain multiple labels, with k set to the number of unique labels within that
cluster. This effectively breaks the “problematic” cluster into multiple sub-clusters. The
process is repeated until all clusters contain inputs which share a single label. The number of clusters, which is an input parameter of the kMeans algorithm, is often chosen
arbitrarily. In our approach, we take guidance from the training data to customize the
number of clusters to the domain under consideration. Pseudocode for the MATLAB
implementation of the algorithm appears in Fig. 1. In every iteration, count.csv
maps the index of each input dataset, clusterINDEX.csv, to the number of unique
labels its instances correspond to. Clusters whose instances correspond to the same label
are named clusterFinalINDEX.csv.

Let us consider a toy example with training data labeled as either stars or circles.
Each training data point is characterised by two dimensions/attributes (x,y). The original kMeans algorithm with k = 2, will partition the training inputs into 2 groups, purely
based on proximity w.r.t. the 2 attributes (Fig. 2a). However, this groups stars and circles together. Our modified algorithm creates the same partitions in its first iteration,
however, since each cluster does not satisfy the invariant that it only contains training
inputs with the same label, it proceeds to iteratively divide each cluster into two subclusters until this invariant is satisfied. This creates 5 clusters as shown in (Fig. 2b); 3
with label star and 2 with label circle. This example is typical for domains such as image classification, where even a small change in some attribute values for certain inputs
could change their label.
Our modified clustering algorithm typically produces small, dense clusters of
consistently-labeled inputs. The underlying assumption of our approach is that each
such cluster therefore constitutes a safe region in which all inputs (and not just the
training points) should be labeled consistently. For instance, in our toy example, the algorithm creates relatively small clusters of stars and circles, separating them from each
other. Searching within these clusters, which represent small neighborhoods of inputs
belonging to the same label, may yield more meaningful results than searching regions
within an arbitrary distance of each input.
Each of the clusters generated by kMeans is characterized by a centroid cen and
a radius R, indicating the maximum distance of any instance in the cluster from its
centroid. While inputs deep within each cluster are expected to be labeled consistently,
the boundaries of the clusters may lie in low-density regions, and could have different
labels. In order to improve the accuracy of our approach, we shrink the clusters by
replacing R with the average distance of any instance from the centroid, denoted r. This
increases the likelihood that all points within the cluster should be consistently labeled,
and that any deviation from this would constitute a valid adversarial perturbation. The
training inputs within a cluster have the same label, which we refer to as the label of the
cluster, l. To summarize, the main hypothesis behind our approach is:
Hypothesis 1 For a given cluster C, with centroid cen and radius r, any input x within
distance r from cen has the same true label l as that of the cluster:
kx − cenk ≤ r

⇒

label(x) = l

It immediately follows from this hypothesis that any point x0 in the cluster which is
assigned a different label F (x0 ) 6= l by the network constitutes an adversarial perturbation. An adversarial input for our toy example could be as follows; a hypothetical NN,
in its process of input transformation may incorrectly bring some of the inputs within
the cluster with stars close to circles, thereby classifying them as circle.
Distance metric. The similarity of the inputs within a cluster is determined by the
distance metric used for calculating the proximity of the inputs. Therefore, it is important to choose a distance metric that generates acceptable levels of similarity for the
domain under consideration. Our approach assumes that every input, characterized by
m attributes, can be considered as a point in Euclidean space. The Euclidean distance

(Eq. 1) is a commonly used metric for measuring the proximity of points in Euclidean
space. However, recent studies indicate that the usefulness of Euclidean distance in determining the proximity between points diminishes as the dimensionality increases [1].
The Manhattan distance (Eq. 1) has been found to capture proximity more accurately
at high dimensions. Therefore, in our experiments, we set the distance metric depending on the dimensionality of the input space (Section 4). Other distance metrics can be
easily accommodated by our approach.
3.2

Cluster Analysis

The clusters obtained as a result of the previous step characterize the behavior of the
network over large chunks of the input space. Analysis of these clusters can provide
useful insights regarding the behavior and accuracy of the network. Listed below are
cluster properties that we use in our approach.
– Density: We define the density of a cluster to be the number of instances per unit
distance within the cluster. For a cluster with n points and average distance r from
the points to the centroid, the cluster’s density is defined to be n/r. A cluster with
high density contains a large number of instances at close proximity to each other
(and because of our modified clustering algorithm, these instances are also labeled
consistently). We assume that in such clusters Hypothesis 1 holds, since it seems
undesirable that the network should assign a different label to inputs that lie within
the average distance from the centroid. However, this cannot be said regarding a
cluster with low density, which encompasses fewer inputs belonging to the same label and which are spread out. Therefore, for the purpose of the robustness check, we
disregard clusters with low density, in order to increase the chances of examining
only valid safe regions, and hence of detecting only valid adversarial perturbations.
– Centroid behavior: The centroid of a cluster can be considered as a representative
for the behavior of the network over that cluster — especially when the cluster’s
density is high. A classifier neural network assigns to each input a score for each
possible label, representing the network’s level of confidence that the input should
have that label (the label with the highest confidence is the one then assigned to the
input). Intuitively, targeted adversarial perturbations are more likely to exist, e.g.,
for the label whose level of confidence at the centroid is the second highest, than for
the least likely label. In our approach, we use the label scores to look for targeted
safe regions: regions of the input space within which the network is guaranteed to
be robust against misclassification to a specific target label.
3.3

Cluster Verification

Having identified and analyzed the clusters, we next use the Reluplex tool [11] to verify
a formula representing the negation of Hypothesis 1. This is done in a targeted manner
or on a per label basis. If the negated hypothesis is shown not to hold, the region is
indeed safe with respect to that label (targeted safe region); and otherwise, Reluplex
provides a satisfying assignment, which constitutes a valid adversarial perturbation.
The encoding is shown in Eq. 2:

∃x.

kx − cenkL1 ≤ r

∧

score(x, l0 ) ≥ score(x, l)

(2)

Here, x represents an input point, and cen, r and l represent the centroid, radius and
label of the cluster, respectively. l0 represents a label other than l. Reluplex models the
network without the final softmax layer, and so the networks’ outputs correspond to
the levels of confidence that the network assigns to each of the possible labels; we use
score(x, y) to denote the level of confidence assigned to label y at point x. Intuitively,
the formula holds for a given l0 if and only if there exists a point x within distance at
most r from cen, for which l0 is assigned higher confidence than l. Consequently, if
the property does not hold, then for every x within the cluster l has its score higher
than l0 . This ensures targeted robustness of the network for label l0 : the network is
guaranteed not to misclassify any input within the region to the target label l0 . Note that
for overlapping clusters with different labels, there is uncertainty regarding the desired
labels for the clusters’ intersection. Our method of reducing the clusters’ radius can
serve to exclude such regions.
The property in Eq. 2 is checked sequentially for every possible l0 ∈ L − {l},
where L denotes the set of all possible labels. If the property is unsatisfiable for all
l0 , it ensures complete robustness of the network for inputs within the cluster; i.e., the
network is guaranteed not to misclassify any input within the region to any other label.
This can be expressed more formally as shown below:
∀x. kx − cenkL1 ≤ r

⇒

∀l ∈ L − {l}. score(x, l) ≥ score(x, l0 )

(3)

from which it follows that Hypothesis 1 holds, i.e. that:
∀x. kx − cenkL1 ≤ r

⇒

label(x) = l

(4)

As is the case with many SMT-based solves, Reluplex typically solves satisfiable
queries more quickly that unsatisfiable ones. Therefore, in order to optimize performance we test the possible target labels l0 in descending order of the scores that they
are assigned at the centroid, score(cen, l0 ). Intuitively, this is because the label with the
2nd -highest score is more likely to yield a satisfiable query, etc.
Distances in Reluplex. Reluplex takes as input a conjunction of linear equations and
certain piecewise-linear constraints. Consequently, it is straightforward to model the
neural network itself and the query in Eq. 2. Our ability to encode the distance constraint
from that equation, kx − cenk ≤ r, depends on the distance metric being used. While
L1 is piecewise linear and can be encoded, L2 unfortunately cannot.
When dealing with domains where L2 distance is a better measure of proximity, we thus use the following approximation. We perform the clustering phase using the L2 distance metric as described before, and for each cluster obtain the radius r. When verifying the property in Eq. 2, however, we use the L1 norm. Because
kx − cenkL1 ≤ kx − cenkL2 , it is guaranteed that the verification is conducted within
the cluster under consideration, and any adversarial perturbation discovered will thus
be valid. If the verification shows that the network is robust, however, then this holds
only for the portion of the cluster that was checked. This limitation can be waived by
using a verification technique that directly supports L2 , or by enhancing Reluplex to
support it.

Clusters and scalability. The main source of computational complexity in neural network verification is the presence of non-linear, non-convex activation functions. However, when restricted to a small sub-domain of the input space, these functions may
present purely linear behavior — in which case they can be disregarded and replaced
with a linear constraint, which greatly simplifies the problem. Consequently, performing verification within small domains is beneficial, as many activation functions can
often be disregarded. Our approach naturally involves verification queries on small
clusters, which tends to be very helpful in this regard. Reluplex has built-in bound
tightening [11] functionality to detect such cases; and we leverage this functionality by
computing lower and upper bounds for each of the input variables within the cluster,
and provide these as part of our query to Reluplex.
Our approach lends itself to more scalable verification also through parallelization.
Because each cluster involves stand-alone verification queries, their verification can be
performed in parallel. Also, because Eq. 2 is checked independently for every l0 , these
queries can also be performed in parallel — expediting the process even further [12].
3.4

Processing Possible Adversarial Perturbations

A SAT solution to Eq. 2 for any target label (l0 ) indicates the presence of an input within
the region for which the network assigns a higher score to label l0 than to l. The check
for the validity of the adversarial example needs to be done by the user/domain expert.
Note that this does not mean that l0 has the highest score; i.e. it need not be a targeted
adversarial example for l0 . In some cases, there may be specific constraints on inputs
that can be considered valid adversarial examples. We have been able to successfully
model such domain-specific constraints for ACAS Xu to generate valid adversarial perturbations (Section 4).

4

Evaluation

We evaluated a proof-of-concept implementation of DeepSafe on two networks. The
first network was designed as a controller for the next-generation Airborne Collision
Avoidance System for unmanned aircraft (ACAS Xu), a highly safety-critical system.
The second network is a digit classifier over the popular MNIST image dataset.
4.1

ACAS Xu

ACAS X is a family of collision avoidance systems for aircraft, which is currently
under development by the Federal Aviation Administration (FAA) [9]. ACAS Xu is the
version for unmanned aircraft control. It is intended to be airborne and receive sensor
information regarding the drone (the ownship) and any nearby intruder drones, and
then issue horizontal turning advisories aimed at preventing collisions. The input sensor
data includes: (i) ρ: distance from ownship to intruder; (ii) θ: angle of intruder relative
to ownship heading direction; (iii) ψ: heading angle of intruder relative to ownship
heading direction; (iv) vown : speed of ownship; (v) vint : speed of intruder; (vi) τ : time
until loss of vertical separation; and (vii) aprev : previous advisory. See Fig 3 [11], for an

ψ
vown

vint

ρ

Intruder

Ownship
θ
Fig. 3. Inputs to the ACAS Xu system

illustration. The five possible output actions are as follows: Clear-of-Conflict (COC),
Weak Right, Weak Left, Strong Right, and Strong Left. Each advisory is assigned a
score, with the lowest score corresponding to the best action.
The FAA is currently exploring an implementation of ACAS Xu that uses an array
of 45 deep neural networks. These networks were obtained by discretizing the two
parameters, τ and aprev , and so each network contains five input dimensions and treats
τ and aprev as constants.

Fig. 4. Mis-classified as Strong left instead
of Strong Right

Fig. 5. Mis-classified as Strong left instead
of Strong Right

Applying our approach. We evaluated our techniques on one of the 45 ACAS Xu networks. It is a NN with 8 hidden layers and 300 ReLU activation nodes per layer. This
network had 2662704 inputs with known labels, each comprised of 5 dimensions, and
these were classified into 5 output labels, each representing a possible turning advisory
for the unmanned aircraft. The kMeans clustering was performed using L2 distance
metric. It yielded 7100 clusters with more than one input, and 146 single-input clusters.
These clusters were then sorted in descending order of their density. Reluplex was run
on the 40 most dense clusters, with a timeout set to 12 hours for each cluster. An unsatisfiable answer (indicating that Eq. 2 holds) was successfully obtained for all possible
l0 labels on 18 clusters, which were then deemed safe (confirmed by domain experts).
For 9 of the remaining clusters an unsatisfiable answer was obtained on some of the
l0 labels with the solver timing out for the rest, and for 3 additional clusters the solver
timed out without returning a concrete result for any of the l0 labels.

Processing adversarial examples using domain-specific knowledge For 6 clusters, Reluplex detected adversarial perturbations: inputs within the cluster which were classified
by the network as belonging to a different class than the cluster label. However, not every such example is considered valid — i.e., some may be invalid, in the sense that they
do not constitute incorrect network behavior. Here we consulted with the developers
of the networks [9], who provided an additional criterion in order to guide the search
towards perturbations which were likely to be valid: the adversarial perturbation should
share the values of the ψ, vown and vint parameters with nearby, correctly-classified inputs. We incorporated this information as follows: Given that the initial check (Eq. 2)
returns a SAT solution, we use Relulex to perform 2 additional checks. Each of them
solves the same equation Eq. 2, but in a constrained domain. In the first check we slice
the cluster to obtain the centroid plane, in which the last 3 dimensions are fixed to the
values of the centroid. The radius r has the same value as used before. In the second
check we slice to obtain the maximum plane, in which the last 3 dimensions are fixed
to the 3-valued tuple that appears maximum number of times in the cluster. The radius
is altered so that our search space remains within the cluster boundaries; this is obtained by applying the Pythagoras theorem using the radius r and the distance between
the centroid-plane and maximum-plane w.r.t the last three dimensions. The first two
parameters, ρ and θ, are allowed to vary as before.
For 2 of the 6 clusters, this resulted in UNSAT. For the rest, some adversarial examples were found on the centroid plane and/or maximum planes. These are valid adversarial examples. ACAS Xu domain experts stated that ACAS Xu is fairly robust system
and these adversarial examples were found to be small-range or border cases which are
not considered interesting or crucial enough. However, they confirmed that these were
valid adversarial examples nevertheless (Figs. 4, 5, 6, 7).
This particular case thus nicely demonstrates our ability to customize the technique
and integrate domain-specific knowledge provided by experts to help guide the search.

Fig. 6. Mis-classified as Strong Right instead of Clear of Conflict

4.2

Fig. 7. Mis-classified as Strong Right instead of Strong Left

MNIST Image Dataset

The MNIST database (Modified National Institute of Standards and Technology
database) is a large collection of handwritten digits that is commonly used for training various image processing systems [14].
Applying our approach. The MNIST dataset has 60,000 training input images, each
characterized by 784 attributes and belonging to one of 10 labels. kMeans clustering

Fig. 8. Images of 1 misclassified as 8 (a), 4 (b) , and 3 (c)

was performed using the L1 distance metric. It yielded 4524 clusters with more than
one inputs and 3029 single-input clusters. The clusters were sorted in descending order
of their density. Reluplex was run on the top 10 clusters, with a timeout set to 12 hours
for each cluster.
As explained in Section 3, the analysis was targeted: for each label l0 different than
the expected label l, a check was initiated to search for an adversarial example for which
l0 received a higher score than l. The search yielded adversarial examples for each of
the target labels in Eq. 2, for each of the clusters save for the two highest-density ones.
For these 2 clusters, adversarial examples were detected for all labels except the one
with the lowest score (when evaluated on the centroid). The adversarial examples were
validated manually by converting them to images. These results are not surprising, as
MNIST networks are known to be very susceptible to adversarial perturbations [3].
Some of the adversarial examples are shown in Fig. 8.

5

Threats to Validity

We discuss below possible threats to the validity of our approach and the experiments.
– Invalid adversarial examples: The validity of an adversarial perturbation depends
on the accuracy of the cluster in identifying regions of the input space which should
ideally be given the same label. Clustering as used in our approach typically generates small dense groups or small neighborhoods around known inputs. The NN,
on the other hand, attempts to abstract the input by focusing on certain features
more than the others in order to be able to assign a unique label to it. This abstraction also enables generalization of the network to other inputs not part of the
training data. However, this process tends to make the network inaccurate on inputs
in close neighborhoods to known inputs. Therefore, although clustering cannot be
considered as an alternative classifier to NN for any input, it can be considered to
be accurate or an oracle in close neighborhoods of known inputs. This can however
be impacted by the presence of noise in the input space due to irrelevant attributes,
which the NN sieves out.
– Invalid safety regions: There could be a scenario where both the cluster and the
network agree on the labels for all inputs within a region, however, ideally some of
them need to be classified to a different label. This can happen when the training
data is not representative enough.

– Generalization of experimental results: The current implementation of the solver
Reluplex used in our prototype tool only supports piecewise-linear activation functions. This could limit the generalization of the experimental results to networks
which use other types of activation functions.

6

Related Work

The vulnerability of neural networks to adversarial perturbations was first discovered
by Szegedy et. al. in 2013 [20]. They model the problem of finding the adversarial
example as a constrained minimization problem. Goodfellow et al. [7] introduced the
Fast Gradient Sign Method for crafting adversarial perturbations using the derivative
of the models loss function with respect to the input feature vector. They show that
NNs trained for the MNIST and CIFAR-10 classification tasks can be fooled with a
high success rate. An extension of this approach applies the technique in an iterative
manner [5]. Jacobian-based Saliency Map Attack (JSMA) [17] proposed a method for
targeted misclassification by exploiting the forward derivative of a NN to find an adversarial perturbation that will force the model to misclassify into a specific target class.
Carlini et. al. [3] recently proposed an approach that could not be resisted by state-ofthe-art networks such as those using defensive distillation. Their optimization algorithm
uses better loss functions and parameters (empirically determined) and uses three different distance metrics.
The DeepFool [15] technique simplifies the domain by considering the network to
be completely linear. They compute adversarial inputs on the tangent plane (orthogonal
projection) of a point on the classifier function. They then introduce non-linearity to the
model, and repeat this process until a true adversarial example is found.
Deep Learning Verification (DLV) [8] is an approach that defines a region of safety
around a known input and applies SMT solving for checking robustness. They consider
the input space to be discretized and alter the input using manipulations until it is at a
minimal distance from the original, to generate possibly-adversarial inputs. They can
only guarantee freedom of adversarial perturbations within the discrete points that are
explored. Our clustering approach can potentially improve the technique by constraining the discrete search within regions.

7

Conclusion

This paper presents a novel, data-guided technique to search for adversarial perturbations (or prove they cannot occur) within well-defined geometric regions in the input
space that correspond to clusters of similar inputs known to share the same label. In
doing so, the approach identifies and provides proof for regions of safety in the input
space within which the network is robust with respect to target labels. Preliminary experiments on the ACAS Xu and MNIST datasets highlight the potential of the approach
in providing formal guarantees about the robustness of neural networks in a scalable
manner.
In the future, we plan to investigate the following directions:

1. Re-training: If there are a number of single-input clusters or clusters with low
cardinality, it could indicate two cases: (i) if the density is low, there is not enough
training data in that region; or (ii) if the density is high, there is a lot of noise or
number of redundant attributes, which leads to repeated splitting of clusters. The
first case could act as a feedback for re-training. The second case is an indicator
that the clustering should probably be carried out at a higher layer of abstraction,
with a smaller number of more relevant attributes.
2. Input to other techniques: The boundaries of the cluster spheres formed by
kMeans lie in low density areas. Therefore, the network could be assumed to have
low accuracy around these boundaries. Thus, adversarial robustness checks around
instances that are closer to the edge of the clusters could exhibit a high number
of adversarial perturbations. This analysis could help identify potential inputs to
which other techniques for assessing local robustness could be applied.
3. Other Solvers: While in our implementation we have used Reluplex to perform the
verification, our approach is general and can use other tools as a back-end solver. As
checking robustness for deep neural networks is an active area of research, we plan
to investigate and integrate other solvers, as they become available. We also plan to
investigate testing, guided by the computed regions, as an alternative to verification,
for increased scalability, but at the price of losing the formal guarantees.
Acknowledgements. This work was partially supported by grants from NASA, NSF,
FAA and Intel.

References
1. C. C. Aggarwal, A. Hinneburg, and D. A. Keim. On the surprising behavior of distance
metrics in high dimensional spaces. In Proc. 8th Int. Conf. on Database Theory (ICDT),
pages 420–434, 2001.
2. N. Carlini, G. Katz, C. Barrett, and D. Dill. Ground-Truth Adversarial Examples, 2017.
Technical Report. http://arxiv.org/abs/1709.10207.
3. N. Carlini and D. Wagner. Towards evaluating the robustness of neural networks. In Proc.
38th IEEE Symposium on Security and Privacy, 2017.
4. R. Ehlers. Formal verification of piece-wise linear feed-forward neural networks. In Proc.
15th Int. Symp. on Automated Technology for Verification and Analysis (ATVA), 2017.
5. R. Feinman, R. R. Curtin, S. Shintre, and A. B. Gardner. Adversarial machine learning at
scale, 2016. Technical Report. http://arxiv.org/abs/1611.01236.
6. R. Feinman, R. R. Curtin, S. Shintre, and A. B. Gardner. Detecting adversarial samples from
artifacts, 2017. Technical Report. http://arxiv.org/abs/1703.00410.
7. I. J. Goodfellow, J. Shlens, and C. Szegedy. Explaining and harnessing adversarial examples,
2014. Technical Report. http://arxiv.org/abs/1412.6572.
8. X. Huang, M. Kwiatkowska, S. Wang, and M. Wu. Safety verification of deep neural networks. In Proc. 29th Int. Conf. on Computer Aided Verification (CAV), pages 3–29, 2017.
9. K. Julian, J. Lopez, J. Brush, M. Owen, and M. Kochenderfer. Policy compression for aircraft
collision avoidance systems. In Proc. 35th Digital Avionics System Conf. (DASC), pages 1–
10, 2016.
10. T. Kanungo, D. M. Mount, N. S. Netanyahu, C. D. Piatko, R. Silverman, and A. Y. Wu. An
efficient k-means clustering algorithm: Analysis and implementation. IEEE Transactions on
Pattern Analysis and Machine Intelligence, 24(7):881–892, 2002.

11. G. Katz, C. Barrett, D. Dill, K. Julian, and M. Kochenderfer. Reluplex: An efficient SMT
solver for verifying deep neural networks. In Proc. 29th Int. Conf. on Computer Aided
Verification (CAV), pages 97–117, 2017.
12. G. Katz, C. Barrett, D. Dill, K. Julian, and M. Kochenderfer. Towards proving the adversarial robustness of deep neural networks. In Proc. 1st Workshop on Formal Verification of
Autonomous Vehicles (FVAV), pages 19–26, 2017.
13. A. Kurakin, I. Goodfellow, and S. Bengio. Adversarial Examples in the Physical World,
2016. Technical Report. http://arxiv.org/abs/1607.02533.
14. Y. LeCun, C. Cortes, and C. J. C. Burges. The MNIST database of handwritten digits.
http://yann.lecun.com/exdb/mnist/.
15. S. Moosavi-Dezfooli, A. Fawzi, and P. Frossard. Deepfool: A simple and accurate method to
fool deep neural networks. In Proc. IEEE Conf. on Computer Vision and Pattern Recognition
(CVPR), pages 2574–2582, 2016.
16. N. Papernot and P. D. McDaniel. On the effectiveness of defensive distillation, 2016. Technical Report. http://arxiv.org/abs/1607.05113.
17. N. Papernot, P. D. McDaniel, S. Jha, M. Fredrikson, Z. B. Celik, and A. Swami. The limitations of deep learning in adversarial settings. In Proc. 1st IEEE European Symposium on
Security and Privacy (EuroS&P), pages 372–387, 2016.
18. L. Pulina and A. Tacchella. An abstraction-refinement approach to verification of artificial
neural networks. In Proc. 22nd Int. Conf. on Computer Aided Verification (CAV), pages
243–257, 2010.
19. L. Pulina and A. Tacchella. Challenging SMT solvers to verify neural networks. AI Communications, 25(2):117–135, 2012.
20. C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, I. Goodfellow, and R. Fergus.
Intriguing properties of neural networks, 2013. Technical Report. http://arxiv.org/
abs/1312.6199.

