SyReNN: A tool for analyzing deep neural networks

Abstract

Deep Neural Networks (DNNs) are rapidly gaining popularity in a variety of important domains. Unfortunately, modern DNNs have been shown to be vulnerable to a variety of attacks and buggy behavior. This has motivated recent work in formally analyzing the properties of such DNNs. This paper introduces SyReNN, a tool for understanding and analyzing a DNN by computing its symbolic representation. The key insight is to decompose the DNN into linear functions. Our tool is designed for analyses using low-dimensional subsets of the input space, a unique design point in the space of DNN analysis tools. We describe the tool and the underlying theory, then evaluate its use and performance on three case studies: computing Integrated Gradients, visualizing a DNN’s decision boundaries, and repairing buggy DNNs.

1 Introduction

Deep Neural Networks (DNNs) [1] have become the state-of-the-art in a variety of applications including image recognition [2, 3] and natural language processing [4]. Moreover, they are increasingly used in safety- and security-critical applications such as autonomous vehicles [5] and medical diagnosis [6,7,8,9]. These advances have been accelerated by improved hardware and algorithms.

DNNs (Sect. 2) are programs that compute a vector-valued function, i.e., from ${\mathbb {R}}^n$ to ${\mathbb {R}}^m$. They are loop-free programs written as a concatenation of alternating linear and non-linear layers. The coefficients of the linear layers are learned from data via gradient descent during a training process. A number of different non-linear layers (called activation functions) are commonly used, including the rectified linear and maximum pooling functions.

Fig. 1

Precise visualization of decision boundaries computed using SyReNN for the a ACAS Xu network and b MNIST digit recognition network. This is not a plot interpolating between finitely-many sampled points, instead SyReNN was used to quickly and precisely compute the exact decision boundaries

Owing to the variety of application domains and deployment constraints, DNNs come in many different sizes. For instance, large image-recognition and natural-language processing models are trained and deployed using cloud resources [3, 4], medium-size models could be trained in the cloud but deployed on hardware with limited resources [5], and finally small models could be trained and deployed directly on edge devices [10,11,12,13,14]. There has also been a recent push to compress trained models to reduce their size [15]. Such smaller models play an especially important role in privacy-critical applications, such as wake word detection for voice assistants, because they allow sensitive user data to stay on the user’s own device instead of needing to be sent to a remote computer for processing.

Although DNNs are very popular, they are not perfect. One particularly concerning development is that modern DNNs have been shown to be extremely vulnerable to adversarial examples, inputs that are intentionally manipulated to appear unmodified to humans but become misclassified by the DNN [16,17,18,19]. Similarly, fooling examples are inputs that look like random noise to humans, but are classified with high confidence by DNNs [20]. Mistakes made by DNNs have led to loss of life [21, 22] and wrongful arrests [23, 24]. For this reason, it is important to develop techniques for analyzing, understanding, and repairing DNNs.

This paper introduces SyReNN, a tool for understanding and analyzing DNNs. SyReNN implements state-of-the-art algorithms for computing precise symbolic representations of piecewise-linear DNNs (Sect. 3). Given a bounded polytope subset of the input space of a DNN, SyReNN computes a symbolic representation that decomposes the behavior of the DNN on that infinite subspace into finitely many linear functions. SyReNN implements the one-dimensional analysis algorithm of Sotoudeh and Thakur [25] and extends it to the two-dimensional setting as described in Sect. 4.

Key insights. There are two key insights enabling this approach, initially identified in Sotoudeh and Thakur [25]. First, most popular DNN architectures today are piecewise-linear, meaning they can be precisely decomposed into finitely many linear functions. This allows us to reduce their analysis to equivalent questions in linear algebra, one of the most well-understood fields of modern mathematics. Second, many applications only require analyzing the behavior of the DNN on a low-dimensional subset of the input space. Whereas prior work has attempted to give up precision for efficiency while analyzing high-dimensional input regions [26,27,28], our work has focused on algorithms that are both efficient and precise while analyzing lower-dimensional regions (Sect. 4).

Use cases. We demonstrate the utility of SyReNN on three main applications, each highlighting the key advantage of SyReNN; viz., the ability to provide precise information about the DNN by restricting the analysis to a low-dimensional subset of its input space.

The first application is in visualizing the decision boundaries of a DNN. With SyReNN, we can precisely plot the decision boundaries for a two-dimensional subset of the input space. The two-dimensional nature of the plot makes it ideal for a human designer to look at to understand the behavior of the DNN. The precise nature of the information provided by SyReNN ensures that the plot shows the true behavior on the infinite set of points. Figure 1a shows one such 2-dimensional plot for the ACAS Xu network ([5]), which determines what action an aircraft (ownship) should take to avoid a collision with an intruder. Notably, this is not the result of plotting the behavior of the DNN on a finite sampling of the inputs — such an approach would likely miss key behavior of the DNN, whereas our approach guarantees to find the exact decision boundaries. The network takes 5 inputs corresponding to the velocity and position of the aircraft; the plot shows the behavior of the DNN for a 2-dimensional subspace of the input space. From this plot, one can already see interesting and potentially dangerous behavior of the network: there is a region behind the plane where an intruder on the left may cause the network to recommend performing a weak left towards the intruder; there are small regions in which the network recommends strong right (or strong left) which should be weak right (or weak left). For safety-critical applications, such as aircraft collision avoidance, such precise visualization can be invaluable to a developer. Visualization of the ACAS Xu network is described in detail in Sect. 8.1. Section 8.2 describes the visualization of decision boundaries of image recognition networks. For instance, Fig. 1b shows the visualization of the decision boundaries of an MNIST handwritten digit recognition DNN. The corners of the triangle are three different drawings of the number 5, while points interior to the triangle correspond to interpolations between those images. The different colors show exactly where the network begins to misclassify fives as a variety of other digits, helping human designers better understand, and eventually improve, the behavior of the DNN.

The second application of SyReNN is the provable repair of DNNs (Sect. 8.3). DNN repair deals with the increasingly important problem of correcting DNN behavior to satisfy a given specification of a DNN after it has been trained. In contrast to heuristic approaches, e.g., based on gradient descent, provable repair guarantees that the repaired DNN does in fact satisfy the repair specification. Prior work can repair the behavior of the DNN for a finite set of input points [29, 30]. With SyReNN one can extend these techniques to repair the behavior for an infinite set of points (represented as a 2D polytope).

The last application of SyReNN is the precise computation of Integrated Gradients (IG) [31], a state-of-the-art measure used to determine which input dimensions, e.g., pixels for an image-recognition network, were most important in the final classification produced by the network (Sect. 8.4). IG is defined in terms of the DNN’s behavior on the line connecting the all-zero input and the input in question. Without the precise and efficient low-dimensional analysis of SyReNN, all prior work had only been approximating the IG.

Tool design. The SyReNN tool is designed to be easy to use and extend, as well as efficient (Sect. 7). The core of SyReNN is written as a highly-optimized, parallel C++ server using Intel TBB for parallelization [32] and Eigen for matrix operations [33]. CPU-based SyReNN uses Intel MKL-DNN for DNN evaluation while GPU-based SyReNN uses Nvidia cuDNN and cuBLAS for DNN evaluation as well as a mix of Intel TBB and Nvidia CUDA for symbolic representation computation. A user-friendly Python front-end interfaces with the PyTorch deep learning framework [34].

Contributions. The contributions of this paper are:

• A definition of symbolic representation of DNNs (Sect. 3).

• Efficient algorithms for computing symbolic representations for DNNs over low-dimensional input subspaces on CPU (Sect. 4) and GPU (Sect. 5).

• A generalization of the algorithm to arbitrary-dimensional input subspaces (Sect. 6).

• A design of a usable and well-engineered tool implementing these ideas called SyReNN (Sect. 7).

• Three applications of SyReNN (Sect. 8).

Section 2 presents preliminaries about DNNs; Sect. 9 presents related work; Sect. 10 concludes. SyReNN is available on GitHub at https://github.com/95616ARG/SyReNN_GPU.

2 Preliminaries

We now formally define the notion of DNN we will use in this paper.

Definition 1

A Deep Neural Network (DNN) is a function $f: {\mathbb {R}}^n \rightarrow {\mathbb {R}}^m$ which can be written $f = f_n \circ f_{n-1} \cdots \circ f_1$ for a sequence of layer functions $f_1$, $f_2$, ..., $f_n$.

Our work is primarily concerned with the popular class of piecewise-linear DNNs, defined below. In this definition and the rest of this paper, we will use the term “polytope” to mean a convex and bounded polytope, i.e., a bounded, finite intersection of linear constraints.

Definition 2

A function $f: {\mathbb {R}}^n \rightarrow {\mathbb {R}}^m$ is piecewise-linear (PWL) if its input domain ${\mathbb {R}}^n$ can be partitioned into finitely many possibly-unbounded polytopes $X_1, X_2, \ldots , X_k$ such that ${f}_{\restriction X_i}$ is linear for every $X_i$.

The most common activation function used today is the ReLU function, a PWL activation function defined below.

Definition 3

The rectified linear function (ReLU) is a function $\textsc {ReLU}: {\mathbb {R}}^n \rightarrow {\mathbb {R}}^m$ defined component-wise by

$$\begin{aligned} \textsc {ReLU}(\vec {v})_i :={\left\{ \begin{array}{ll} 0 &{}\text {if } v_i < 0 \\ v_i &{}\text {otherwise}, \\ \end{array}\right. } \end{aligned}$$

where $\textsc {ReLU}(\vec {v})_i$ is the ith component of the vector $\textsc {ReLU}(\vec {v})$ and $v_i$ is the ith component of the vector $\vec {v}$.

To show that $\textsc {ReLU}{}$ is PWL, we must partition its input domain ${\mathbb {R}}^n$ so that, in each partition, $\textsc {ReLU}{}$ is linear. In this case, we can use the orthants of ${\mathbb {R}}^n$ as our partitioning: within each orthant, the signs of the components do not change hence $\textsc {ReLU}{}$ is the linear map that just zeros out the negative components.

Although we focus on $\textsc {ReLU}{}$ due to its popularity and expository power, SyReNN works with a number of other popular PWL layers including MaxPool, Leaky ReLU, Hard Tanh, Fully-Connected, and Convolutional layers, as defined in [1]. PWL layers have become exceedingly common. In fact, nearly all of the state-of-the-art image recognition models bundled with PyTorch [35] are PWL.

Example 1

The DNN $f: {\mathbb {R}}^1 \rightarrow {\mathbb {R}}^1$ defined by

$$\begin{aligned} f(x) :=\begin{bmatrix} 1&-1&-1 \end{bmatrix} \textsc {ReLU}{}\left( \begin{bmatrix} 1 &{} -1 \\ 1 &{} 0 \\ -1 &{} 0 \end{bmatrix} \begin{bmatrix} x \\ 1 \end{bmatrix} \right) \end{aligned}$$

can be broken into layers $f = f_3 \circ f_2 \circ f_1$ where

$$\begin{aligned}{} & {} f_1(x) :=\begin{bmatrix} 1 &{} -1 \\ 1 &{} 0 \\ -1 &{} 0 \end{bmatrix} \begin{bmatrix} x \\ 1 \end{bmatrix}, \quad f_2 = \textsc {ReLU}{}, \quad \text {and} \quad \\{} & {} f_3(\vec {v}) = \begin{bmatrix} 1&-1&-1 \end{bmatrix}\vec {v}. \end{aligned}$$

The DNN’s input–output behavior on the domain $[-1, 2]$ is shown in Fig. 2.

Fig. 2

Input–output behavior of the DNN from Example 1

3 A symbolic representation of DNNs

We formalize the symbolic representation according to the following definition:

Definition 4

Given a PWL function $f: {\mathbb {R}}^n \rightarrow {\mathbb {R}}^m$ and a bounded convex polytope $X \subseteq {\mathbb {R}}^n$, we define the symbolic representation of f on X, written $\widehat{{f}_{\restriction X}}$, to be a finite set of polytopes $\widehat{{f}_{\restriction X}}~=~\{ P_1, \ldots , P_n \}$, such that:

• 1. The set $\{ P_1, P_2, \ldots , P_n \}$ partitions X, except possibly for overlapping boundaries.

• 2. Each $P_i$ is a bounded convex polytope.

• 3. Within each $P_i$, the function ${f}_{\restriction P_i}$ is linear.

Notably, if f is a DNN using only PWL layers, then f is PWL and so we can define $\widehat{{f}_{\restriction X}}$. This symbolic representation allows one to reduce questions about the DNN f to questions about finitely many linear functions. For example, because linear functions are convex, to verify that $\forall \vec {{\textit{x}}} \in X.\quad f(\vec {{\textit{x}}}) \in Y$ for some polytope Y, it suffices to verify $\forall P_i \in \widehat{{f}_{\restriction X}}. \quad \forall \vec {v} \in \texttt {Vert}(P_i). \quad f(\vec {v}) \in Y$, where $\texttt {Vert}(P_i)$ is the (finite) set of vertices for the bounded convex polytope $P_i$; thus, here both of the quantifiers are over finite sets. The symbolic representation described above can be seen as a generalization of the ExactLine representation [25], which considered only one-dimensional restriction domains of interest. ExactLine is now included in SyReNN as an optimization for the case of one-dimensional input polytopes.

Example 2

Consider again the DNN $f: {\mathbb {R}}^1 \rightarrow {\mathbb {R}}^1$ given by

$$\begin{aligned} f(x) :=\begin{bmatrix} 1&-1&-1 \end{bmatrix} \textrm{ReLU}\left( \begin{bmatrix} 1 &{} -1 \\ 1 &{} 0 \\ -1 &{} 0 \end{bmatrix} \begin{bmatrix} x \\ 1 \end{bmatrix} \right) \end{aligned}$$

and the region of interest $X = [-1, 2]$. The input–output behavior of f on X is shown in Fig. 2. From this, we can see that

$$\begin{aligned} \widehat{{f}_{\restriction X}} = \{ [-1, 0], [0, 1], [1, 2] \}. \end{aligned}$$

Within each of these partitions, the input–output behavior is linear, which for ${\mathbb {R}}^1 \rightarrow {\mathbb {R}}^1$ we can see visually as just a line segment. As this set fully partitions X, then, this is a valid $\widehat{{f}_{\restriction X}}$.

4 Computing the symbolic representation on 2D regions

This section presents an efficient algorithm for computing $\widehat{{f}_{\restriction X}}$ for a DNN f composed of PWL layers. To retain both scalability and precision, in this section we will require the input region X be two-dimensional. This design choice is relatively unexplored in the neural-network analysis literature (most analyses strike a balance between precision and scalability, ignoring dimensionality). We show that, for two-dimensional X, we can use an efficient polytope representation to produce an algorithm that demonstrates good best-case and in-practice efficiency while retaining full precision. This algorithm represents a direct generalization of the approach of [25].

The difficulties our algorithm addresses arise from three areas. First, when computing $\widehat{{f}_{\restriction X}}$ there may be exponentially many such partitions on all of ${\mathbb {R}}^n$ but only a small number of them may intersect with X. Consequently, the algorithm needs to be able to find those partitions that intersect with X efficiently without explicitly listing all of the partitions on ${\mathbb {R}}^n$. Second, it is often more convenient to specify the partitioning via hyperplanes separating the partitions than by explicit polytopes. For example, for the one-dimensional $\textsc {ReLU}{}$ function we may simply state that the point $x = 0$ separates the two partitions, because $\textsc {ReLU}{}$ is linear both in the region $x \le 0$ and $x \ge 0$. Finally, neural networks are typically composed of sequences of linear and piecewise-linear layers, where the partitioning imposed by each layer individually may be well-understood but their composition is more complex. For example, identifying the linear partitions of $y = \textsc {ReLU}{}(4\cdot \textsc {ReLU}{}(-3x - 1) + 2)$ is non-trivial, even though we know the linear partitions of each composed function individually.

Our algorithm only requires the user to specify the hyperplanes defining the partitioning for the activation function used in each layer, and the current implementation comes with common PWL activation functions built-in. For example, if a $\textsc {ReLU}{}$ layer is used for an n-dimensional input vector, then the hyperplanes would be defined by the equations $x_1 = 0, x_2 = 0, \ldots , x_n = 0$. SyReNN computes the symbolic representation for a single layer at a time, composing them sequentially to compute the symbolic representation across the entire network.

To allow such compositions of layers, instead of directly computing $\widehat{{f}_{\restriction X}}$, we will define another primitive, denoted by the operator $\otimes$ and sometimes referred to as $\textsc {ExtendPWL}$, such that

$$\begin{aligned} \textsc {ExtendPWL}{}(h, \widehat{{g}_{\restriction X}}) = h \otimes \widehat{{g}_{\restriction X}} = \widehat{{h \circ g}_{\restriction X}}. \end{aligned}$$

(1)

Consider $f = f_n \circ f_{n-1} \circ \cdots \circ f_1$, and let $I: x \mapsto x$ be the identity map. I is linear across its entire input space, and, thus, $\widehat{{I}_{\restriction X}} = \{ X \}$. By the definition of $\textsc {ExtendPWL}{}(f_1, \cdot )$, we have $f_1 \otimes \widehat{{I}_{\restriction X}} = \widehat{{(f_1 \circ I)}_{\restriction X}} = \widehat{{f_1}_{\restriction X}}$, where the final equality holds by the definition of the identity map I. We can then iteratively apply this procedure to inductively compute $\widehat{{(f_i \circ \cdots \circ f_1)}_{\restriction X}}$ from $\widehat{{(f_{i-1} \circ \cdots \circ f_1)}_{\restriction X}}$ like so:

$$\begin{aligned} f_i \otimes \widehat{{(f_{i - 1} \circ \cdots \circ f_1)}_{\restriction X}} = \widehat{{(f_i \circ f_{i - 1} \circ \cdots \circ f_1)}_{\restriction X}} \end{aligned}$$

until we have computed $\widehat{{(f_n \circ f_{n-1} \circ \cdots \circ f_1)}_{\restriction X}} = \widehat{{f}_{\restriction X}}$, which is the required symbolic representation. Notably, linear functions do not change linear partitions, hence if f is linear then $f \otimes \widehat{{g}_{\restriction X}} = \widehat{{f\circ g}_{\restriction X}} = \widehat{{g}_{\restriction X}}$. This process is formalized in Algorithm 1.

4.1 Algorithm for ExtendPWL

Algorithm 2 presents an algorithm for computing $\textsc {ExtendPWL}$ for arbitrary PWL functions, where $\textsc {ExtendPWL}{}(h, \widehat{{g}_{\restriction X}}) = h \otimes \widehat{{g}_{\restriction X}} = \widehat{{h \circ g}_{\restriction X}}$.

Geometric intuition for the algorithm. Consider the $\textsc {ReLU}{}$ function (Definition 3). It can be shown that, within any orthant (i.e., when the signs of all coefficients are held constant), $\textsc {ReLU}{}(\vec {{\textit{x}}})$ is equivalent to some linear function, in particular the element-wise product of $\vec {x}$ with a vector that zeroes out the negative-signed components. However, for our algorithm, all we need to know is that the linear partitions of $\textsc {ReLU}{}$ (in this case the orthants) are separated by hyperplanes $x_1 = 0, x_2 = 0, \ldots , x_n = 0$.

Given a two-dimensional polytope X, the execution of the algorithm for $f = \textsc {ReLU}{}$ can be visualized as follows. We pick some vertex v of X, and begin traversing the boundary of the polytope in counter-clockwise order. If we hit an orthant boundary (corresponding to some hyperplane $x_i = 0$), it implies that the behavior of the function behaves differently at the points of the polytope to one side of the boundary from those at the other side of the boundary. Thus, we partition X into $X_1$ and $X_2$, where $X_1$ lies to one side of the hyperplane and $X_2$ lies to the other side. We recursively apply this procedure to $X_1$ and $X_2$ until the resulting polytopes all lie on exactly one side of every hyperplane (orthant boundary). But lying on exactly one side of every hyperplane (orthant boundary) implies each polytope lies entirely within a linear partition of the function (a single orthant), hence the application of the function on that polytope is linear, and hence we have our partitioning.

Functions used in algorithms. Given a two-dimensional polytope X, Vert(X) returns a list of its vertices in counter-clockwise order, repeating the initial vertex at the end. Given a set of points S, ConvexHull(S) represents their convex hull (the smallest polytope containing every point in S). Given a scalar value x, Sign(x) computes the sign of that value (i.e., $-1$ if $x < 0$, $+1$ if $x > 0$, and 0 if $x = 0$). Given an n-dimensional polytope P, $\textrm{Facets}(P)$ is the set of $n-1$-dimensional facets that make up the boundary of P.

Fig. 3

Diagrams demonstrating the 2D $\textsc {ExtendPWL}$ algorithm

Algorithm description. The key insight of the algorithm is to recursively partition the polytopes until such a partition lies entirely within a linear region of the function f. Algorithm 2 begins by constructing a queue containing the polytopes of $\widehat{{g}_{\restriction X}}$. Each iteration either removes a polytope from the queue that lies entirely in one linear region (placing it in Y), or splits (partitions) some polytope into two smaller polytopes that get put back into the queue. When we pop a polytope P from the queue, Line 6 iterates over all hyperplanes $N_k\cdot x = b_k$ defining the piecewise-linear partitioning of f, looking for any for which some vertex $V_i$ lies on the positive side of the hyperplane and another vertex $V_j$ lies on the negative side of the hyperplane. If none exist (Line 7), by convexity we are guaranteed that the entire polytope lies entirely on one side with respect to every hyperplane, meaning it lies entirely within a linear partition of f. Thus, we can add it to Y and continue. If two such vertices are found (starting Line 10), we then call SplitPlane() (Algorithm 3) to actually partition the polytope on opposite sides of the hyperplane, adding both to our worklist. SplitPlane() works by finding “extreme” i and j indices such that $V_i$ is the last vertex in a counter-clockwise traversal to lie on the same side of the hyperplane as $V_1$ and $V_j$ is the last vertex lying on the opposite side of the hyperplane, then solving for the new vertex where that edge intersects the hyperplane.

In the best case, each partition is in a single orthant. Then, the algorithm never calls SplitPlane() at all — it merely iterates over all of the n input partitions, checks their v vertices, and appends to the resulting set (for a best-case complexity of O(nv)). In the worst case, it splits each polytope in the queue on each hyperplane, resulting in exponential time complexity. As we will show in Sect. 8, this exponential worst-case behavior is not encountered in practice, thus making SyReNN a practical tool for DNN analysis.

Example of the algorithm. Consider the polytope shown in Fig. 3a with vertices $\{ v_1, v_2, v_3 \}$, and suppose our activation function has two piecewise-linear regions separated by the vertical line (1D hyperplane) $Nx + b = 0$ shown.

Because this hyperplane has some of the vertices of the polytope on one side and some on the other, we will use it as the N, b hyperplane on Line 10. Then SplitPlane is called. We will assume the vertices are ordered so that the extremal vertices found starting at Line 1 are $V_i = v_1$ and $v_j = v_3$. SplitPlane will then add new vertices $p_i = v_4$ (shown in Fig. 3b) where the edge $v_1\rightarrow v_2$ intersects the hyperplane, as well as $p_j = v_5$ where the edge $v_3 \rightarrow v_1$ intersects the hyperplane. Separating all of the vertices on the left of the hyperplane from those on the right, we find that this has partitioned the original polytope into two sub-polytopes, each on exactly one side of the hyperplane, as desired. If there were more intersecting hyperplanes, we would then recurse on each of the newly-generated polytopes to further subdivide them by the other hyperplanes.

Proofs of correctness. The two theorems below formally argue for correctness of Algorithm 3 and Algorithm 2. They are a special case of the arguments in Sect. 6.

Theorem 1

Algorithm 3 correctly splits a 2D polytope $\texttt {ConvexHull}(V)$ by the hyperplane $Nx = b$.

Proof

The intuition was described earlier in this section. Formally, Algorithm 3 is the special case of Algorithm 6 for $k = 2$. See Theorem 4 for the proof of its correctness.

This special-casing relies on one key observation, which is that, in Algorithm 6 for $k = 2$, exactly two of the facets (edges) will cross the hyperplane. To see why, first consider the restriction of the hyperplane $Nx = b$ to the polytope $\texttt {ConvexHull}(V)$. Notice that, assuming the hyperplane actually crosses $\texttt {ConvexHull}(V)$ (i.e., does not contain it entirely), then this restriction will correspond to a line crossing a polytope. But, if this line crossed three distinct edges, then it would have at least three distinct intersection points with the polytope. But these three points must make a line, meaning one of those points must be between the other two, meaning one of those edges must have points that can be written as a convex combination of those on the other two edges, i.e., one of the edges must be on the interior of the polytope, a contradiction. $\square$

Theorem 2

Algorithm 2 correctly computes $f \otimes \widehat{{g}_{\restriction X}}$.

Proof

The intuition was described earlier in this section. For a formal correctness proof, see the proof of the generalized Theorem 5, from which this claim follows as a special case. The only difference in the algorithms is that we call the 2D-specialized SplitPlane instead of SplitHyperPlane[2]. $\square$

4.2 Representing Polytopes

We close this section with a discussion of implementation concerns when representing the polytopes that make up the partitioning of $\widehat{{f}_{\restriction X}}$. In standard computational geometry, polytopes can be represented in two equivalent forms:

• 1. The half-space or H-representation, which encodes the polytope as an intersection of finitely many half-spaces. (Each half-space being defined by a linear inequality $ax \le b$.)

• 2. The vertex or V-representation, which encodes the polytope as a set of finitely many points; the polytope is then taken to be the convex hull of the points (i.e., smallest convex shape containing all of the points).

Certain operations are more efficient when using one representation compared to the other. For example, finding the intersection of two polytopes in an H-representation can be done in linear time by conjoining their representative linear constraints, but the same is not possible in V-representation. On the other hand, checking if a polytope in V-representation is empty is as simple as checking whether it has any vertices at all, while the same query for a polytope in H-representation requires solving a considerably more expensive linear programming problem.

There are three main operations on polytopes we need perform in our algorithms: (i) identifying which hyperplanes a polytope intersects, (ii) splitting a polytope with a hyperplane, and (iii) applying a linear map to all points in the polytope. In general, the first and third are significantly more efficient in a V-representation, while the second is often more efficient in an H-representation. In particular, (i) is linear time on a V-representation but requires solving a complicated linear programming problem on an H-representation. Similarly, unless the linear map happens to be invertible, which almost never happens for DNN weight matrices which are usually learned and between different-dimensional spaces, (iii) is only as expensive as a matrix multiplication on a V-representation, but requires a doubly-exponential variable elimination algorithm such as Fourier-Motzkin [36] for polytopes in the H-representation.

While it is true in general that splitting a V-representation polytope with a hyperplane is difficult, when restricted to two-dimensional polytopes, it is actually efficient in a V-representation, as demonstrated by Algorithm 3, helping to motivate our use of the V-representation in our algorithm. Our algorithm shows how to do polytope splitting efficiently for two-dimensional polytopes embedded in any dimensional space, i.e., even though the polytopes are two-dimensional, they (and their vertices) live in a much higher-dimensional space.

Furthermore, even though it is easy to split an H-representation polytope, determining when such a split leads to a non-empty polytope requires solving a relatively expensive LP problem. This is exacerbated by the fact that, although the polytopes in question are two-dimensional, they lie within a much higher-dimensional space. This means that the corresponding LP problem will have thousands of variables, even if the actual polytope it describes has at most two dimensions. This significantly increases overhead in the H-representation approach, a problem neatly avoided by specifying the vertices directly in the V-representation.

Comparing performance. To better quantify the performance characteristics of both representations for our particular application area, we evaluated two different operations in the H-representation and compare to our results using the V-representation in Sect. 8.

First, we used an off-the-shelf Fourier-Motzkin implementation [37] to transform a single two-dimensional input polytope through the first layer of the ACAS Xu network as evaluated in Sect. 8.1, except using the H-representation. Transforming even this single polytope requires over 0.1 seconds on modern hardware. Such transformation operations would have to be performed at least once for each of the approximately 30, 000 linear regions identified by SyReNN in Sect. 8.1 and Table 1, leading to almost an hour of solving time compared to 0.1 seconds for the entire run with SyReNN using a V-representation.

Alternatively, a different way to implement SyReNN with H-representation polytopes but avoiding the expensive projection step would be to perform the entire analysis in a space with as many dimensions as DNN nodes. This would avoid projection, but still relies on an LP solver to determine which linear regions, i.e., assignment of activated nodes, are feasible. We performed a similar experiment, using the Gurobi LP solver [38] to identify a linear region of the DNN by iteratively asking the LP solver if there exists an input that causes the ith DNN node to be activated. If so, we modify the LP to assert it is activated and continue to the $(i+1)$th node. Otherwise, we assert it is not activated and again continue to the $(i+1)$th node. Even with a state-of-the-art LP solver, Gurobi solving time for even a single linear region of the network is over 0.3 seconds, which is larger than it takes our V-representation SyReNN to identify over 30, 000 linear regions.

While it is likely that optimizations may reduce the runtime for an H-representation based approach, it is unlikely to make up the four-orders-of-magnitude difference in runtime demonstrated by these experiments. Furthermore, such approaches require the use of complicated polytope projection and feasibility solvers, compared to the relatively simple SplitPlane algorithm used by SyReNN.

Numerical precision. Furthermore, the two polytope representations have different resiliency to floating-point operations. In particular, H-representations for polytopes in ${\mathbb {R}}^n$ are notoriously difficult to achieve high-precision with, because the error introduced from using floating point numbers gets arbitrarily large as one goes in a particular direction along any hyperplane facet. Ideally, we would like the hyperplane to be most accurate in the region of the polytope itself, which corresponds to choosing the magnitude of the norm vector correctly. Unfortunately, to our knowledge, there is no efficient algorithm for computing the ideal floating point H-representation of a polytope, although libraries such as APRON [39] are able to provide reasonable results for low-dimensional spaces. However, because neural networks utilize extremely high-dimensional spaces (often hundreds or thousands of dimensions) and we wish to iteratively apply our analysis, we have found that errors from using floating-point H-representations can quickly multiply and compound to become infeasible. By contrast, floating-point inaccuracies in a V-representation are directly interpretable as slightly misplacing the vertices of the polytope; no “localization” process is necessary to penalize inaccuracies close to the polytope more than those far away from it.

Another difference is in the space complexity of the representation. In general, H-representations can be more space-efficient for common shapes than V-representations. However, when the polytope lies in a low-dimensional subspace of a larger space, the V-representation is usually significantly more efficient.

Thus, V-representations are a good choice for low-dimensionality polytopes embedded in high-dimensional space, which is exactly what we need for analyzing neural networks with two-dimensional restriction domains of interest. This is why we designed our algorithms to rely on $\texttt {Vert}(X)$, so that they could be directly computed on a V-representation. Importantly, our algorithm operates entirely within the V-representation: we never need to convert between them. This is particularly nice when the polytope lies in a two-dimensional subspace, as storing the vertices in counter-clockwise order allows us to recover the edges from the vertices. Meanwhile, converting to a full H-representation would likely incur significant overhead due to the very high-dimensional space the polytope is embedded in.

5 Batched $\textsc {ExtendPWL}$ Algorithm

This section presents Batched $\textsc {ExtendPWL}$ algorithm for computing $f \otimes \widehat{{g}_{\restriction X}}$ for two-dimensional X. f is a PWL function such that the hyperplanes impose a partitioning of the space where f is equivalent to some linear function within any partition. The algorithm is presented in Algorithm 4. The batched nature of the algorithm allows it to exploit GPU-style parallelism. In this algorithm, we introduce the notion of edges of polytopes (1-dimensional faces). $\texttt {Edges}(P)$ returns the set of edges of the polytope P. The algorithm begins by initializing the result Y with $\widehat{{g}_{\restriction X}}$ (Line 1). Each of the following iterations over all $k\in [1,m]$ hyperplanes (Line 2-10) splits each polytope in Y by the kth hyperplane and adds the resulting partitions back to Y. This ensures that, after the kth iteration, none of the polytopes in Y cross the first k hyperplanes. During iteration k, the algorithm first collects all vertices (Line 3) and edges (Line 6) of all polytopes in Y as V and E, respectively. The algorithm then computes a map $\texttt {S}$ from any vertex $v\in V$ to its sign regarding the working hyperplane k (Line 5). With the sign map $\texttt {S}$, the algorithm then identifies edges that cross the kth hyperplane (Line 6) as $E^\times$. $\texttt {CrossPlane}$ checks if the two endpoints of edge e has different signs. Then the algorithm computes a map from each such edge e in $E^\times$ to its intersection vertex with the hyperplane k as $\texttt {I}$ by interpolation (Line 7). The algorithm then collects polytopes p in Y that intersect with the kth hyperplane as $P^\times$ (Line 8), splits each of them using $\textrm{SplitPlane}$ (presented later) and collects all partitions as $P^\varDelta$ (Line 9). The kth iteration ends by replacing intersected polytopes in Y with their partitions regarding the hyperplane k.

The procedure $\textrm{SplitPlane}$ (Line 12–29) splits the polytope p into two halves, one on either side of the kth hyperplane, using the sign map $\texttt {S}$ and intersection map $\texttt {I}$. It begins by initializing the sets pos and neg to contain edges of polytope p which lie on the positive and negative side of the hyperplane k, with empty sets (Line 13), as well as the set $V^\times$, which will contain the vertices lying on the kth hyperplane itself (shared by both partitions), with empty set (Line 14). The procedure then iterates over edges of polytope k (Line 15-26). The iteration for edge e begins by checking if it crosses the hyperplane k (Line 16). If so, the procedure first adds the intersection vertex $\texttt {I}(e)$ to $V^\times$ (Line 17). Then the procedure splits the intersected edge e by the intersection vertex $\texttt {I}(e)$ as new edges $(e.u, \texttt {I}(e))$ and $(e.v, \texttt {I}(e))$ (Line 18), where e.u and e.v are two endpoints of edge e. For each new edge $e'$, the procedure adds $e'$ to the pos set if it is on the positive side of the hyperplane k (Line 19-20), otherwise to the neg set (Line 21-22). If the iterating edge e does not cross hyperplane k, then the procedure adds e to the pos set if it is on the positive side of the hyperplane k (Line 23-24), otherwise to the neg set (Line 25-26). After the iterations, the procedure ends by adding the convex hull of intersected vertices $V^\times$ to both pos and neg (Line 27-28), and returns the set of face hulls of pos and neg (Line 29).

Theorem 3

Algorithm 4 correctly computes $f \otimes \widehat{{g}_{\restriction X}}$.

Proof

It suffices to show that the algorithm correctly partitions each input polytope P such that the signs within a partition are constant. Notably, because of convexity, it suffices to show that the signs of the vertices of each partition are constant.

In iteration k, Algorithm 4 splits all polytopes which cross the hyperplane k and maintains the invariant that each $\textrm{SplitPlane}$ splits an intersected polytope into two new ones such that the signs within each partition regarding hyperplanes [1, k] are constant. This invariant ensures that the algorithm is correct. $\square$

Algorithm 4 is optimized to utilize GPU. Specifically, lines marked by $\star$ (Line 5-8) can be parallelized on GPU and lines marked by $\diamond$ (Line 9) can be parallelized on CPU. Thus, one would expect that this algorithm when executed using a GPU would perform significantly better than the same algorithm on a CPU; we empirically confirm this in Sect. 8.2. Furthermore, we also see that this Batched ExtendPWL algorithm when executed using a GPU outperforms the Ordered ExtendPWL algorithm (2) on a CPU. Two major overheads when using GPU are data movement and kernel launches. To avoid redundant data movement between GPU memory and CPU memory, we maintain vertices as a matrix on GPU memory and only access it from GPU. We also maintain the endpoints of all edges in a contiguous GPU memory. There are only two floating-point computations; viz., computing the signs of vertices and the intersection vertices of the intersected edges. To avoid redundant launches of the GPU kernel, we perform these computations in batches, and cache the results in maps for later use (Line 5 and 7).

6 Extending to higher-dimensional regions

The 2D algorithm described in Sect. 4.1 can be seen as implementing the recursive case of a more general, n-dimensional version of the algorithm that recurses on each of the $(n-1)$-dimensional facets. In 2D, we trace the edges (1D faces) and use the 1D algorithm from [25] to subdivide them based on intersections with the hyperplanes defining the function.

In this section, we will describe the more general n-dimensional recursive algorithm. This generalized algorithm is given in Algorithm 5 and Algorithm 6.

The overall operation of Algorithm 5 is identical to that of Algorithm 2, as we repeatedly split the input polytopes by the hyperplanes until each resulting partition lies in exactly one linear region, i.e., on exactly one side of each hyperplane. The key difference is that now the polytopes are no longer 2D, hence, we can no longer use the 2D-optimized SplitPlane() and instead call the more general SplitHyperPlane[k](P, g, N, b) defined in Algorithm 6.

The rest of the changes occur in Algorithm 6. The goal of this algorithm is to take a polytope P and split it into (at most) two polytopes $P_1$ and $P_2$, such that each $P_i$ lies entirely on one side of the hyperplane defined by $Nx \le b$.

In the one-dimensional base case, this is relatively simple, as we can directly compute the point m at which the line interpolating between the endpoints s, e of the one-dimensional polytope (line segment) P crosses the hyperplane.

In the n-dimensional recursive case, we recurse on each facet of P. We then partition each of those facets into sub-facets $F_1, F_2$ such that each sub-facet lies on entirely one side of the hyperplane. We collect all of the sub-facets that lie on one side into the set l and those that lie on the other side into the set g. Then B collects the vertices that lie on the border, i.e., $\texttt {ConvexHull}(B) = P \cap \{ x \mid Nx = b \}$. Now, consider the surfaces of our desired partitions $P_1$ and $P_2$. Every point on the surface of $P_1$ is either a point on the surface of P that lies on one side of the hyperplane (i.e., in one of the l facets), or it is a point on the intersection $\texttt {ConvexHull}(B)$. Therefore, $\textrm{FaceHull}(l)$ gives a satisfying $P_1$ and $\textrm{FaceHull}(u)$ a satisfying $P_2$.

We have experimented with such approaches, but found that the overhead of keeping track of all $(n-k)$-dimensional faces (commonly known as the face poset or combinatorial structure [40] of a polytope) was too large in higher dimensions. The two-dimensional algorithm addresses this concern by storing the combinatorial structure implicitly, representing 2D polytopes by their vertices in counter-clockwise order, from which edges correspond exactly to sequential vertices. To our knowledge, such a compact representation allowing arbitrary $(n-k)$-dimensional faces to be read off is not known for higher-dimensional polytopes.

Theorem 4

Algorithm 6 correctly splits a polytope $\texttt {ConvexHull}(V)$ by the hyperplane $Nx = b$.

Proof

In the $k = 1$ case, we have two options:

• If both endpoints are on the same side of the hyperplane, then the splitting is just the polytope (line segment) itself, so we return $\{ P \}$ correctly.

• Otherwise, we wish to split the line segment P defined by $s + \alpha (e - s)$ by the intersecting, non-parallel line defined by $Nx = b$. This intersection point can be computed algebraically to be the point m as shown, leaving the two partition segments $\texttt {ConvexHull}(\{ s, m \})$ and $\texttt {ConvexHull}(\{ m, e \})$ returned.

Next, the recursive case. Notice that the algorithm only ever partitions polytopes (never adding new points outside the input polytope), so $\textrm{FaceHull}(l) \cup \textrm{FaceHull}(u) \subseteq P$.

Therefore, it suffices to show that the facets in l form the surface of $L = P \cap \{ x \mid Nx \le b \}$ and the facets in u form the surface of $U = P \cap \{ x \mid Nx \ge b \}$. We will argue for l here, u is analogous.

Consider any point x on the surface of L. Either (i) x is also on the surface of P, or (ii) x is interior to P, and thus must be on the facet $P \cap \{ x \mid Nx = b \}$.

Case (i) implies x will be on some facet F of P, and thus x will be in the sub-facet $F_l$ of F intersected with the lower-half L. This facet is included in l by line 13.

Case (ii) implies x will be on $P \cap \{ x \mid Nx = b \}$. Notice that this is a single facet, hence its vertices will all be adjacent to other facets. Hence, each of the vertices will be added to set B on line 11. So these points will be in $\texttt {ConvexHull}(B)$, and thus in l as of line 16.

Therefore, all of the surface points are accounted for in the facet sets and therefore the returned polytopes are supersets of the desired $P_1$, $P_2$. We already saw that they are also subsets, hence they are the desired partitions $P_1$ and  $P_2$. $\square$

Theorem 5

Algorithm 5 correctly computes $f \otimes \widehat{{g}_{\restriction X}}$.

Proof

It suffices to show that the algorithm correctly partitions each input polytope P such that the signs within a partition are constant. Notably, because of convexity, it suffices to show that the signs of the vertices of each partition are constant.

We maintain two invariants every time we process some polytopes from the queue. The first is that the corresponding polytope will only be added to Y if the signs of all vertices are constant (or zero). The second is that at each step, we partition the polytope into two new ones (using SplitPlane) such that fewer sign switches happen in each than the original polytope. This follows from the correctness of the SplitPlane algorithm.

The first invariant ensures that, if it halts, the algorithm is correct. The second ensures that it will halt, as there are finitely many dimensions to consider. $\square$

7 SyReNN tool

This section provides more details about the design and implementation of our tool, SyReNN (Symbolic Representations of Neural Networks), which computes $\widehat{{f}_{\restriction X}}$, where f is a DNN using only piecewise-linear layers and X is a union of one- or two-dimensional polytopes. The tool is available under the MIT license at https://github.com/95616ARG/SyReNN_GPU.

Input and output format. SyReNN supports reading DNNs from two standard formats: ERAN (a textual format used by the ERAN project [41]) as well as ONNX (an industry-standard format supporting a wide variety of different models) [42]. Internally, the input DNN is described as an instance of the Network class, which is itself a list of sequential Layers. A number of layer types are provided by SyReNN, including FullyConnectedLayer, ConvolutionalLayer, and ReLULayer. To support more complicated DNN architectures, we have implemented a ConcatLayer, which represents a concatenation of the output of two different layers. The input region of interest, X, is defined as a polytope described by a list of its vertices in counter-clockwise order. The output of the tool is the symbolic representation  $\widehat{{f}_{\restriction X}}$.

Overall architecture. We designed SyReNN in a client–server architecture using gRPC [43] and protocol buffers [44] as a standard method of communication between the two. This architecture allows the bulk of the heavy computation to be done in efficient C++ code, while allowing user-friendly interfaces in a variety of languages. It also allows practitioners to run the server remotely on a more powerful machine if necessary. The C++ server implementation uses the Intel TBB library for parallelization. Our front-end library pysyrenn is written in Python. The entire project can be built using the Bazel build system.

Server architecture. The major algorithms are implemented as a gRPC server written in C++. When a connection is first made, the server initializes the state with an empty DNN $f(x) = x$. During the session, three operations are permitted: (i) append a layer g so that the current session’s DNN is updated from $f_0$ to $f_1(x) :=g(f_0(x))$, (ii) compute $\widehat{{f}_{\restriction X}}$ for a one-dimensional X, or (iii) compute $\widehat{{f}_{\restriction X}}$ for a two-dimensional X. We have separate methods for one- and two-dimensional X, because the one-dimensional case has specific optimizations for controlling memory usage. The SegmentedLine and UPolytope types are used to represent one- and two-dimensional partitions of X, respectively. When operation (i) is performed, a new instance of the LayerTransformer class is initialized with the relevant parameters and added to a running vector of the current layers. When operation (ii) is performed, a new queue of SegmentedLines is constructed, corresponding to X, and the before-allocated LayerTransformers are applied sequentially to compute $\widehat{{f}_{\restriction X}}$. In this case, extra control is provided to automatically gauge memory usage and pause computation for portions of X until more memory is made available. Finally, when operation (iii) is performed, a new instance of UPolytope is initialized with the vertices of X and the LayerTransformers are again applied sequentially to compute $\widehat{{f}_{\restriction X}}$. In this case, SyReNN can optimize the memory layout of UPolytopes and LayerTransformers for GPU as well as perform the GPU-based algorithm if the client asks for it.

Client architecture. Our Python client exposes an interface for defining DNNs similar to the popular Sequential-Network Keras API [45]. Objects represent individual layers in the network, and they can be combined sequentially into a Network instance. The key addition of our library is that this Network exposes methods for computing $\widehat{{f}_{\restriction X}}$ given a V-representation description of X. To do this, it invokes the server and passes a layer-by-layer description of f followed by the polytope X, then parses the response $\widehat{{f}_{\restriction X}}$.

Extending to support different layer types. Different layer types are supported by sub-classing the LayerTransformer class. Instances of this class expose a method for computing $\textsc {ExtendPWL}{}(h, \cdot )$ for the corresponding layer h. To simplify implementation, two sub-classes of LayerTransformer are provided: one for linear layers (such as fully-connected and convolutional layers), and one for piecewise-linear layers. For linear layers, all that needs to be provided is a method computing the layer function itself. For piecewise-linear layers, two methods need to be provided: (i) computing the layer function itself, and (ii) describing the hyperplanes which separate the linear regions. The base class then directly implements Algorithm 2 for that layer. At least one CPU and one GPU implementation should be provided. This architecture makes supporting new layers a straight-forward process.

Fig. 4

Visualization of decision boundaries for the ACAS Xu network using three different approaches. Using SyReNN (left) quickly produces the exact decision boundaries. Using abstract interpretation-based tools like DeepPoly (middle and right) is slower and produces only imprecise approximations of the decision boundaries. k gives the number of partitions used by the DeepPoly algorithm, impacting the coarseness of the resulting approximation

Float safety. Like Reluplex [46], SyReNN uses floating-point arithmetic to compute $\widehat{{f}_{\restriction X}}$ efficiently. Unfortunately, this means that in some cases its results will not be entirely precise when compared to a real-valued or multiple-precision version of the algorithm. If a perfectly precise solution is required, the server code can be modified to use multiple-precision rationals instead of floats. Alternatively, a confirmation pass can be run using multiple-precision numbers after the initial float computation to confirm the accuracy of its results. The use of over-approximations may also be explored for ensuring correctness with floating-point evaluation, like in DeepPoly [27]. Unfortunately, our algorithm does not directly lift to using such approximations, since they may blow the originally-2D region into a higher-dimensional (but very “flat”) over-approximate polytope, preventing us from applying the 2D algorithm for the next layer.

Usage examples. The tool user will begin by loading a model from disk, like

We can use this network to compute the network on finite input points like so

Or we can compute the behavior of the network on all points between and like so:

Here, is a Numpy array where each element is an endpoint between and , defining the partitioning $\widehat{{f}_{\restriction X}}$. The option allows us to avoid re-computing the DNN on those endpoints, if its output is important:

Meanwhile, controls whether the preimages will be relative (a ratio between 0 and 1) or absolute (a point between and ).

Similarly, given the vertices of a 2D polytope, we can compute the $\widehat{{f}_{\restriction X}}$ like so

The resulting variable will be a list of partitions, which each partition being an array of its vertices.

8 Applications of SyReNN

This section presents the use of SyReNN in four example case studies.

8.1 Visualization of decision boundaries for ACAS Xu networks

Table 1 Comparing the performance of DNN visualization using SyReNN versus DeepPoly for the ACAS Xu network [5]. $\widehat{{f}_{\restriction X}}$ size is the number of partitions in the symbolic representation. SyReNN time is the time taken to compute $\widehat{{f}_{\restriction X}}$ using SyReNN. ${{\,\textrm{DeepPoly}\,}}[k]$ time is the time taken to compute DeepPoly for approximating decision boundaries with k partitions. Each scenario represents a different two-dimensional slice of the input space; within each slice, the heading of the intruder relative to the ownship along with the speed of each involved plane is fixed

Our first major task is visualizing the decision boundaries of a DNN on infinitely many input points. Figure 4 shows a visualization of an ACAS Xu DNN [5] which takes as input the position of an airplane and an approaching attacker, then produces as output one of five advisories instructing the plane, such as “clear of conflict” or to move “weak left.” Every point in the diagram represents the relative position of the approaching plane, while the color indicates the advisory.

One approach to such visualizations is to simply sample finitely many points and extrapolate the behavior on the entire domain from those finitely many points. However, this approach is imprecise and risks missing vital information because there is no way to know the correct sampling density to use to identify all important features.

Another approach is to use a tool such as DeepPoly [27] to over-approximate the output range of the DNN. However, because DeepPoly is a coarse over-approximation, there may be regions of the input space for which it cannot state with confidence the decision made by the network. In fact, the approximations used by DeepPoly are extremely coarse. A naïve application of DeepPoly to this problem results in it being unable to make claims about any of the input space of interest. In order to utilize it, we must partition the space and run DeepPoly within each partition, which significantly slows down the analysis. Even when using $25^2$ partitions, Fig. 4b shows that most of the interesting region is still unclassifiable with DeepPoly (shown in white). Only with $100^2$ partitions can DeepPoly effectively approximate the decision boundaries, although it is still quite imprecise.

By contrast, SyReNN can be used to exactly determine the decision boundaries on any 2D polytope subset of the input space, which can then be plotted. This is shown in Fig. 4a. Furthermore, as shown in Table 1, the approach using SyReNN is significantly faster than that using DeepPoly, even as we get the precise answer instead of an approximation. Such visualizations can be particularly helpful in identifying issues to be fixed using techniques such as those in Sect. 8.3.

Implementation. The helper class PlanesClassifier is provided by our Python client library. It takes as input a DNN f and an input region X, then computes the decision boundaries of f on X.

The MNIST and CIFAR-10 DNNs used are from the ERAN project [41], and more details about the models are available on the ERAN repository. For example, the MNIST $3\times 100$ model has three layers and 210 nodes, while the MNIST $9\times 200$ model has nine layers with 1610 nodes. The ACAS Xu networks have 300 nodes each [46].

Performance evaluation. Timing comparisons are given in Table 1. We see that SyReNN is quite performant, and the time taken to compute the exact SyReNN is negligible even comparing with the coarsest approximation from DeepPoly using $25^2$ partitions. Experiments were performed on an Intel Core i9-9960X with 32 cores at 4.4GHz and 128GB of memory.

8.2 Visualization of decision boundaries for image recognition networks

Table 2 Pretrained MNIST and CIFAR-10 models used to evaluate the performance of DNN visualization using different implementations. $\widehat{{f}_{\restriction X}}$ is the number of partitions in the symbolic representation. #Neurons is the number of neurons. #Split is the number (in millons) of calls to SplitPlane in batched ExtendPWL Algorithm 4

Fig. 5

Visualization of decision boundaries for the MNIST networks

Table 3 Total time for computing $\widehat{{f}_{\restriction X}}$ of X using SyReNN for image recognition networks. The parenthesized number is speed up comparing to Ordered-CPU

This section compares the performance of the ordered ExtendPWL (Algorithm 2) implemented on CPU against the batched ExtendPWL (Algorithm 4) implemented on both CPU and GPU, in visualization tasks for larger image recognition networks including MNIST and CIFAR-10. Table 2 shows the pretrained models we used from ERAN [41]. All models only use the ReLU activation function. The models labeled with $m\times n$ are fully-connected feed-forward neural networks with m layers in total, n neurons at each hidden layer. MNIST ConvSmall is a four-layer convolutional network with 3, 604 neurons. The input plane we chose to visualize for all MNIST networks or all CIFAR-10 networks are the same respectively. The MNIST networks take as input a $28\times 28$ image of a handwritten digit embedded in a 784-dimensional input space, and predict the digit. The CIFAR-10 DNNs take as input a $32\times 32$ color image embedded in a 3, 072-dimensional input space, and predict one of ten labels including “airplane”, “bird”, “dog”, etc. Figure 5 visualizes the decision boundaries of four MNIST networks over the same input plane (which correspond to the first four rows in Table 3). The diagrams present the classified input planes computed using SyReNN in its two-dimensional subspace. Every point inside the triangle formed by the three input images represents an image interpolated from the three vertex images, while the color indicates the classification.

Performance evaluation. All experiments were performed on an Intel Core i9-9960X with 32 cores at 4.4GHz with 128GB of memory and Titan RTX with 24GB of GPU memory.

Table 4 Total time spent in ExtendPWL when computing $\widehat{{f}_{\restriction X}}$ of X using SyReNN for image recognition networks. The parenthesized number is speed up comparing to Ordered-CPU

Table 3 shows the total time taken to compute SyReNN using different implementations of ExtendPWL. The Ordered-CPU column uses the Ordered ExtendPWL algorithm (Algorithm 2) on a CPU; the Batched-CPU and Batched-GPU columns use the Batched ExtendPWL algorithm (Algorithm 4) on a CPU and a GPU, respectively. All three implementations exploit multi-threading on CPU; additionally Batched-GPU exploits CUDA on GPU.

For all but the smallest two networks (MNIST $3\times 100$ and CIFAR-10 $4\times 100$), Batched-GPU is significantly faster than Ordered-CPU. For those two small networks the total SyReNN time is negligible; the slowdown of Batched-GPU could be attributed to the overhead of using the GPU (e.g., kernel launch time).

Except for MNIST $9\times 200$ network, Ordered-CPU outperforms Batched-CPU. Batched-CPU and Ordered-CPU should have the same performance in computing linear layers. Thus, one can infer that the slowdown of Batched-CPU can be attributed to the poor performance of Batched ExtendPWL (Algorithm 4) compared to that of Ordered ExtendPWL (Algorithm 2). Specifically, the implementation of Ordered ExtendPWL uses pipeline parallelism, which is better suited for the CPU. In contrast, the batched parallelism in Batched ExtendPWL is ill suited for the CPU. Consequently, we see that the Batched-GPU is significantly faster than Batched-CPU.

Table 4 shows the time spent in ExtendPWL when computing SyReNN. The Ordered-CPU column uses the Ordered ExtendPWL algorithm (Algorithm 2) on a CPU; the Batched-CPU and Batched-GPU columns use the Batched ExtendPWL algorithm (Algorithm 4) on a CPU and a GPU, respectively. For all but the smallest two networks (MNIST $3\times 100$ and CIFAR-10 $4\times 100$), Batched-GPU is significantly faster than Ordered-CPU. Thus, we can conclude that the speedup of SyReNN when using Batched-GPU compared to Ordered-CPU (as seen in Table 3) cannot only be attributed to the fact that the computation of the linear layers is significantly faster on a GPU owing to faster matrix multiplications; the use of the Batched ExtendPWL plays an important role in achieving the speedup.

8.3 Provable repair of DNNs

We have so far seen how SyReNN can be used to analyze trained DNNs and better understand their behavior. A natural next step is to repair DNNs to remove buggy behavior. In this section, we briefly describe Provable Repair of DNNs [30], and show how SyReNN forms a key component of Provable Polytope Repair of DNNs.

Traditional methods for fixing DNNs involve simply re-training the DNN while focusing on the identified-buggy points. However, this approach has a number of issues. First, it does not provide any guarantees that a repair will be found. This is exacerbated by the many hyperparameters involved with DNN re-training, so the user must try many combinations hoping that one works. Second, even if a repair is found, it does not provide any guarantee that this is the smallest repair — indeed, DNNs often over-correct, forgetting things they learned earlier, causing drawdown, or a degradation of accuracy on the original dataset after re-training. Finally, re-training operates inherently on finitely many input points at a time, whereas we often want to guarantee a DNN’s behavior on infinitely many inputs, as described below.

Fig. 6

Natural adversarial example [47]

Pointwise Repair. The simplest setting for repair is what we call pointwise repair. In the image recognition case, pointwise repair consists of correcting the DNN so it assigns the correct classification to every one of a set of finitely many input images. For example, [47] describes a dataset of Natural Adversarial Examples, i.e., challenging images that many state-of-the-art image recognition models fail to correctly classify. An example of such an image is given in Fig. 6. We can use provable pointwise repair to find a minimal modification to a given DNN that causes it to correctly classify those images.

The key theory behind pointwise DNN repair we will use was developed in [30]. In that work, we consider the satisfiability problem corresponding to the single-layer pointwise DNN repair. In essence, we can describe the DNN’s output as an equation in terms of the input points and the weights of the DNN. We then want to solve these equations for the weights that produce the desired outputs on the given inputs. The key source of non-linearity is that, even if the input is fixed, changing a weight in the DNN can change which nodes are activated or inactivated, i.e., more generally, which linear region each of the intermediate vectors in the DNN’s evaluation falls into.

To address this, [30] introduced a new DNN architecture called Decoupled DNNs (DDNNs), where there are two sets of weights: the activation weights and the value weights. The former have sole control over which nodes are activated, while the latter have sole control over what the nodes output if they are activated. Once the weights are decoupled in this manner, we see that changing the value weights alone will never change which nodes are activated or inactivated, and this turns out to be enough to make the single-layer repair problem linear (thus solvable in polynomial time) for DDNNs. This is summarized by the following theorem, reproduced from [30]:

Theorem 6

Let N be a DDNN with layers $(W^{(a, i)}, W^{(v, i)}, \sigma ^{(i)})$ and fix an index j. Then, for any $\vec {v}$, $N(\vec {v})$ varies linearly as a function of $W^{(v, j)}$.

Fortunately, there is a simple, syntactic procedure to convert any DNN into an equivalent DDNN. Thus, we can take the user-provided DNN, convert it to a DDNN, and then repair the DDNN as a linear programming problem using off-the-shelf solvers such as Gurobi [38].

Fig. 7

Fog-corrupted digit [48]

Polytope Repair. A more challenging setting for repair is polytope repair. For this, we consider an image classifier that has been trained to correctly recognize digits in clear images, and want to modify this classifier so it also correctly classifies foggy variants of those images (Fig. 7). The key is that we want to ensure it works no matter the level of fog corruption applied. In pixel space, a single image forms a point and the set of all foggy variants of that image forms a line segment, with each point on the line segment corresponding to the image with some percent of fog applied. We can use provable polytope repair to find a minimal modification to a given DNN that causes it to classify all of the points on those lines correctly.

The key result we need for polytope repair of DDNNs was presented in [30]:

Theorem 7

Let N be a PWL DNN with layers $(W^{(i)}, \sigma ^{(i)})$ and define a DDNN M with layers $(W^{(i)}, W^{(v, i)}, \sigma ^{(i)})$. Then, within any linear region of the DNN N, the DDNN M is also linear.

This theorem states that modifications to the value weights in a DDNN do not change the partitioning of the SyReNN for the DDNN. Recall further that, by definition, the DDNN behaves linearly within each SyReNN partition, and due to properties of linear maps, we can say that the entire partition satisfies some linear constraint if and only if its finitely many vertex points do. Thus, as these partitions do not change during repair for a DDNN, provable polytope repair reduces to provable pointwise repair on the finitely many vertices of the linear regions. The key is that one must compute those vertex points, but this is exactly what SyReNN allows us to do.

Case Studies. Here we report on three case studies from [30]. In the first, Provable Repair was used to repair an image-recognition network that struggled to classify a set of challenging images. In the second, Provable Repair was used to repair a digit-recognition network that struggled to classify images with varying amounts of fog applied. Finally, the third uses Provable Repair to enforce a safety specification on the ACAS Xu DNN seen in Sect. 8.1.

Table 5 Summary of experimental results for task 1. D: Drawdown (%), T: Time, BD: Best Drawdown, PR: Provable Repair, FT: Fine-Tuning baseline

Table 6 Summary of experimental results for task 2. D: Drawdown (%), G: Generalization (%), T: Time, PR: provable repair, FT: fine-tuning baseline. $*$ means fine-tuning diverged and timed out after 1000 epochs, the results shown are from the last iteration of fine-tuning before the timeout

Implementation. The DNN Repair code is available as a separate Python library called PRDNN that interfaces with our Python client. It takes as input a DNN f and pairs of input region, output label $X_i, Y_i$, then computes a new DNN $f'$ which maps all points in each $X_i$ into $Y_i$.

Baseline. We compared against a baseline using fine-tuning, i.e., re-training the DNN with the buggy inputs until they are all correctly classified. We discuss a variety of alternative repair methods in Sect. 9; to our knowledge, almost none have publicly-available implementations, none support the guarantees of time complexity and completeness that PRDNN does, and none support provable polytope repair.

Empirical results. Results for the challenging-images task are summarized in Table 5. Results for the foggy-digits task are summarized in Table 6. Drawdown is the drop in accuracy on the original dataset, while generalization is the increase in accuracy on points that are misclassified by the buggy network in a similar way to those repaired on.

For the aircraft collision-avoidance task, Provable Polytope Repair succeeded in under 22 seconds, with zero drawdown and $95\%$ generalization. Meanwhile, the fine-tuning baseline timed out after over 1 hour, and had negative efficacy; while the original network misclassified only 3 points in the sampled repair set, the FT-repaired network misclassified 181 points; $12\%$ drawdown; and $96\%$ generalization.

8.4 Integrated gradients

A common problem in the field of explainable machine learning is understanding why a DNN made the prediction it did. For example, given an image classified by a DNN as a ‘cat,’ why did the DNN decide it was a cat instead of, say, a dog? Were there particular pixels which were particularly important in deciding this? Integrated Gradients (IG) [31] is the state-of-the-art method for computing such model attributions.

Definition 5

Given a DNN f, the integrated gradients along dimension i for input x and baseline $x'$ is defined to be:

$$\begin{aligned} IG_i(x) {\tiny {def}} \over =(x_i - x_i') \times \int _{\alpha =0}^{1}\frac{ \partial f(x' + \alpha \times (x-x') )}{\partial x_i}d\alpha . \end{aligned}$$

(2)

The computed value $IG_i(x)$ determines relatively how important the ith input (e.g., pixel) was to the classification.

However, exactly computing this integral requires a symbolic, closed form for the gradient of the network. Until [25], it was not known how to compute such a closed-form and so IGs were always only approximated using a sampling-based approach. Unfortunately, because it was unknown how to compute the true value, there was no way for practitioners to determine how accurate their approximations were. This is particularly concerning in fairness applications where an accurate attribution is exceedingly important.

In [25], it was recognized that, when $X = \texttt {ConvexHull}(\{ x, x' \})$, $\widehat{{f}_{\restriction X}}$ can be used to exactly compute $IG_i(x)$. This is because within each partition of $\widehat{{f}_{\restriction X}}$ the gradient of the network is constant because it behaves as a linear function, and hence the integral can be written as the weighted sum of such finitely many gradients. Using our symbolic representation, the exact IG can thus be computed as follows:

$$\begin{aligned}{} & {} \sum _{\texttt {ConvexHull}(\{ y_i, y'_i \}) \in \widehat{{f}_{\restriction \texttt {ConvexHull}(\{ x, x' \})}}} (y'_i - y_i) \nonumber \\ {}{} & {} \times \frac{\partial f(0.5\times (y_i + y'_i))}{\partial x_i} \end{aligned}$$

(3)

Where here $y_i, y'_i$ are the endpoints of the segment with $y_i$ closer to x and $y'_i$ closest to $x'$.

Implementation. The helper class IntegratedGradientsHelper is provided by our Python client library. It takes as input a DNN f and a set of $(x, x')$ input-baseline pairs and then computes IG for each pair.

Empirical results. In [25] SyReNN was used to show conclusively that existing sampling-based methods were insufficient to adequately approximate the true IG. This realization led to changes in the official IG implementation to use the more-precise trapezoidal sampling method we argued for.

Timing numbers. In those experiments, we used SyReNN to compute $\widehat{{f}_{\restriction X}}$ for three different DNNs f, namely the small, medium, and large convolutional models from [41]. For each DNN, we ran SyReNN on 100 one-dimensional lines. The 100 calls to SyReNN completed in 20.8 s for the small model, 183.3 for the medium model, and 615.5 for the big model. Tests were performed on an Intel Core i7-7820X CPU at 3.60GHz with 32GB of memory.

9 Related work

SyReNN Primitive. The related problem of exact reach set analysis for DNNs was investigated in [49]. However, the authors use an algorithm that appears to suggest explicitly enumerating all exponentially-many ( $2^n$) possible signs at each ReLU layer. By contrast, our algorithm adapts to the actual input polytopes, efficiently restricting its consideration to activations that are actually possible. Furthermore, they focus on the particular problem of reach set analysis for full-dimensional subsets of the DNN’s input domain, whereas the key focus of SyReNN is enabling analyses such as IG, visualization, and repair that rely on precise and efficient analysis of low-dimensional subsets of the input domain. These differences in focus become clear in the evaluation, where the approach of [49] takes multiple minutes to identify 1250 linear regions, while SyReNN identifies tens of thousands of lower-dimensional linear regions in less than a second (Sect. 8). Newer algorithms and representations [50] may further improve the performance of higher-dimensional exact analysis in the future, however we expect techniques specialized to the low-dimensional case to continue to be significantly faster.¹ Thus, the choice of which approach to use is mostly driven by application domain constraints, e.g., the applications in Sect. 8 were inherently low-dimensional.

Hanin and Rolnick [51] prove theoretical properties about the cardinality of $\widehat{{f}_{\restriction X}}$ for ReLU networks, showing that $\left| \widehat{{f}_{\restriction X}}\right|$ is expected to grow polynomially with the number of nodes in the network for randomly-initialized networks.

Thrun [52] and Bastani et al. [53] extract symbolic rules meant to approximate DNNs, which can approximate the symbolic representation $\widehat{{f}_{\restriction X}}$.

DNN Visualization and Understanding. Integrated Gradients was first proposed by [31], however they used a Riemann sum approximation instead of computing it exactly. The one-dimensional version of SyReNN [25] was the first approach able to exactly compute IG.

The ERAN [41] tool and underlying DeepPoly [27] domain were designed to verify the non-existence of adversarial examples. Breutel et al. [54] give an iterative refinement algorithm for an overapproximation of the weakest precondition as a polytope where the required output is also a polytope.

Scheibler et al. [55] verify the safety of a machine-learning controller using the SMT-solver iSAT3, but support small unrolling depths and basic safety properties. Zhu et al. [56] use a synthesis procedure to generate a safe deterministic program that can enforce safety conditions by monitoring the deployed DNN and preventing potentially unsafe actions. The presence of adversarial and fooling inputs for DNNs as well as applications of DNNs in safety-critical systems has led to efforts to verify and certify DNNs [27, 28, 46, 57,58,59,60,61,62]. Approximate reachability analysis for neural networks safely overapproximates the set of possible outputs [28, 49, 50, 61, 63,64,65].

Given polytopes in the output space, Yang et al. [66] compute the exact set of corresponding input polytopes. Their technique is restricted to DNNs with ReLU but supports polytopes in arbitrary-dimensional subspaces. They utilize the facet-vertex incidence matrix (FVIM), which is a compact representation of convex polytopes.

Provable Repair. Prior work in the area of network repair focuses on enforcing constraints on the network during training. DiffAI [67] is an approach to train neural networks that are certifiably robust to adversarial perturbations. DL2 [68] allows for training and querying neural networks with logical constraints.

The layer-wise repair process described in [29] is most similar to the one described in this paper. The key advantage of our approach is the use of Decoupled DNNs. Decoupled DNNs allow for both guaranteed polytope repair as well as guaranteed polynomial-time pointwise repair, neither of which is guaranteed by any other system that we are aware of. Furthermore, to our knowledge, the repair system in [29] is not publicly available for comparison. In theory, any pointwise repair algorithm (such as the one in [29]) could be used along with Decoupled DNNs in order to enable polytope repair.

10 Conclusion

We presented SyReNN, a tool for understanding and analyzing DNNs. Given a piecewise-linear network and a low-dimensional polytope subspace of the input space, SyReNN computes a symbolic representation that decomposes the behavior of the DNN into finitely many linear functions. We showed how to efficiently compute this representation, and presented the design of the corresponding tool. We illustrated the utility of SyReNN on three application domains: visualizing the behavior of DNNs, repairing DNNs, and computing exact IG.

In contrast to prior work, SyReNN explores a unique point in the design space of DNN analysis tools. Instead of trading off precision of the analysis for efficiency, SyReNN focuses on analyzing DNN behavior on low-dimensional subspaces of the domain, for which we can provide both efficiency and precision.