# Traversing the Local Polytopes of ReLU Neural Networks: A Unified Approach
for
Network Verification

Shaojie Xu, Joel Vaughan, Jie Chen, Aijun Zhang, Agus Sudjianto The authors
are with Wells Fargo & Company. The views expressed in the paper are those of
the authors and do not represent the views of Wells Fargo.

###### Abstract

Although neural networks (NNs) with ReLU activation functions have found
success in a wide range of applications, their adoption in risk-sensitive
settings has been limited by the concerns on robustness and interpretability.
Previous works to examine robustness and to improve interpretability partially
exploited the piecewise linear function form of ReLU NNs. In this paper, we
explore the unique topological structure that ReLU NNs create in the input
space, identifying the adjacency among the partitioned local polytopes and
developing a traversing algorithm based on this adjacency. Our polytope
traversing algorithm can be adapted to verify a wide range of network
properties related to robustness and interpretability, providing an unified
approach to examine the network behavior. As the traversing algorithm
explicitly visits all local polytopes, it returns a clear and full picture of
the network behavior within the traversed region. The time and space
complexity of the traversing algorithm is determined by the number of a ReLU
NN’s partitioning hyperplanes passing through the traversing region.

###### Index Terms:

ReLU NNs, Piecewise-Linear NNs, Adversarial Attack, Robustness,
Interpretability, Network Verification

##  I Introduction & Related Work

Neural networks with rectified linear unit activation functions (ReLU NNs) are
arguably the most popular type of neural networks in deep learning. This type
of network enjoys many appealing properties including better performance than
NNs with sigmoid activation [1], universal approximation ability [2, 3, 4, 5],
and fast training speed via scalable algorithms such as stochastic gradient
descent (SGD) and its variants [6].

Despite their strong predictive power, ReLU NNs have seen limited adoption in
risk-sensitive settings [7]. These settings require the model to make robust
predictions against potential adversarial noise in the input [8, 9, 10, 11].
The alignment between model behavior and human intuition is also desirable
[12]: prior knowledge such as monotonicity may be incorporated into model
design and training [13, 14, 15, 16]; users and auditors of the model may
require a certain degree of explanations of the model predictions [17, 18].

The requirements in risk-sensitive settings has motivated a great amount of
research on verifying certain properties of ReLU NNs. These works often
exploit the piecewise linear function form of ReLU NNs. In [19] the robustness
of a network is verified in very small input region via linear programming
(LP). To consider the non-linearity of ReLU activation functions, [20, 21, 22,
23] formulated the robustness verification problem as a satisfiability modulo
theories (SMT) problem. A more popular way to model ReLU nonlinearality is to
introduce a binary variable representing the on-off patterns of ReLU neurons.
Property verification can then be solved using mixed-integer programming (MIP)
[24, 25, 15, 26, 27].

The piecewise linear functional form of ReLU NNs also creates distinct
topological structures in the input space. Previous studies have shown that a
ReLU NN partitions the input space into convex polytopes and has one linear
model associated with each polytope [4, 28, 29, 30, 31, 32]. Each polytope can
be coded by a binary activation code, which reflects the on-off patterns of
the ReLU neurons. The number of local polytopes is often used as a measure of
the model’s expressivity [33, 3]. Built upon this framework, multiple studies
[31, 34, 35] tried to explain the behavior of ReLU NNs and to improve their
interpretability. They viewed ReLU NN as a collection of linear models.
However, the relationship among the local polytopes and their linear models
was not fully investigated.

When the network’s behavior within some specific region in the input space is
of interest, one can collect all the local polytopes overlapped with the
region to conduct analysis. The methods to collect these polytopes can be
categorized into top-down and bottom-up approaches. The top-down approaches in
[36, 32] pass the entire region of interest through a ReLU NN and calculate
how the hyperplanes corresponding to the neurons partition the region into
local polytopes. The major drawback of the top-down approach is that the
analysis must start after the computationally expensive forward passing is
fully finished.

One the contrary, the bottom-up approaches start from a point of interest
inside the region, moving from one local polytope to another while running the
analysis, and can be stopped at any time. [37, 38] achieved the movement among
polytopes by generating a sequence of samples in the input space using
randomized local search. Although being computationally simple, this sample-
based method does not guarantee covering all polytopes inside the region of
interest. The most recent work and also the closest to ours is [39], where
polytope boundaries and adjacency are identified using LP, and the traversing
is done directly on the polytopes.

In this paper, we explore the topological relationship among the local
polytopes created by ReLU NNs. We propose algorithms to identify the adjacency
among these polytopes, based on which we develop traversing algorithms to
visit all polytopes within a bounded region in the input space. Compared with
[39], our polytope traversing algorithm exploits ReLU NNs’ hierarchical
partitioning of the input space to reduce computational overhead and
accelerates the discovering of adjacent polytopes. The thoroughness of our
traversing algorithm is proved. Our paper has the following major
contributions:

  1. 1.

The polytope traversing algorithm provides a unified framework to examine the
network behavior. Since each polytope contains a linear model whose properties
are easy to verify, the full verification on a bounded domain is achieved
after all the covered polytopes are visited and verified. We provide
theoretical guarantees on the thoroughness of the traversing algorithm.

  2. 2.

Property verification based on the polytope traversing algorithm can be easily
customized. Identifying the adjacency among the polytopes is formulated as LP.
Within each local polytope, the user has the freedom to choose the solver most
suitable for the verification sub-problem. We demonstrate that many common
applications can be formulated as convex problems within each polytope.

  3. 3.

Because the polytope traversing algorithm explicitly visits all the local
polytopes, it returns a full picture of the network behavior within the
traversed region and improves interpretability.

Although we focus on ReLU NN with fully connected layers through out this
paper, our polytope traversing algorithm can be naturally extended to other
piecewise linear networks such as those containing convolutional and
maxpooling layers.

The rest of this paper is organized as follows: Section II reviews how
polytopes are created by ReLU NNs. Section III introduces two related
concepts: the boundaries of a polytope and the adjacency among the polytopes.
Our polytope traversing algorithm is described in Section IV. Section V
demonstrates several applications of adapting the traversing algorithm for
network property verification. Two specific cases studies are shown in Section
VI. The paper is concluded in Section VII.

##  II The Local Polytopes in ReLU NNs

###  II-A The case of one hidden layer

A ReLU NN partitions the input space $\mathbb{R}^{P}$ into several polytopes
and forms a linear model within each polytope. To see this, we first consider
a simple NN with one hidden layer of $M$ neurons. It takes an input
$\boldsymbol{x}\in\mathbb{R}^{P}$ and outputs
$\boldsymbol{o}\in\mathbb{R}^{Q}$ by calculating:

$\begin{split}\boldsymbol{o}=\boldsymbol{W}^{o}\boldsymbol{h}+\boldsymbol{b}^{o}&=\boldsymbol{W}^{o}\left(\sigma(\boldsymbol{W}\boldsymbol{x}+\boldsymbol{b})\right)+\boldsymbol{b}^{o}\\\
\text{where}\ \sigma(\boldsymbol{x})_{m}&=\begin{cases}0,\
&\boldsymbol{x}_{m}<0\\\ \boldsymbol{x}_{m},\ &\boldsymbol{x}_{m}\geq
0\end{cases}\ .\end{split}$ (1)

For problems with a binary or categorical target variable (i.e. binary or
multi-class classification), a sigmoid or softmax layer is added after
$\boldsymbol{o}$ respectively to convert the convert the NN outputs to proper
probabilistic predictions.

The ReLU activation function $\sigma({\cdot})$ inserts non-linearity into the
model by checking a set of linear inequalities:
$\boldsymbol{w}_{m}^{T}\boldsymbol{x}+b_{m}\geq 0,\ m=1,2,\ldots,M$, where
$\boldsymbol{w}_{m}^{T}$ is the $m$th row of matrix $\boldsymbol{W}$ and
$b_{m}$ is the $m$th element of $\boldsymbol{b}$. Each neuron in the hidden
layer creates a partitioning hyperplane in the input space with the linear
equation $\boldsymbol{w}_{m}^{T}\boldsymbol{x}+b_{m}=0$. The areas on two
sides of the hyperplane are two halfspaces. The entire input space is,
therefore, partitioned by these $M$ hyperplanes. We define a local polytope as
a set containing all points that fall on the same side of each and every
hyperplane. The polytope encoding function (2) uses an element-wise indicator
function $\mathbbm{1}(\cdot)$ to create a unique binary code $\boldsymbol{c}$
for each polytope. Since the $m$th neuron is called “ON” for some
$\boldsymbol{x}$ if $\boldsymbol{w}_{m}^{T}\boldsymbol{x}+b_{m}\geq 0$, the
code $\boldsymbol{c}$ also represents the on-off pattern of the neurons. Using
the results of this encoding function, we can express each polytope as an
intersection of $M$ halfspaces as in (3), where the binary code
$\boldsymbol{c}$ controls the directions of the inequalities.

$\displaystyle C(\boldsymbol{x})=$
$\displaystyle\mathbbm{1}(\boldsymbol{W}\boldsymbol{x}+\boldsymbol{b}\geq 0)\
.$ (2) $\displaystyle\mathcal{R}_{\boldsymbol{c}}=\\{\boldsymbol{x}\ |\
(-1)^{c_{m}}(\boldsymbol{w}_{m}^{T}\boldsymbol{x}$ $\displaystyle+b_{m}\leq
0),\ \forall m=1,\ldots,M\\}\ .$ (3)

Figure 1.(b) shows an example of ReLU NN trained on a two-dimensional
synthetic dataset (plotted in Figure 1.(a)). The bounded input space is
$[-1,1]^{2}$ and the target variable is binary. The network has one hidden
layer of 20 neurons. The partitioning hyperplanes associated with these
neurons are plotted as the blue dashed lines. They form in total 91 local
polytopes within the bounded input space.

For a given $\boldsymbol{x}$, if
$\boldsymbol{w}_{m}^{T}\boldsymbol{x}+b_{m}\geq 0$, the ReLU neuron turns on
and passes through the value. Otherwise, the neuron is off and suppresses the
value to zero. Therefore, if we know the $m$th neuron is off, we can mask the
corresponding $\boldsymbol{w}_{m}$ and $b_{m}$ by zeros and create
$\tilde{\boldsymbol{W}}_{\boldsymbol{c}}$ and
$\tilde{\boldsymbol{b}}_{\boldsymbol{c}}$ that satisfy (5). The non-linear
operation, therefore, can be replaced by the a locally linear operation after
zero-masking. Because each local polytope $\mathcal{R}_{\boldsymbol{c}}$ has a
unique neuron activation pattern encoded by $\boldsymbol{c}$, the zero-masking
process in (4) is also unique for each polytope. Here, $\mathbf{1}$ is a
vector of 1s of length $p$ and $\otimes$ denotes element-wise product.

$\displaystyle\tilde{\boldsymbol{W}}_{\boldsymbol{c}}=\boldsymbol{W}\otimes(\boldsymbol{c}\mathbf{1}^{T})\
,\
\tilde{\boldsymbol{b}}_{\boldsymbol{c}}=\boldsymbol{b}\otimes\boldsymbol{c}\
,$ (4)
$\displaystyle\sigma(\boldsymbol{W}\boldsymbol{x}+\boldsymbol{b})=\tilde{\boldsymbol{W}}_{\boldsymbol{c}}\boldsymbol{x}+\tilde{\boldsymbol{b}}_{\boldsymbol{c}},\quad\forall\boldsymbol{x}\in\mathcal{R}_{\boldsymbol{c}}\
.$ (5)

Within each polytope, as the non-linearity is taken out by the zero-masking
process, the input $\boldsymbol{x}$ and output $\boldsymbol{o}$ have a linear
relationship:

$\begin{split}\boldsymbol{o}=\boldsymbol{W}^{o}(\sigma(\boldsymbol{W}\boldsymbol{x}+\boldsymbol{b}))+\boldsymbol{b}^{o}&=\hat{\boldsymbol{W}}_{\boldsymbol{c}}^{o}\boldsymbol{x}+\hat{\boldsymbol{b}}_{\boldsymbol{c}}^{o}\
,\ \forall\boldsymbol{x}\in\mathcal{R}_{\boldsymbol{c}}\ ,\\\ \text{where}\
\hat{\boldsymbol{W}}_{\boldsymbol{c}}^{o}=\boldsymbol{W}^{o}\tilde{\boldsymbol{W}}_{\boldsymbol{c}}\
&,\
\hat{\boldsymbol{b}}_{\boldsymbol{c}}^{o}=\boldsymbol{W}^{o}\tilde{\boldsymbol{b}}_{\boldsymbol{c}}+\boldsymbol{b}^{o}\end{split}$
(6)

The linear model associated with polytope $\mathcal{R}_{\boldsymbol{c}}$ has
the weight matrix $\hat{\boldsymbol{W}}_{\boldsymbol{c}}^{o}$ and the bias
vector $\hat{\boldsymbol{b}}_{\boldsymbol{c}}^{o}$. The ReLU NN is now
represented by a collection of linear models, each defined on a local polytope
$\mathcal{R}_{\boldsymbol{c}}$.

In Figure 1.(b), we represent the linear model in each local polytopes as a
red solid line indicating
$\left(\hat{\boldsymbol{w}}^{o}_{\boldsymbol{c}}\right)^{T}\boldsymbol{x}+\hat{b}^{o}_{\boldsymbol{c}}=0$.
In this binary response case, the two sides of this line have the opposite
class prediction. We only plot the line if it passes through its corresponding
polytope. For other polytopes, the entire polytopes fall on one side of their
corresponding class-separating lines and the predicted class is the same
within the whole polytope. The red lines all together form the decision
boundary of the ReLU NN and are continuous when passing through one polytope
to another. This is a direct result of ReLU NN being a continuous model.

Figure 1: Examples of trained ReLU NNs and their local polytopes. (a) The
grid-like training data with binary target variable. (b) A trained ReLU NN
with one hidden layer of 20 neurons. The heatmap shows the predicted
probability of a sample belong to class 1. The blue dashed lines are the
partitioning hyperplanes associated with the ReLU neurons, which form 91 local
polytopes in total. The red solid lines represent the linear model within each
polytope where class separation occurs. (c) A trained ReLU NN with two hidden
layers of 10 and 5 neurons respectively. The blue dashed lines are the
partitioning hyperplanes associated with the first 10 ReLU neurons, forming 20
level-1 polytopes. The orange dashes lines are the partitioning hyperplanes
associated with the second 5 ReLU neurons within each level-1 polytope. There
are in total 41 (level-2) local polytopes. The red solid lines represent the
linear model within each level-2 polytope where class separation occurs.

###  II-B The case of multiple layers

We can generalize the results to ReLU NNs with multiple hidden layers. A ReLU
NN with $L$ hidden layers hierarchically partitions the input space and is
locally linear in each and every level-$L$ polytope. Each level-$L$ polytope
$\mathcal{R}^{L}$ has a unique binary code
$\boldsymbol{c}^{1}\boldsymbol{c}^{2}\ldots\boldsymbol{c}^{L}$ representing
the activation pattern of the neurons in all $L$ hidden layers. The
corresponding partitioning hyperplanes of each level,
$\hat{\boldsymbol{W}}^{l}\boldsymbol{x}+\hat{\boldsymbol{b}}^{l}=0$,
$l=1,2,\ldots,L$, can be calculated recursively level by level, using the zero
masking procedure:

$\displaystyle\hat{\boldsymbol{W}}^{1}=\boldsymbol{W}^{1}\ ,\
\hat{\boldsymbol{b}}^{1}=\boldsymbol{b}^{1}$ (7)
$\displaystyle\tilde{\boldsymbol{W}}^{l}=\hat{\boldsymbol{W}}^{l}\otimes(\boldsymbol{c}^{l}\mathbf{1}^{T})\
,\
\tilde{\boldsymbol{b}}^{l}=\hat{\boldsymbol{b}}^{l}\otimes\boldsymbol{c}^{l}$
(8)
$\displaystyle\hat{\boldsymbol{W}}^{l+1}=\boldsymbol{W}^{l+1}\tilde{\boldsymbol{W}}^{l}\
,\
\hat{\boldsymbol{b}}^{l+1}=\boldsymbol{W}^{l+1}\tilde{\boldsymbol{b}}^{l}+\boldsymbol{b}^{l+1}\
.$ (9)

We emphasis that $\tilde{\boldsymbol{W}}^{l}$, $\tilde{\boldsymbol{b}}^{l}$,
$\hat{\boldsymbol{W}}^{l+1}$, and $\hat{\boldsymbol{b}}^{l+1}$ depend on all
polytope code up to level $l$:
$\boldsymbol{c}^{1}\boldsymbol{c}^{2}\ldots\boldsymbol{c}^{l}$. The
subscription $\boldsymbol{c}$ is dropped to simplify the notations.

At each level $l$, the encoding function $C^{l}(\cdot)$ and the polytope
$\mathcal{R}^{l}$ expressed as an intersection of $\sum_{t=1}^{l}M_{t}$
halfspaces can be written recursively as:

$\displaystyle
C^{1}(\boldsymbol{x})=\mathbbm{1}(\boldsymbol{W}^{1}\boldsymbol{x}+\boldsymbol{b}^{1}\geq
0)$ (10) $\displaystyle\begin{split}&\mathcal{R}^{1}=\\{\boldsymbol{x}\ |\
(-1)^{c_{m}}\left((\boldsymbol{w}^{1})_{m}^{T}\boldsymbol{x}+(b^{1})_{m}\leq
0\right),\\\ &\quad\quad\quad\quad\forall m=1,2,\ldots,M_{1}\\}\end{split}$
(11) $\displaystyle
C^{l+1}(\boldsymbol{x})=\mathbbm{1}(\hat{\boldsymbol{W}}^{l+1}\boldsymbol{x}+\hat{\boldsymbol{b}}^{l+1}\geq
0)\ ,\ \forall\boldsymbol{x}\in\mathcal{R}^{l}$ (12)
$\displaystyle\begin{split}&\mathcal{R}^{l+1}=\\{\boldsymbol{x}\ |\
(-1)^{c_{m}}\left((\hat{\boldsymbol{w}}^{l+1})_{m}^{T}\boldsymbol{x}+(\hat{b}^{l+1})_{m}\leq
0\right),\\\ &\quad\quad\quad\quad\forall m=1,2,\ldots,M_{l+1}\\}\ \cap\
\mathcal{R}^{l}\ .\end{split}$ (13)

Finally, the linear model in a level-$L$ polytope is:

$\begin{split}\boldsymbol{o}=\hat{\boldsymbol{W}}^{o}\boldsymbol{x}+\hat{\boldsymbol{b}}^{o}\
&,\ \forall\boldsymbol{x}\in\mathcal{R}^{L}\ ,\\\ \text{where}\
\hat{\boldsymbol{W}}^{o}=\boldsymbol{W}^{o}\tilde{\boldsymbol{W}}^{L}\ &,\
\hat{\boldsymbol{b}}^{o}=\boldsymbol{W}^{o}\tilde{\boldsymbol{b}}^{L}+\boldsymbol{b}^{o}\
.\end{split}$ (14)

Figure 1.(c) shows an example of ReLU NN with two hidden layers of size 10 and
5 respectively. The partitioning hyperplanes associated with the first 10
neuron are plotted as the blue dashed lines. They form 20 level-1 polytopes
within the bounded input space. Within each of the level-1 polytope, the
hyperplanes associated with the second 5 neurons further partition the
polytope. In many cases, some of the 5 hyperplanes are outside the level-1
polytope and, therefore, not creating a new sub-partition. The hyperplanes do
create new partitions are plotted as the orange dashed lines. The orange lines
are only straight within a level-1 polytope but are continuous when passing
through one polytope to another, which is also a result of ReLU NN being a
continuous model. In total, this ReLU NN creates 41 (level-2) local polytopes.
As in Figure 1.(b), the linear model within each level-2 polytope is
represented as a red solid line if class separation occurs within the
polytope.

##  III Polytope Boundaries and Adjacency

Beyond viewing ReLU NNs as a collection of linear models defined on local
polytopes, we explore the topological relationship among these polytopes. A
key concept is the boundaries of each polytope. As shown in (13), each
level-$l$ polytope $\mathcal{R}_{\boldsymbol{c}}$ with corresponding binary
code
$\boldsymbol{c}=\boldsymbol{c}^{1}\boldsymbol{c}^{2}\ldots\boldsymbol{c}^{l}$
is an intersection of $\sum_{t=1}^{l}M_{t}$ halfspaces induced by a set of
inequality constraints. Two situations can rise among these inequalities.
First, an arbitrary $\boldsymbol{c}$ may lead to conflicting inequalities and
makes $\mathcal{R}_{\boldsymbol{c}}$ an empty set. This situation can be
common when the number of neurons is much larger than the dimension of the
input space. Second, there can be redundant inequalities which means removing
them does not affect set $\mathcal{R}_{\boldsymbol{c}}$. We now show that the
non-redundant inequalities are closely related to the boundaries of a
polytope.

###### Definition III.1

Let $\mathcal{R}$ contains all $\boldsymbol{x}\in\mathbb{R}^{P}$ that satisfy
$M$ linear inequalities:
$\mathcal{R}=\\{\boldsymbol{x}|g_{1}(\boldsymbol{x})\leq
0,g_{2}(\boldsymbol{x})\leq 0,\ldots,g_{M}(\boldsymbol{x})\leq 0\\}$. Assume
that $\mathcal{R}\neq\emptyset$. Let $\tilde{\mathcal{R}}$ contains all
$\boldsymbol{x}$’s that satisfy $M-1$ linear inequalities:
$\tilde{\mathcal{R}}=\\{\boldsymbol{x}|g_{1}(\boldsymbol{x})\leq
0,\ldots,g_{m-1}(\boldsymbol{x})\leq 0,g_{m+1}(\boldsymbol{x})\leq
0,\ldots,g_{M}(\boldsymbol{x})\leq 0\\}$. Then the inequality
$g_{m}(\boldsymbol{x})\leq 0$ is a redundant inequality with respect to
(w.r.t.) $\mathcal{R}$ if $\mathcal{R}=\tilde{\mathcal{R}}$.

With the redundant inequality defined above, the following lemma provides an
algorithm to identify them. The proof of this lemma is in the Appendix.

###### Lemma III.1

Given a set $\mathcal{R}=\\{\boldsymbol{x}|g_{1}(\boldsymbol{x})\leq
0,\ldots,g_{M}(\boldsymbol{x})\leq 0\\}\neq\emptyset$, then
$g_{m}(\boldsymbol{x})$ is a redundant inequality if the new set formed by
flipping this inequality is empty:
$\hat{\mathcal{R}}=\\{\boldsymbol{x}|g_{1}(\boldsymbol{x})\leq
0,\ldots,g_{m}(\boldsymbol{x})\geq 0,\ldots,g_{M}(\boldsymbol{x})\leq
0\\}=\emptyset$.

We can now define the boundaries of a polytope formed by a set of linear
inequalities using a similar procedure in LemmaIII.1. The concept of polytope
boundaries also leads to the definition of adjacency. Intuitively, we can move
from one polytope to its adjacent polytope by crossing a boundary.

###### Definition III.2

Given a non-empty set formed by $M$ linear inequalities:
$\mathcal{R}=\\{\boldsymbol{x}|g_{1}(\boldsymbol{x})\leq
0,\ldots,g_{M}(\boldsymbol{x})\leq 0\\}\neq\emptyset$, then the hyperplane
$g_{m}(\boldsymbol{x})=0$ is a boundary of $\mathcal{R}$ if the new set formed
by flipping the corresponding inequality is non-empty:
$\hat{\mathcal{R}}=\\{\boldsymbol{x}|g_{1}(\boldsymbol{x})\leq
0,\ldots,g_{m}(\boldsymbol{x})\geq 0,\ldots,g_{M}(\boldsymbol{x})\leq
0\\}\neq\emptyset$. Polytope $\hat{\mathcal{R}}$ is called one-adjacent to
$\mathcal{R}$.

Since for each polytope the directions of its linear inequalities are
reflected by the binary code, two one-adjacent polytopes must have their code
differ by one bit. Figure 2.(a) demonstrates the adjacency among the local
polytopes. The ReLU NN is the same as in Figure 1.(b). Using the procedure in
Definition III.2, 4 out of the 20 partitioning hyperplanes are identified as
the boundaries of polytope No.0 and marked in red. The 4 one-adjacent
neighbors to polytope No.0 are No.1, 2, 3, and 4; each can be reached by
crossing one boundary.

As we have shown in the Section II-B, ReLU NNs create polytopes level by
level. We follow the same hierarchy to define the polytope adjacency. Assume
two non-empty level-$l$ polytopes, $\mathcal{R}$ and $\hat{\mathcal{R}}$, are
inside the same level-$(l-1)$ polytope, which means their corresponding code
$\boldsymbol{c}=\boldsymbol{c}^{1}\boldsymbol{c}^{2}\ldots\boldsymbol{c}^{l}$
and
$\hat{\boldsymbol{c}}=\boldsymbol{c}^{1}\boldsymbol{c}^{2}\ldots\hat{\boldsymbol{c}}^{l}$
only differs at level-$l$. We say that polytope $\hat{\mathcal{R}}$ is a
level-$l$ one-adjacent neighbor of $\mathcal{R}$ if $\hat{\boldsymbol{c}}^{l}$
and $\boldsymbol{c}^{l}$ only differs in one bit.

The condition that
$\boldsymbol{c}=\boldsymbol{c}^{1}\boldsymbol{c}^{2}\ldots\boldsymbol{c}^{l}$
and
$\hat{\boldsymbol{c}}=\boldsymbol{c}^{1}\boldsymbol{c}^{2}\ldots\hat{\boldsymbol{c}}^{l}$
only differs at level-$l$ is important. In this way, the two linear
inequalities associated with each pair of bits in $\boldsymbol{c}$ and
$\hat{\boldsymbol{c}}$ have the same coefficients, and the difference in
$\boldsymbol{c}^{l}$ and $\hat{\boldsymbol{c}}^{l}$ only changes the direction
of the linear inequality. On the other hand, if the two codes differ at a
level $l^{\prime}<l$, then according to the recursive calculation in (8) and
(9), the codes starting from level $l^{\prime}+1$ will correspond to linear
inequalities of different coefficients, leaving our Definition III.2 of
adjacency not applicable.

Figure 2.(b) demonstrates the hierarchical adjacency among the local
polytopes. The ReLU NN is the same as in Figure 1.(c). Level-1 polytopes
$(1,\cdot)$ and $(2,\cdot)$ are both (level-1) one-adjacent to $(0,\cdot)$.
Within the level-1 polytope $(0,\cdot)$, Level-2 polytopes $(0,0)$ and $(0,1)$
are (level-2) one-adjacent to each other. Similarly, we can identify the
level-2 adjacency of the other two pairs $(1,0)-(1,1)$ and $(2,0)-(2,1)$. Note
that in the plot, even thought one can move from polytope $(2,1)$ to $(0,1)$
by crossing one partitioning hyperplane, we do not define these two polytopes
as adjacent, as they lie into two different level-1 polytopes.

##  IV Polytope Traversing

Figure 2: Demonstration of the BFS-base polytope traversing algorithm. (a)
Traversing the 8 local polytopes within the bounded regions. The ReLU NN is
the same as in Figure 1.(b). The lines marked in red are the boundaries of
polytope No.0. (b) Traversing the 6 local polytopes within the bounded region.
The ReLU NN is the same as in Figure 1.(c). The polytopes are indexed as
“(level-1, level-2)”. (c) The evolution of the BFS queue for traversing the
local polytopes in (a). The gray arrows show the traversing order. The colored
arrows at the bottom indicate the one-adjacent neighbors added to the queue.
(d) The evolution of the hierarchical BFS queue for traversing the local
polytopes in (b). The level-1 BFS queue is shown vertically while the level-2
BFS queue is shown horizontally.

###  IV-A The case of one hidden layer

The adjacency defined in the previous section provides us an order to traverse
the local polytopes: starting from an initial polytope $\mathcal{R}$, visiting
its all one-adjacent neighbors, then visiting all the neighbors’ neighbors and
so on.

This algorithm can be viewed as breath-first search (BFS) on a polytope graph.
To create this graph, we turn each polytope created by the ReLU NN into a
node. An edge is added between each pair of polytopes that are one-adjacent to
each other. The BFS algorithm uses a queue to keep track the traversing
progress. At the beginning of traversing, the initial polytope is added to an
empty queue and is marked as visited afterwards. In each iteration, we pop out
the first polytope from the queue and identify all of its one-adjacent
neighbors. Among these identified polytopes, we add those that have not been
visited to the back of the queue and mark them as visited. The iteration stops
when the queue is empty.

The key component of the polytope traversing algorithm is to identify a
polytope’s one-adjacent neighbors. For a polytope
$\mathcal{R}_{\boldsymbol{c}}$ coded by $\boldsymbol{c}$ of $M$ bits, there
are at most $M$ one-adjacent neighbors with codes corresponding to flipping
one of the bits in $\boldsymbol{c}$. Each valid one-adjacent neighbor must be
non-empty and can be reached by crossing a boundary. Therefore, we can check
each linear inequality in (3) and determine whether it is a boundary or
redundant. Some techniques of identifying redundant inequalities are
summarized in [40]. By flipping the bits corresponding to the identified
boundaries, we obtain the codes of the one-adjacent polytopes.

Equivalently, we can identify the one-adjacent neighbors by going through all
$M$ candidate codes and selecting those corresponding to non-empty sets.
Checking the feasibility of a set constrained by a set of linear inequalities
is often referred to as the “Phase-I Problem” of LP and can be solved
efficiently by modern LP solvers. During BFS iterations, we can hash the
checked codes to avoid checking them repetitively. The BFS-based polytope
traversing algorithm is summarized in Algorithm 1. We now state the
correctness of this algorithm with its proof in Appendix.

###### Theorem IV.1

Given a ReLU NN with one hidden layer of $M$ neurons as specified in (1),
Algorithm 1 covers all non-empty local polytopes created by the neural
network. That is, for all $\boldsymbol{x}\in\mathbb{R}^{P}$, there exists one
$\mathcal{R}_{\boldsymbol{c}}$ as defined in (3) such that
$\boldsymbol{x}\in\mathcal{R}_{\boldsymbol{c}}$ and
$\boldsymbol{c}\in\mathcal{S}_{R}$, where $\mathcal{S}_{R}$ is the result
returned by Algorithm 1.

Algorithm 1 visits all the local polytopes created by a ReLU NN within
$\mathbb{R}^{P}$. The time complexity is exponential to the number of neurons,
as all $2^{M}$ possible activation patterns are checked once in the worst-case
scenario. The space complexity is also exponential to the number of neurons as
we hash all the checked activation patterns. Furthermore, for each activation
pattern, we solve a phase-I problem of LP with $M$ inequalities in
$\mathbb{R}^{P}$. Traversing all local polytopes in $\mathbb{R}^{P}$,
therefore, becomes intractable for neural networks with a large number of
neurons.

Fortunately, traversing in $\mathbb{R}^{P}$ is usually undesirable. Firstly, a
neural network may run into extrapolation issues for points outside the sample
distribution. The polytopes far away from the areas covered by the samples are
often considered unreliable. Secondly, many real-life applications, to be
discussed in Section V, only require traversing within small bounded regions
to examine the local behavior of a model. In the next section, we introduce a
technique to improve the efficiency when traversing within a bounded region.

Algorithm 1 BFS-Based Polytope Traversing

1:A ReLU NN with one hidden layer of $M$ neurons as specified in (1).

2:An initial point $\boldsymbol{x}\in\mathbb{R}^{P}$.

3:Initialize an empty queue $\mathcal{Q}$ for BFS.

4:Initialize an empty set $\mathcal{S}_{R}$ to store the codes of all visited
polytopes.

5:Initialize an empty set $\mathcal{S}_{\boldsymbol{c}}$ to store all checked
codes.

6:Calculate $\boldsymbol{x}$’s initial polytope code $\boldsymbol{c}$ using
(2).

7:Append $\boldsymbol{c}$ to the end of the $\mathcal{Q}$.

8:Add $\boldsymbol{c}$ to both $\mathcal{S}_{R}$ and
$\mathcal{S}_{\boldsymbol{c}}$.

9:while $\mathcal{Q}$ is not empty do

10: Pop out the first element in the front of BFS queue:
$\boldsymbol{c}=\mathcal{Q}.\text{pop}()$.

11: for $m=1,2,\ldots,M$ do

12: Create a candidate polytope code $\hat{\boldsymbol{c}}$ by flipping one
bit in $\boldsymbol{c}$: $\hat{c}_{m}=1-c_{m}$ and $\hat{c}_{k}=c_{k}\forall
k\neq m$.

13: if $\hat{\boldsymbol{c}}\notin\mathcal{S}_{\boldsymbol{c}}$ then

14: Check if
$\mathcal{R}_{\hat{\boldsymbol{c}}}=\\{\boldsymbol{x}|(-1)^{\hat{c}_{k}}\left(\boldsymbol{w}_{k}^{T}\boldsymbol{x}+b_{k}\right)\leq
0,\ k=1,2\ldots,M\\}$ is empty using LP.

15: Add $\hat{\boldsymbol{c}}$ to $\mathcal{S}_{\boldsymbol{c}}$.

16: if $\mathcal{R}_{\hat{\boldsymbol{c}}}\neq\emptyset$ then

17: Append $\hat{\boldsymbol{c}}$ to the end of the $\mathcal{Q}$.

18: Add $\hat{\boldsymbol{c}}$ to $\mathcal{S}_{R}$.

19:Return $\mathcal{S}_{R}$.

###  IV-B Polytope traversing within a bounded region

We first consider a region with each dimension bounded independently:
$l_{j}\leq x_{j}\leq u_{j}$, $j=1,2,\ldots,P$. These $2\times P$ linear
inequalities creates a hypercube denoted as $\mathcal{B}$. During the BFS-
based polytope traversing, we repetitively flip the direction of one of the
$M$ inequalities to identify the one-adjacent neighbors. When the bounded
region is small, it is likely that only a small number of the $M$ hyperplanes
cut through the hypercube. For the other hyperplanes, the entire hypercube
falls onto only one side. Flipping to the other sides of these hyperplanes
would leave the bounded region. Therefore, at the very beginning of polytope
traversing, we can run through the $M$ hyperplanes to identify those cutting
through the hypercube. Then in each neighbor identifying step, we only flip
these hyperplanes.

To identify the hyperplanes cutting through the hypercube, we denote the two
sides of a hyperplane $\mathcal{H}$ and $\bar{\mathcal{H}}$:
$\mathcal{H}=\\{\boldsymbol{x}|\boldsymbol{w}_{m}^{T}\boldsymbol{x}+b_{m}\leq
0\\}$ and
$\bar{\mathcal{H}}=\\{\boldsymbol{x}|\boldsymbol{w}_{m}^{T}\boldsymbol{x}+b_{m}\geq
0\\}$. If neither $\mathcal{H}\cap\mathcal{B}$ nor
$\hat{\mathcal{H}}\cap\mathcal{B}$ is empty, we say the hyperplane
$\boldsymbol{w}_{m}^{T}\boldsymbol{x}+b_{m}=0$ cuts through $\mathcal{B}$.
$\mathcal{H}\cap\mathcal{B}$ and $\hat{\mathcal{H}}\cap\mathcal{B}$ are both
constrained by $2\times P+1$ inequalities, checking their feasibility can
again be formulated as a phase-I problem of LP. We name this technique
hyperplane pre-screening and summarize it in algorithm 2.

Algorithm 2 Hyperplane Pre-Screening

1:A set of hyperplanes $\boldsymbol{w}_{m}^{T}\boldsymbol{x}+b_{m}\leq 0$,
$m=1,2,\ldots,M$.

2:A bounded traversing region $\mathcal{B}$, e.g. $\\{\boldsymbol{x}|l_{j}\leq
x_{j}\leq u_{j}$, $j=1,2,\ldots,P\\}$.

3:Initialize an empty set $\mathcal{T}$ to store all hyperplanes cutting
through $\mathcal{B}$.

4:for $m=1,2,\ldots,M$ do

5: Get two halfspaces
$\mathcal{H}=\\{\boldsymbol{x}|\boldsymbol{w}_{m}^{T}\boldsymbol{x}+b_{m}\leq
0\\}$ and
$\bar{\mathcal{H}}=\\{\boldsymbol{x}|\boldsymbol{w}_{m}^{T}\boldsymbol{x}+b_{m}\geq
0\\}$.

6: if $\mathcal{H}\cap\mathcal{B}\neq\emptyset$ and
$\hat{\mathcal{H}}\cap\mathcal{B}\neq\emptyset$ then

7: Add $m$ to $\mathcal{T}$.

8:Return $\mathcal{T}$.

Hyperplane pre-screening effectively reduces the complexity from
$\mathcal{O}\left(2^{M}\right)$ to
$\mathcal{O}\left(2^{|\mathcal{T}|}\right)$, where $|\mathcal{T}|$ is the
number of hyperplanes cutting through the hypercube. The number
$2^{|\mathcal{T}|}$ corresponds to the worst-case scenario. Since the BFS-
based traversing only checks non-empty polytopes and their potential one-
adjacent neighbors, the number of activation patterns actually checked can be
less than $2^{|\mathcal{T}|}$. In general, the fewer hyperplanes go through
$\mathcal{B}$ the faster polytope traversing finishes.

Figure 2.(a) shows traversing the 8 local polytopes within the bounded region.
The ReLU NN is the same as in Figure 1.(b). The lines marked in red are the
hyperplanes cutting through the bounded region and are identified by the pre-
screening algorithm. The evolution of the BFS queue is shown in Figure 2.(c).
The gray arrows show the traversing order. The colored arrows at the bottom
indicate the one-adjacent neighbors added to the queue. When polytope No.0 is
popped from the queue, its one-adjacent neighbors, No.1, 2, 3, and 4, are
added to the queue. Next, when polytope No.1 is popped, its one-adjacent
neighbors, No.5 and 6, are added. Polytope No.0, although as a one-adjacent
neighbor to No.1, is ignored since it has been visited. Similarly, when
polytope No.2 is popped, only one of its one-adjacent neighbors, No. 7, is
added, since all others have been visited (including those in the queue). The
algorithm finished after popping Polytope No.8 as no new polytopes can be
added and the queue is empty. All 8 local polytopes in the bounded region are
traversed.

Because $\mathcal{B}$ is bounded by a set of linear inequalities, the
correctness of BFS-based polytope traversing as stated in Theorem IV.1 can be
easily extended to this bounded traversing case. Following similar steps of
the proof of Theorem IV.1 in the Appendix, we can show that for any two non-
empty polytopes overlapped with $\mathcal{B}$, we can move from one to another
by repetitively finding a one-adjacent neighbor within $\mathcal{B}$. We
emphasis that the correctness of BFS-based polytope traversing can be proved
for any traversing region bounded by a set of linear inequalities. This
realization is critical to generalize our results to the case of ReLU NNs with
multiple hidden layers. Furthermore, as any closed convex set can be
represented as the intersection of a set of (possibly infinite) halfspaces,
the correctness of BFS-based polytope traversing is true for any closed convex
$\mathcal{B}$.

###  IV-C Hierarchical polytope traversing in the case of multiple hidden
layers

The BFS-based polytope traversing algorithm can be generalized to ReLU NNs
with multiple hidden layers. In section II-B, we described how a ReLU NN with
$L$ hidden layers hierarchically partition the input space into polytopes of
$L$ different level. Then in sectionIII, we showed the adjacency of level-$l$
polytopes is conditioned on all of them belonging to the same level-$(l-1)$
polytope. Therefore, to traverse all level-$L$ polytopes, we need to traverse
all level-$(L-1)$ polytopes and within each of them traversing the sub-
polytopes by following the one-adjacent neighbors.

The procedure above leads us to a recursive traversing scheme. Assume a ReLU
NN with L hidden layers and a closed convex traversing region $\mathcal{B}$.
Starting from a sample $\boldsymbol{x}\in\mathcal{B}$, we traverse all level-1
polytopes using the BFS-based algorithm. Inside each level-1 polytope, we
traverse all the contained level-2 polytopes, so on and so forth until we
reach the level-L polytopes. As shown in (13), each level-$l$ polytope is
constrained by $\sum_{t=1}^{l}M_{t}$ linear inequalities, the way to identify
level-$l$ one-adjacent neighbors is largely the same as what we have described
in Section IV-A. Two level-$l$ one-adjacent neighbors must have the same
$\sum_{t=1}^{l-1}M_{t}$ linear inequalities corresponding to
$\boldsymbol{c}^{1}\boldsymbol{c}^{2}\ldots\boldsymbol{c}^{l-1}$, and have one
of the last $M_{l}$ inequalities differ in direction, so there are $M_{l}$
cases to check.

We can use hyperplane pre-screening at each level of traversing. When
traversing the level-$l$ polytopes within in a level-$(l-1)$ polytope
$\mathcal{R}^{l-1}$, we update the bounded traversing region by taking the
intersection of $\mathcal{R}^{l-1}$ and $\mathcal{B}$. We then screen the
$M_{l}$ partitioning hyperplanes and only select those passing through this
update traversing region.

The BFS-based hierarchical polytope traversing algorithm is summarized in
Algorithm 3. The correctness of this algorithm can be proved based on the
results in Section IV-B, which guarantees the thoroughness of traversing the
level-$l$ polytopes within in any level-$(l-1)$ polytope. Then the overall
thoroughness is guaranteed because each level of traversing is thorough. We
state the result in the following theorem.

###### Theorem IV.2

Given a ReLU NN with $L$ hidden layers and a closed convex traversing region
$\mathcal{B}$. Algorithm 3 covers all non-empty level-$L$ polytopes created by
the neural network that overlap with $\mathcal{B}$. That is, for all
$\boldsymbol{x}\in\mathcal{B}$, there exists one
$\mathcal{R}_{\boldsymbol{c}}$ as defined in (13) such that
$\boldsymbol{x}\in\mathcal{R}_{\boldsymbol{c}}$ and
$\boldsymbol{c}\in\mathcal{S}_{R}$, where $\mathcal{S}_{R}$ is the result
returned by Algorithm 3.

Figure 2.(b) shows traversing the 6 local polytopes within the bounded region.
The ReLU NN is the same as in Figure 1.(c). The evolution of the hierarchical
BFS queue is shown in Figure 2.(d). The level-1 BFS queue is shown vertically
while the level-2 BFS queue is shown horizontally. Starting from level-1
polytope $(0,\cdot)$, the algorithm traverses the two level-2 polytopes inside
it (line 10 in Algorithm 3). It then identifies the two (level-1) one-adjacent
neighbors of $(0,\cdot)$: $(1,\cdot)$ and $(2,\cdot)$. Every time a level-1
polytope is identified, the algorithm goes into it to traverse all the level-2
polytopes inside (line 36). At the end of the recursive call, all 6 local
polytopes in the bounded region are traversed.

Algorithm 3 BFS-Based Hierarchical Polytopes Traversing in a Bounded Region

1:A ReLU NN with $L$ hidden layers.

2:A closed convex traversing region $\mathcal{B}$.

3:An initial point $\boldsymbol{x}\in\mathcal{B}$.

4:Initialize an empty set $\mathcal{S}_{R}$ to store the codes of all visited
polytopes.

5:

6:function HIERARCHICAL_TRAVERSE($\boldsymbol{x},l$)

7: Initialize an empty queue $\mathcal{Q}^{l}$ for BFS at level $l$.

8: Initialize an empty set $\mathcal{S}_{\boldsymbol{c}}^{l}$ to store all
checked level-$l$ codes.

9: Calculate $\boldsymbol{x}$’s initial polytope code $\boldsymbol{c}$
recursively using (12).

10: if $l==L$ then

11: Add $\boldsymbol{c}$ to $\mathcal{S}_{R}$

12: else

13: HIERARCHICAL_TRAVERSE($\boldsymbol{x}$,$l$+1)

14: if $l>1$ then

15: Get the level-$(l-1)$ polytope code specified by the front segment of
$\boldsymbol{c}$:
$\boldsymbol{c}^{1:l-1}=\boldsymbol{c}^{1}\boldsymbol{c}^{2}\ldots\boldsymbol{c}^{l-1}$.

16: Use $\boldsymbol{c}^{1:l-1}$ to get the level-$(l-1)$ polytope
$\mathcal{R}_{\boldsymbol{c}}^{l-1}$ as in (13).

17: else

18: $\mathcal{R}_{\boldsymbol{c}}^{0}=\mathbb{R}^{P}$

19: Form the new traversing region
$\mathcal{B}^{l-1}=\mathcal{B}\cap\mathcal{R}_{\boldsymbol{c}}^{l-1}$.

20: Append the code segment $\boldsymbol{c}^{l}$ to the end of the
$\mathcal{Q}^{l}$.

21: Add the code segment $\boldsymbol{c}^{l}$ to
$\mathcal{S}_{\boldsymbol{c}}$.

22: Get the $M_{l}$ hyperplanes associated with $\boldsymbol{c}^{l}$.

23: Pre-Screen the hyperplanes associated with $\boldsymbol{c}^{l}$ using
Algorithm 2 with bounded region $\mathcal{B}^{l-1}$.

24: Collect the pre-screening results $\mathcal{T}$.

25: while $\mathcal{Q}^{l}$ is not empty do

26: Pop the first element in the front of BFS queue:
$\boldsymbol{c}^{l}=\mathcal{Q}^{l}.\text{pop}()$.

27: for $m\in\mathcal{T}$ do

28: Create a candidate polytope code $\hat{\boldsymbol{c}}^{l}$ by flipping
one bit in $\boldsymbol{c}^{l}$: $\hat{c}_{m}^{l}=1-c_{m}^{l}$ and
$\hat{c}_{k}^{l}=c_{k}^{l}\forall k\neq m$.

29: if $\hat{\boldsymbol{c}}^{l}\notin\mathcal{S}_{\boldsymbol{c}}$ then

30: Get set
$\mathcal{R}_{\hat{\boldsymbol{c}}}=\\{\boldsymbol{x}|(-1)^{\hat{c}_{k}}\left(\langle\hat{\boldsymbol{w}}_{k}^{l},\boldsymbol{x}\rangle+\hat{b}_{k}^{l}\right)\leq
0,\ k=1,2\ldots,M_{l}\\}$

31: Check if $\mathcal{R}_{\hat{\boldsymbol{c}}}\cap\mathcal{B}^{l-1}$ is
empty using LP.

32: Add $\hat{\boldsymbol{c}}^{l}$ to $\mathcal{S}_{\boldsymbol{c}}$.

33: if $\mathcal{R}_{\hat{\boldsymbol{c}}}\cap\mathcal{B}^{l-1}\neq\emptyset$
then

34: Append $\hat{\boldsymbol{c}}^{l}$ to the end of the $\mathcal{Q}^{l}$.

35: if $l==L$ then

36: Add
$\hat{\boldsymbol{c}}=\boldsymbol{c}^{1}\boldsymbol{c}^{2}\ldots\hat{\boldsymbol{c}}^{l}$
to $\mathcal{S}_{R}$

37: else

38: Find a point
$\hat{\boldsymbol{x}}\in\mathcal{R}_{\hat{\boldsymbol{c}}}\cap\mathcal{B}^{l-1}$

39: HIERARCHICAL_TRAVERSE($\hat{\boldsymbol{x}}$,$l$+1)

40:

41:HIERARCHICAL_TRAVERSE($\boldsymbol{x}$,1)

42:Return $\mathcal{S}_{R}$.

##  V Network Property Verification Based on Polytope Traversing

The biggest advantage of the polytope traversing algorithm is its ability to
be adapted to solve many different problems of practical interest. Problems
such as local adversarial attacks, searching for counterfactual samples, and
local monotonicity verification can be solved easily when the model is linear.
As we have shown in Sections II-B, the local model within each level-$L$
polytope created by a ReLU NN is indeed linear. The polytope traversing
algorithm provides a way to analyze not only the behavior of a ReLU NN at one
local polytope but also the behavior within the neighborhood, and therefore
enhances our understanding of the overall model behavior. In this section, we
describe the details of adapting the polytope traversing algorithm to verify
several properties of ReLU NNs.

Figure 3: Demonstration of different applications of the polytope traversing
algorithm. We use the ReLU NN in Figure 1.(b) as an example. (a) Conducting
local adversarial attack by finding the maximum (green) and minimum (red)
model predictions within a bounded region. (b) Creating counterfactual samples
that are closest to the original sample. The distance are measured in $L_{1}$
(green) and $L_{2}$ (red) norms. (c) Monotonicity verification in a bounded
region. The polytope in red violates condition of model prediction
monotonically decreasing along the horizontal axis.

###  V-A Local Adversarial Attacks

We define the local adversarial attack problem as finding the perturbation
within a bounded region such that the model output can be changed most
adversarially. Here, we assume the model output to be a scalar in $\mathbb{R}$
and consider three regression cases with different types of response variable:
continuous, binary, and categorical. The perturbation region is a convex set
around the original sample. For example, we can allow certain features to
increase or decrease by certain amount; or we can use a norm ($L_{1}$,
$L_{2}$, $L_{\infty}$) ball centered at the original sample.

In the continuous response case, the one-dimensional output after the last
linear layer of a ReLU NN is directly used as the prediction of the target
variable. Denote the model function as $f(\cdot)$, the original sample as
$\boldsymbol{x}_{0}$, and the perturbation region as $\mathcal{B}$. The local
adversarial attack problem can be written as:

$\begin{split}\max_{\boldsymbol{x}\in\mathcal{B}}|f(\boldsymbol{x})-f(\boldsymbol{x}_{0})|=\max\Big{(}\max_{\boldsymbol{x}\in\mathcal{B}}f(\boldsymbol{x})-f(\boldsymbol{x}_{0}),\\\
f(\boldsymbol{x}_{0})-\min_{\boldsymbol{x}\in\mathcal{B}}f(\boldsymbol{x})\Big{)}\
,\end{split}$ (15)

which means we need to find the range of the model outputs on $\mathcal{B}$.
We can traverse all local polytopes covered by $\mathcal{B}$, finding the
model output range within each intersection $\mathcal{B}\cap\mathcal{R}$, then
aggregating all the local results to get the final range. Finding the output
range within each $\mathcal{B}\cap\mathcal{R}$ is a convex problem with linear
objective function, so the optimality can be guaranteed within each polytope.
Because our traversing algorithm covers all polytopes overlapped with
$\mathcal{B}$, the final solution also has guaranteed optimality.

In the case of binary response, the one-dimensional output after the last
linear layer of a ReLU NN is passed through a logistic/sigmoid function to
predict the probability of a sample belonging to class 1. To conduct
adversarial attack, we minimize the predicted probability $f(\boldsymbol{x})$
if the true response $y$ is 1, and maximize the prediction if the true
response is 0:

$\begin{cases}\max_{\boldsymbol{x}\in\mathcal{B}}f(\boldsymbol{x}),\quad
y=0\\\ \min_{\boldsymbol{x}\in\mathcal{B}}f(\boldsymbol{x}),\quad y=1\
.\end{cases}$ (16)

Because of the monotonicity of the logistic function, the minimizer and
maximizer of the probabilistic output are the same minimizer and maximizer of
the output after the last linear layer (i.e. the predicted log odds), making
it equivalent to the case of continuous response.

In the case of categorical response with levels 1 to $Q$, the output after the
last linear layer of a ReLU NN is in $\mathbb{R}^{Q}$ and is passed through a
softmax layer to be converted to probabilistic predictions of a sample
belonging to each class. The adversarial sample is generated to minimize the
predicted probability of the sample being in its true class. Within each local
polytope, the linear models are given by (14), and the predicted probability
of class $q$ can be minimized by finding the maximizer of the following
optimization problem:

$\max_{\boldsymbol{x}\in\mathcal{B}\cap\mathcal{R}}\sum_{i=1,i\neq
q}^{Q}e^{(\hat{\boldsymbol{w}}_{i}^{o}-\hat{\boldsymbol{w}}_{q}^{o})^{T}\boldsymbol{x}+(\hat{b}_{i}^{o}-\hat{b}_{q}^{o})}\
,$ (17)

where $\left(\hat{\boldsymbol{w}}_{i}^{o}\right)^{T}$ is the $i$th row of the
matrix $\hat{\boldsymbol{W}}^{o}$ and $\hat{b}_{i}^{o}$ is the $i$th element
in $\hat{\boldsymbol{b}}^{o}$. Since the objective function in (17) is convex,
the optimality of local adversarial attack with polytope traversing is
guaranteed.

Figure 3.(a) demonstrates local adversarial attack in the case of regression
with binary response. The ReLU NN is the same as in Figure 1.(b), which
predicts the probability of a sample belong to class 1. The predictions across
the whole domain are shown as the heat map. Within the region bounded by the
black box, we find the minimum and maximum predictions and marked them by red
and green respectively. Due to the nature of linear models, the minimizer and
maximizer always fall on the intersections of partitioning hyperplanes and/or
region boundaries.

###  V-B Counterfactual sample generation

In classification problems, we are often interested in finding the smallest
perturbation on a sample such that the model changes its class prediction. The
magnitude of the perturbation is often measured by $L_{1}$, $L_{2}$, or
$L_{\infty}$ norm. The optimization problem can be written as:

$\min_{\boldsymbol{x}}||\boldsymbol{x}-\boldsymbol{x}_{0}||_{p}\quad\text{s.t.}f_{\mathcal{C}}(\boldsymbol{x})\neq
f_{\mathcal{C}}(\boldsymbol{x}_{0})\ ,$ (18)

where $\boldsymbol{x}_{0}$ is the original sample, $p$ indicates a specific
type of norm, and $f_{\mathcal{C}}(\cdot)$ is a ReLU NN outputting class
predictions.

We can adapt the polytope traversing algorithm to solve this problem. In the
case of binary response, each local polytope has an associated hyperplane
separating the two classes:
$(\hat{\boldsymbol{w}}^{o})^{T}\boldsymbol{x}+\hat{b}^{o}=\gamma$, where
$\hat{\boldsymbol{w}}^{o}$ and $\hat{b}^{o}$ are given in (14), and $\gamma$
is the threshold converting predicted log odds to class. Finding the
counterfactual sample within a local polytope $\mathcal{R}$ can be written as
a convex optimization problem:

$\min_{\boldsymbol{x}}||\boldsymbol{x}-\boldsymbol{x}_{0}||_{p}\quad\text{s.t.}(-1)^{\hat{y}_{0}}\left((\hat{\boldsymbol{w}}^{o})^{T}\boldsymbol{x}+\hat{b}^{o}\right)>\gamma,\
\boldsymbol{x}\in\mathcal{R}\ .$ (19)

where $\hat{y}_{0}$ is the original class (0 or 1) predicted by the model.

We start the traversing algorithm from the polytope where $\boldsymbol{x}_{0}$
lies. In each polytope, we solve (19). It is possible that the entire polytope
fall on one side of the class separating hyperplane and (19) does not have any
feasible solution. If a solution can be obtained, we compare it with the
solutions in previously traversed polytopes and keep the one with the smallest
perturbation. Furthermore, we use this perturbation magnitude to construct a
new bounded traversing region around $\boldsymbol{x}_{0}$. Because no points
outside this region can have a smaller distance to the original points, once
we finish traversing all the polytopes inside this region, the algorithm can
conclude. In practice we often construct this dynamic traversing region as
$\mathcal{B}=\\{\boldsymbol{x}\ |\
||\boldsymbol{x}-\boldsymbol{x}_{0}||_{\infty}<d^{*}\\}$, where $d^{*}$ is the
smallest perturbation magnitude so far. When solving for (19) in the
proceeding polytopes, we add $x\in\mathcal{B}$ to the constraints.
$\mathcal{B}$ is updated whenever a smaller $d^{*}$ is found. Because the new
traversing region is always a subset of the previous one, our BFS-based
traversing algorithm covers all polytopes within the final traversing region
under this dynamic setting. The final solution to (18) is guaranteed to be
optimal, and the running time depends on how far the original point is away
from a class boundary.

In the case of categorical response with levels 1 to $Q$, the output after the
last linear layer of a ReLU NN has $Q$ dimensions and the dimension of the
largest value is the predicted class. We ignore the softmax layer at the end
because it does not change the rank of the dimensions. Assuming the original
example is predicted to belong to class $\hat{q}_{0}$, we generate
counterfactual samples in the rest of $Q-1$ classes.

We consider one of these classes at a time and denote it as $q$. Within each
ReLU NN’s local polytope, the linear models are given by (14). The area where
a sample is predicted to be in class $q$ is enclosed by the intersection of
$Q-1$ halfspaces:

$\mathcal{C}_{q}=\\{\boldsymbol{x}|\left(\hat{\boldsymbol{w}}_{q}^{o}-\hat{\boldsymbol{w}}_{i}^{o}\right)^{T}\boldsymbol{x}+(\hat{b}_{q}^{o}-\hat{b}_{i}^{o})>0,\forall
i=1,\ldots,Q,i\neq q\\}.$ (20)

Therefore, within each local polytope, we solve the convex optimization
problem:

$\min_{\boldsymbol{x}}||\boldsymbol{x}-\boldsymbol{x}_{0}||_{p}\quad\text{s.t.}\
\boldsymbol{x}\in\mathcal{C}_{q}\cap\mathcal{R}\ .$ (21)

We compare all feasible solutions of (21) under different $q$ and keep the one
counterfactual sample that is closest to $\boldsymbol{x}_{0}$. The traversing
procedure and the dynamic traversing region update is the same as in the
binary response case. Since (21) is convex, the final solution to (18) is
guaranteed to be optimal.

Figure 3.(b) demonstrates counterfactual sample generation in the case of
binary classification. The ReLU NN is the same as in Figure 1.(b) whose class
decision boundaries are plotted in red. Given an original sample plotted as
the black dot, we generate two counterfactual samples on the decision
boundaries. The red dot has the smallest $L_{2}$ distance to the original
point while the green dot has the smallest $L_{1}$ distance.

Figure 4: Network verification results of all 45 ACAS Xu networks for property
II (a), III (b), and IV (c). The blue lines and markers show the number of
local polytopes traversed during verification. The red lines and markers show
the time (in seconds) used. A dot marker indicates the corresponding network
satisfies the property while a cross marker indicates the property is violated
in at least one of the local polytopes.

###  V-C Local monotonicity verification

We can adapt the polytope traversing algorithm to verify if a trained ReLU NN
is monotonic w.r.t. certain features. We consider the regression cases with
continuous and binary response. In both cases, the output after the last
linear layer is a scalar. Since the binary response case uses a logistic
function at the end which is monotonically increasing itself, we can ignore
this additional function. The verification methods for the two cases,
therefore, are equivalent.

To check whether the model is monotonic w.r.t. a specific feature within a
bounded convex domain, we traverse the local polytopes covered by the domain.
Since the model is linear within each polytope, we can easily check the
monotonicity direction (increasing or decreasing) by checking the sign of the
corresponding coefficients. After traversing all local polytopes covered by
the domain, we check their agreement on the monotonicity direction. Since a
ReLU NN produces a continuous function, if the local models are all
monotonically increasing or all monotonically decreasing, the network is
monotonic on the checked domain. If there is a disagreement in the direction,
the network is not monotonic. The verification algorithm based on polytope
traversing not only provides us the final monotonicity result but also tells
us in which part of the domain monotonicity is violated.

Figure 3.(c) demonstrates local adversarial attack in the case of regression
with binary response. The ReLU NN is the same as in Figure 1.(b), which
predicts the probability of a sample belong to class 1. The predictions across
the whole domain are shown as the heat map. We check if the model is
monotonically increasing w.r.t. $x_{1}$ along the horizontal axis. The domain
to check is bounded by the black box. Among the 5 polytopes overlapped with
the domain, one of them violates the monotonically increasing condition and is
marked in red.

###  V-D Comparison with algorithms based on mixed-integer programming

The three applications above have been traditionally solved using MIP [24, 25,
15, 26, 27]. Our algorithms based on polytope traversing have several
advantages. First, our method exploits the topological structure created by
ReLU NNs and fully explains the model behavior in small neighborhoods. For the
$2^{M}$ cases created by a ReLU NN with $M$ neurons, MIP eliminates the
searching branches using branch-and-bound. Our method, on the other hand,
eliminates the searching branches by checking the feasibility of the local
polytopes and their adjacency. Since a small traversing region often covers a
limited number of polytopes, our algorithm has short running time when solving
local problems.

Second, since our algorithm explicitly identifies and visits all the
polytopes, the final results contain not only the optimal solution but also
the whole picture of the model behavior, providing explainability to the
often-so-called black-box model.

Third, our method requires only linear and convex programming solvers and no
MIP solvers. Identifying adjacent polytopes requires only linear programming.
Convex programming may be used to solve the sub-problem within a local
polytope. Our algorithm allows us to incorporate any convex programming solver
that is most suitable for the sub-problem, providing much freedom to
customize.

Last but probably the most important, our algorithm is highly versatile and
flexible. Within each local polytope, the model is linear, which is often the
simplest type of model to work with. Any analysis that one runs on a linear
model can be transplanted here and wrapped inside the polytope traversing
algorithm. Therefore, our algorithm provides a unified framework to verify
different properties of piecewise linear networks.

##  VI Case Studies

Figure 5: Adversarial testing of a MNIST digit classification network w.r.t.
50 testing samples (5 samples per digit). The maximum change of an individual
pixel value is (a) $+/-0.01$ or (b) $+/-0.05$. The blue lines and markers show
the number of local polytopes traversed during verification. The red lines and
markers show the time (in seconds) used. A dot marker indicates the network is
robust w.r.t. the corresponding sample, while a cross marker indicates at
least one adversarial sample can be found. Two adversarial samples are shown
in (c).

###  VI-A ACAS Xu

We applied the polytope traversing algorithm to verify the safety of ACAS Xu
networks [41]. The ACAS Xu networks contain an array of 45 ReLU NNs to issue
advisories to avoid mid-air collisions for unmanned aircraft. This array of
networks was developed to approximate a large lookup table traditionally used
in an Airborne Collision Avoidance System so that the massive memory
occupation by the table and the lookup time can be reduced. Each network takes
five inputs: distance from ownship to intruder, angle from ownship to
intruder, heading angle of the intruder w.r.t. ownship, speed of ownship, and
speed of intruder. The five possible advisories output from each network are:
Clear-of-Conflict (COC), week right, strong right, week left, and strong left.
Each network contains six hidden layers with 50 neurons in each layer,
resulting in a total of 300 neurons.

The appendix of [21] listed 10 desired properties that each network should
satisfy. In our case study, we selected property II, III, and VI. Given a
bounded set in the input space, these properties impose constraints on the
rank of the networks’ multi-class outputs. The verification of these
properties can be formulated as a set of LP within each local polytope. We
coded the polytope traversing algorithm in Python and used the LP solver in
the SciPy package. Figure 4 shows the verification results. The blue lines and
markers show the number of local polytopes traversed during the verification.
The red lines and markers show the total verification time in seconds. A dot
marker indicates the corresponding network satisfies the property while a
cross marker indicates the property is violated in at least one of the local
polytopes. For property III and IV, the violating networks are identified
after traversing only one of their local polytopes. For property II, most of
the violating networks can be identified after traversing 10,000 local
polytopes.

###  VI-B MNIST

We also applied the polytope traversing algorithm to verify the robustness of
a MNIST digits classifier. The neural network
111https://github.com/vtjeng/MIPVerify_data/blob/master/weights/mnist/n1.mat
we tested takes a vectorized image as input which contains 784 pixels. It has
two hidden layers of sizes 40 and 20 respectively. The output has a dimension
of 10, corresponding to each possible digit. This network is trained using
traditional techniques without special enforcement on robustness.

The robustness property requires the network’s prediction to remain the same
when a small perturbation is applied to the pixels of the original sample. In
our test, we scaled all the pixel values to the range of 0 to 1. We tested two
budget levels: 0.01 and 0.05, which means the maximum change each pixel can
take is plus or minus the budget level while remaining inside the 0-1 range.
We selected 50 samples from the testing dateset, five for each digit. We ran
the polytope traversing algorithm until an adversarial sample was found or the
network was verified w.r.t. the testing sample.

Figure 5 shows the robustness test results. As in previous experiments, we use
blue and red lines to show the number of traversed local polytoeps and
computational time (in seconds) respectively. A dot marker indicates the
network is robust w.r.t. the corresponding sample, while a cross marker
indicates at least one adversarial sample is found. Even under the small
budget of 0.01, the network is not robust w.r.t. 11 out of the 50 testing
samples. The number of local polytopes covered within the budget varies
significantly with different original samples. When the budget is increased to
0.05, many adversarial samples can be found in the same polytope that the
original samples fall into. While in some other cases more than 10,000 local
polytopes are traversed before finding the first adversarial sample. Two
adversarial samples are shown in Figure 5.(c). The small perturbations hardly
perceivable to us fool the neural network.

##  VII Conclusion

We explored the unique topological structure that ReLU NNs create in the input
space; identified the adjacency among the partitioned local polytopes;
developed a traversing algorithm based on this adjacency; and proved the
thoroughness of polytope traversing. Our polytope traversing algorithm could
be extended to other piecewise linear networks such as those containing
convolutional or maxpooling layers.

##  VIII Acknowledgments

The authors would like to thank Lin Dong, Linwei Hu, Rahul Singh, and Han Wang
from Wells Fargo, and Sihan Zeng from Georgia Institute of Technology for
their valuable inputs and feedback on this project.

## References

  * [1] Xavier Glorot, Antoine Bordes, and Yoshua Bengio,  “Deep sparse rectifier neural networks,”  in Proceedings of the fourteenth international conference on artificial intelligence and statistics. JMLR Workshop and Conference Proceedings, 2011, pp. 315–323.
  * [2] Raman Arora, Amitabh Basu, Poorya Mianjy, and Anirbit Mukherjee,  “Understanding deep neural networks with rectified linear units,”  in International Conference on Learning Representations, 2018.
  * [3] Zhou Lu, Hongming Pu, Feicheng Wang, Zhiqiang Hu, and Liwei Wang,  “The expressive power of neural networks: A view from the width,”  in Proceedings of the 31st International Conference on Neural Information Processing Systems, 2017, pp. 6232–6240.
  * [4] Guido F Montufar, Razvan Pascanu, Kyunghyun Cho, and Yoshua Bengio,  “On the number of linear regions of deep neural networks,”  Advances in Neural Information Processing Systems, vol. 27, pp. 2924–2932, 2014.
  * [5] Johannes Schmidt-Hieber,  “Nonparametric regression using deep neural networks with relu activation function,”  The Annals of Statistics, vol. 48, no. 4, pp. 1875–1897, 2020.
  * [6] Difan Zou, Yuan Cao, Dongruo Zhou, and Quanquan Gu,  “Gradient descent optimizes over-parameterized deep relu networks,”  Machine Learning, vol. 109, no. 3, pp. 467–492, 2020.
  * [7] Rudy Bunel, Ilker Turkaslan, Philip HS Torr, Pushmeet Kohli, and M Pawan Kumar,  “A unified view of piecewise linear neural network verification,”  in Proceedings of the 32nd International Conference on Neural Information Processing Systems, 2018, pp. 4795–4804.
  * [8] Anish Athalye, Logan Engstrom, Andrew Ilyas, and Kevin Kwok,  “Synthesizing robust adversarial examples,”  in International conference on machine learning. PMLR, 2018, pp. 284–293.
  * [9] Nicholas Carlini and David Wagner,  “Towards evaluating the robustness of neural networks,”  in 2017 ieee symposium on security and privacy (sp). IEEE, 2017, pp. 39–57.
  * [10] Ian J Goodfellow, Jonathon Shlens, and Christian Szegedy,  “Explaining and harnessing adversarial examples,”  arXiv preprint arXiv:1412.6572, 2014.
  * [11] Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow, and Rob Fergus,  “Intriguing properties of neural networks,”  in 2nd International Conference on Learning Representations, ICLR 2014, 2014.
  * [12] Changliu Liu, Tomer Arnon, Christopher Lazarus, Christopher Strong, Clark Barrett, and Mykel J Kochenderfer,  “Algorithms for verifying deep neural networks,”  arXiv preprint arXiv:1903.06758, 2019.
  * [13] Hennie Daniels and Marina Velikova,  “Monotone and partially monotone neural networks,”  IEEE Transactions on Neural Networks, vol. 21, no. 6, pp. 906–917, 2010.
  * [14] Akhil Gupta, Naman Shukla, Lavanya Marla, Arinbjörn Kolbeinsson, and Kartik Yellepeddi,  “How to incorporate monotonicity in deep networks while preserving flexibility?,”  arXiv preprint arXiv:1909.10662, 2019.
  * [15] Xingchao Liu, Xing Han, Na Zhang, and Qiang Liu,  “Certified monotonic neural networks,”  arXiv preprint arXiv:2011.10219, 2020.
  * [16] Arnab Sharma and Heike Wehrheim,  “Testing monotonicity of machine learning models,”  arXiv preprint arXiv:2002.12278, 2020.
  * [17] Divya Gopinath, Hayes Converse, Corina Pasareanu, and Ankur Taly,  “Property inference for deep neural networks,”  in 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE). IEEE, 2019, pp. 797–809.
  * [18] Lingyang Chu, Xia Hu, Juhua Hu, Lanjun Wang, and Jian Pei,  “Exact and consistent interpretation for piecewise linear neural networks: A closed form solution,”  in Proceedings of the 24th ACM SIGKDD International Conference on Knowledge Discovery & Data Mining, 2018, pp. 1244–1253.
  * [19] Osbert Bastani, Yani Ioannou, Leonidas Lampropoulos, Dimitrios Vytiniotis, Aditya Nori, and Antonio Criminisi,  “Measuring neural net robustness with constraints,”  Advances in neural information processing systems, vol. 29, pp. 2613–2621, 2016.
  * [20] Ruediger Ehlers,  “Formal verification of piece-wise linear feed-forward neural networks,”  in International Symposium on Automated Technology for Verification and Analysis. Springer, 2017, pp. 269–286.
  * [21] Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer,  “Reluplex: An efficient smt solver for verifying deep neural networks,”  in International Conference on Computer Aided Verification. Springer, 2017, pp. 97–117.
  * [22] Luca Pulina and Armando Tacchella,  “An abstraction-refinement approach to verification of artificial neural networks,”  in International Conference on Computer Aided Verification. Springer, 2010, pp. 243–257.
  * [23] Luca Pulina and Armando Tacchella,  “Challenging smt solvers to verify neural networks,”  Ai Communications, vol. 25, no. 2, pp. 117–135, 2012.
  * [24] Ross Anderson, Joey Huchette, Will Ma, Christian Tjandraatmadja, and Juan Pablo Vielma,  “Strong mixed-integer programming formulations for trained neural networks,”  Mathematical Programming, pp. 1–37, 2020.
  * [25] Matteo Fischetti and Jason Jo,  “Deep neural networks as 0-1 mixed integer linear programs: A feasibility study,”  arXiv preprint arXiv:1712.06174, 2017.
  * [26] Vincent Tjeng, Kai Y Xiao, and Russ Tedrake,  “Evaluating robustness of neural networks with mixed integer programming,”  in International Conference on Learning Representations, 2018.
  * [27] Lily Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Luca Daniel, Duane Boning, and Inderjit Dhillon,  “Towards fast computation of certified robustness for relu networks,”  in International Conference on Machine Learning. PMLR, 2018, pp. 5276–5285.
  * [28] Thiago Serra, Christian Tjandraatmadja, and Srikumar Ramalingam,  “Bounding and counting linear regions of deep neural networks,”  in International Conference on Machine Learning. PMLR, 2018, pp. 4558–4566.
  * [29] Francesco Croce, Maksym Andriushchenko, and Matthias Hein,  “Provable robustness of relu networks via maximization of linear regions,”  in the 22nd International Conference on Artificial Intelligence and Statistics. PMLR, 2019, pp. 2057–2066.
  * [30] Haakon Robinson, Adil Rasheed, and Omer San,  “Dissecting deep neural networks,”  arXiv preprint arXiv:1910.03879, 2019.
  * [31] Agus Sudjianto, William Knauth, Rahul Singh, Zebin Yang, and Aijun Zhang,  “Unwrapping the black box of deep relu networks: Interpretability, diagnostics, and simplification,”  arXiv preprint arXiv:2011.04041, 2020.
  * [32] Xiaodong Yang, Hoang-Dung Tran, Weiming Xiang, and Taylor Johnson,  “Reachability analysis for feed-forward neural networks using face lattices,”  arXiv preprint arXiv:2003.01226, 2020.
  * [33] Boris Hanin and David Rolnick,  “Deep relu networks have surprisingly few activation patterns,”  Advances in Neural Information Processing Systems, vol. 32, pp. 361–370, 2019.
  * [34] Zebin Yang, Aijun Zhang, and Agus Sudjianto,  “Enhancing explainability of neural networks through architecture constraints,”  IEEE Transactions on Neural Networks and Learning Systems, 2020\.
  * [35] Wei Zhao, Rahul Singh, Tarun Joshi, Agus Sudjianto, and Vijayan N Nair,  “Self-interpretable convolutional neural networks for text classification,”  arXiv preprint arXiv:2105.08589, 2021.
  * [36] Weiming Xiang, Hoang-Dung Tran, and Taylor T Johnson,  “Reachable set computation and safety verification for neural networks with relu activations,”  arXiv preprint arXiv:1712.08163, 2017.
  * [37] Francesco Croce and Matthias Hein,  “A randomized gradient-free attack on relu networks,”  in German Conference on Pattern Recognition. Springer, 2018, pp. 215–227.
  * [38] Francesco Croce, Jonas Rauber, and Matthias Hein,  “Scaling up the randomized gradient-free adversarial attack reveals overestimation of robustness using established attacks,”  International Journal of Computer Vision, vol. 128, no. 4, pp. 1028–1046, 2020.
  * [39] Joseph A Vincent and Mac Schwager,  “Reachable polyhedral marching (rpm): A safety verification algorithm for robotic systems with deep neural network components,”  in 2021 IEEE International Conference on Robotics and Automation (ICRA). IEEE, 2021, pp. 9029–9035.
  * [40] Jan Telgen,  “Identifying redundant constraints and implicit equalities in systems of linear constraints,”  Management Science, vol. 29, no. 10, pp. 1209–1222, 1983.
  * [41] Kyle D Julian, Jessica Lopez, Jeffrey S Brush, Michael P Owen, and Mykel J Kochenderfer,  “Policy compression for aircraft collision avoidance systems,”  in 2016 IEEE/AIAA 35th Digital Avionics Systems Conference (DASC). IEEE, 2016, pp. 1–10.
  * [42] Jan Telgen,  “Minimal representation of convex polyhedral sets,”  Journal of Optimization Theory and Applications, vol. 38, no. 1, pp. 1–24, 1982.

## Appendix

###  VIII-A Proof of Lemma III.1

###### Lemma VIII.1

Given a set $\mathcal{R}=\\{\boldsymbol{x}|g_{1}(\boldsymbol{x})\leq
0,\ldots,g_{M}(\boldsymbol{x})\leq 0\\}\neq\emptyset$, then
$g_{m}(\boldsymbol{x})$ is a redundant inequality if the new set formed by
flipping this inequality is empty:
$\hat{\mathcal{R}}=\\{\boldsymbol{x}|g_{1}(\boldsymbol{x})\leq
0,\ldots,g_{m}(\boldsymbol{x})\geq 0,\ldots,g_{M}(\boldsymbol{x})\leq
0\\}=\emptyset$.

###### Proof:

Let $\tilde{\mathcal{R}}$ be the set formed by removing inequality
$g_{m}(\boldsymbol{x})\leq 0$:
$\tilde{\mathcal{R}}=\\{\boldsymbol{x}|g_{1}(\boldsymbol{x})\leq
0,\ldots,g_{m-1}(\boldsymbol{x})\leq 0,g_{m+1}(\boldsymbol{x})\leq
0,\ldots,g_{M}(\boldsymbol{x})\leq 0\\}$. Then
$\tilde{\mathcal{R}}=\mathcal{R}\cup\hat{\mathcal{R}}$. If
$\hat{\mathcal{R}}=\emptyset$, then $\mathcal{R}=\tilde{\mathcal{R}}$ and the
inequality $g_{m}(\boldsymbol{x})\leq 0$ satisfies Definition III.1. ∎

Note the other direction of Lemma III.1 may not hold. One example is when
identical inequalities appear in the set: both inequalities in
$\mathcal{R}=\\{\boldsymbol{x}|g_{1}(\boldsymbol{x})\leq
0,g_{2}(\boldsymbol{x})\leq 0\\}$ are redundant by definition if
$g_{1}(\cdot)=g_{2}(\cdot)$. However, the procedure in LemmaIII.1 will not
identify them as redundant.

###  VIII-B Proof of Theorem IV.1

###### Theorem VIII.2

Given a ReLU NN with one hidden layer of $M$ neurons as specified in (1),
Algorithm 1 covers all non-empty local polytopes created by the neural
network. That is, for all $\boldsymbol{x}\in\mathbb{R}^{P}$, there exists one
$\mathcal{R}_{\boldsymbol{c}}$ as defined in (3) such that
$\boldsymbol{x}\in\mathcal{R}_{\boldsymbol{c}}$ and
$\boldsymbol{c}\in\mathcal{S}_{R}$, where $\mathcal{S}_{R}$ is the result
returned by Algorithm 1.

###### Proof:

Since each partitioning hyperplane divide $\mathbb{R}^{P}$ into two
halfspaces, all $2^{M}$ activation patterns encoded by $\boldsymbol{c}$ covers
the entire input space. We construct a graph with $2^{M}$ nodes, each
representing a possible polytope code. Some the nodes may correspond to an
empty set due to conflicting inequalities. For each pair of non-empty polytope
that are one-adjacent to each other, we add an edge to their corresponding
nodes. What left to prove is that any pair of non-empty polytopes are
connected.

W.l.o.g. assume two nodes with code $\boldsymbol{c}$ and
$\hat{\boldsymbol{c}}$ that differ only in the first $K$ bits. Also assume the
polytopes $\mathcal{R}_{\boldsymbol{c}}$ and
$\mathcal{R}_{\hat{\boldsymbol{c}}}$ are both non-empty. We will show that
there must exist a non-empty polytope $\mathcal{R}_{\tilde{\boldsymbol{c}}}$
that is one-adjacent to $\mathcal{R}_{\boldsymbol{c}}$ with code
$\tilde{\boldsymbol{c}}$ different from $\hat{\boldsymbol{c}}$ in one of the
first $K$ bits. As a result, $\tilde{\boldsymbol{c}}$ is now one bit closer to
$\hat{\boldsymbol{c}}$.

We prove the claim above by contradiction. Assuming claim is not true, we flip
any one of the first $K$ bits in $\mathcal{R}_{\boldsymbol{c}}$, and the
corresponding polytope $\mathcal{R}_{\tilde{\boldsymbol{c}}^{k}}$ must be
empty. By Definition III.1, the inequality
$(-1)^{c_{m}}\left(\boldsymbol{w}_{m}^{T}\boldsymbol{x}+b_{m}\right)\leq 0$,
$m=1,2,\ldots,K$ must all be redundant, which means they can be removed from
the set of constraints [42, 40]:

$\begin{split}\mathcal{R}_{\boldsymbol{c}}=&\\{\boldsymbol{x}|(-1)^{c_{m}}\left(\boldsymbol{w}_{m}^{T}\boldsymbol{x}+b_{m}\right)\leq
0,\ m=1,2\ldots,M\\}\\\
=&\\{\boldsymbol{x}|(-1)^{c_{m}}\left(\boldsymbol{w}_{m}^{T}\boldsymbol{x}+b_{m}\right)\leq
0,\ m=K+1,\ldots,M\\}\\\
\supseteq&\\{\boldsymbol{x}|(-1)^{c_{m}}\left(\boldsymbol{w}_{m}^{T}\boldsymbol{x}+b_{m}\right)\leq
0,\ m=1,2,\ldots,M\\}\cup\\\
&\\{\boldsymbol{x}|(-1)^{c_{m}}\left(\boldsymbol{w}_{m}^{T}\boldsymbol{x}+b_{m}\right)\geq
0,\ m=1,\ldots,K,\\\ &\quad\ \
(-1)^{c_{m}}\left(\boldsymbol{w}_{m}^{T}\boldsymbol{x}+b_{m}\right)\leq 0,\
m=K+1,\ldots,M\\}\\\
=&\mathcal{R}_{\boldsymbol{c}}\cup\mathcal{R}_{\hat{\boldsymbol{c}}}\
.\end{split}$ (22)

The derived relationship in (22) plus the assumption that all
$\mathcal{R}_{\tilde{\boldsymbol{c}}^{k}}$ must be empty lead to the
conclusion that $\mathcal{R}_{\hat{\boldsymbol{c}}}=\emptyset$, which
contradict with the non-empty assumption.

Therefore, for any two non-empty polytopes $\mathcal{R}_{\boldsymbol{c}}$ and
$\mathcal{R}_{\hat{\boldsymbol{c}}}$, we can create a path from
$\mathcal{R}_{\boldsymbol{c}}$ to $\mathcal{R}_{\hat{\boldsymbol{c}}}$ by
iteratively finding an intermediate polytope whose code is one bit closer to
$\hat{\boldsymbol{c}}$. Since the polytope graph covers all input space and
all non-empty polytopes are connected, BFS guarantees the thoroughness of
traversing. ∎