11institutetext: Kansas State University, Manhattan, KS, 66506
11email<EMAIL_ADDRESS>
# Bisimulations for Neural Network Reduction

Pavithra Prabhakar

###### Abstract

We present a notion of bisimulation that induces a reduced network which is
semantically equivalent to the given neural network. We provide a minimization
algorithm to construct the smallest bisimulation equivalent network.
Reductions that construct bisimulation equivalent neural networks are limited
in the scale of reduction. We present an approximate notion of bisimulation
that provides semantic closeness, rather than, semantic equivalence, and
quantify semantic deviation between the neural networks that are approximately
bisimilar. The latter provides a trade-off between the amount of reduction and
deviations in the semantics.

###### Keywords:

Neural Networks Bisimulation Verification Reduction.

##  1 Introduction

Neural networks (NN) with small size are conducive for both automated analysis
and explainability. Rigorous automated analysis using formal methods has
gained momentum in recent years owing to the safety-criticality of the
application domains in which NN are deployed [3, 16, 12, 20, 19, 11]. For
instance, NN are an integral part of control, perception and guidance of
autonomous vehicles. However, the scalability of these analysis techniques,
for instance, for computing output range for safety analysis [6, 12], is
limited by the large size of the neural networks encountered and the
computational complexity due to the presence of non-linear activation
functions. In this paper, we borrow ideas from formal methods to design novel
network reduction techniques with formal relations between the given and the
reduced networks, that can be applied to reduce the verification time. It can
also potentially impact explainability by presenting to the user a smaller
network with guaranteed bounds on the deviation from the original network.

Bisimulation [14] is a classical notion of equivalence between systems in
process algebra that guarantees that processes that are bisimilar satisfy the
same set of properties specified in certain branching time logics [2]. A
bisimulation is an equivalence relation on the states of a system that
requires similar behaviors with respect to one step of computation, which then
inductively guarantees global behavioral equivalence. Bisimulation algorithm
[2] allows one to construct the smallest systems, bisimulation quotients, that
are bisimilar to a given (finite state) system.

Our first result consists of a definition of bisimulation for neural networks,
namely, NN-bisimulation, that defines a notion of equivalence between neural
networks. The challenge arises from the fact that neural networks semantically
have multiple parallel threads of computation that are both branching and
merging at each step of computation. We observe that the global equivalence
can be established by imposing a _one-step backward pre-sum equivalence_ ,
wherein we require two nodes that belong to the same class to agree on the
biases, the activation functions, and the pre-sums, wherein a pre-sum
corresponds to the sum of the weights on the incoming edges from a given
equivalence class. Our notion resembles that of probabilistic bisimulation
[13], however, our notion is based on pre-sum equivalences rather than post-
sum equivalences. We define a quotienting operation on an NN with respect to a
bisimulation that yields a smaller network which is input-output equivalent to
the given network. We also show that there exists a coarsest bisimulation
which yields the smallest neural network with respect to the quotienting
operation. We provide a minimization algorithm that outputs this smallest
neural network.

The notion of bisimulation can be stringent, since, it preserves the exact
input-output relation. It has been observed, for instance, in the context of
control systems, that a strict notion of equivalence, such as, bisimulation,
does not allow for drastic reduction in state-space, thereby, motivating the
notion of approximate bisimulation. Approximate bisimulations [9, 8] have a
notion of distance between states, and allow a bounded $\epsilon$ deviation
between the executions of the systems in each step. The notion of approximate
bisimulation was successfully used to construct smaller systems in the setting
of dynamical systems and control synthesis [10].

We extend the notion of NN-bisimulation to an approximate notion, wherein we
require nodes belonging to the same class to have bounded deviation,
$\epsilon$, in the biases and the pre-sums. The quotienting operation no more
results in a unique reduced network, but a set of reduced networks. Moreover,
these reduced networks may not have the same input-output relation as the
given neural network. However, we provide a bound on the deviation in the
semantics of two approximately bisimilar NNs. It gives rise to a nice trade-
off between the amount of reduction and the deviation in the semantics, that
translates to a trade-off in the precision and verification time in an
approximation based verification scheme.

### Related work.

Neural network reduction techniques have been explored in different contexts.
There is extensive literature on compression techniques, see, for instance,
surveys on network compression [5, 4]. However, these techniques typically do
not provide formal guarantees on the relation between the given and reduced
systems. Abstraction techniques [15, 17, 7] computing over-approximations of
the input-output relations have been explored in several works, however, they
use slightly different kinds of networks such as interval neural networks and
abstract neural networks, or are limited to certain kinds of activation
functions such as ReLU. Notions of bisimulation for DNNs have not been
explored much in the literature. Equivalence between DNNs is explored [1],
however, the work is restricted to ReLU functions and does not consider
approximate notions.

##  2 Preliminaries

Let $[k]$ denote the set $\\{0,1,\cdots,k\\}$ and $(k]$ the set
$\\{1,2,\cdots,k\\}$. Let $\mathbb{R}$ denote the set of real numbers. We use
$|x|$ to denote the absolute value of $x\in\mathbb{R}$. Given a set $A$, we
use $|A|$ to denote the number of elements of $A$. Given a function
$f:A\to\mathbb{R}$, we define the infinity norm of $f$ to be the supremum of
the absolute values of elements in the range of $f$, that is,
$|\\!|f|\\!|_{\infty}=\sup_{a\in A}|f(a)|$. Given functions $f:A\to B$ and
$g:B\to C$, the composition of $f$ and $g$, $g\circ f:A\to C$, is given by,
for all $a\in A$, $g\circ f(a)=g(f(a))$.

### Partitions.

Given a set $\mathcal{S}$, a (finite) parition of $\mathcal{S}$ is a set
$\mathcal{P}=\\{\mathcal{S}_{1},\cdots,\mathcal{S}_{n}\\}$, such that
$\bigcup_{i}\mathcal{S}_{i}=\mathcal{P}$ and
$\mathcal{S}_{i}\cap\mathcal{S}_{j}=\emptyset$ for all $i\not=j$. We refer to
each element of a partition as a region or a group. A partition $\mathcal{P}$
of $\mathcal{S}$ can be seen as an equivalence relation on $\mathcal{S}$,
given by the relation $s_{1}\mathcal{P}s_{2}$ whenever $s_{1}$ and $s_{2}$
belong to the same group of the partition. Given two partitions $\mathcal{P}$
and $\mathcal{P}^{\prime}$ , we say that $\mathcal{P}$ is finer than
$\mathcal{P}^{\prime}$ (or equivalently, $\mathcal{P}^{\prime}$ is coarser
than $\mathcal{P}$), denoted $\mathcal{P}\preceq\mathcal{P}^{\prime}$, if for
every $S\in\mathcal{P}$, there exists $S^{\prime}\in\mathcal{P}^{\prime}$ such
that $S\subseteq\mathcal{S}^{\prime}$.

##  3 Neural Networks

In this section, we present the preliminaries regarding the neural network.
Recall that a neural network (NN) consists of a layered set of nodes or
neurons, including an input layer, an output layer and one or more hidden
layers. Each node except those in the input layer are annotated with a bias
and an activation function, and there are weighted edges between nodes of
adjacent layers. We capture these elements of a neural network using a tuple
in the following definition.

###### Definition 1

A neural network (NN) is a tuple
$\mathcal{N}=\big{(}k,\mathcal{A}ct,\\{\mathcal{S}_{i}\\}_{i\in[k]},\\{W_{i}\\}_{i\in(k]},$
$\\{b_{i}\\}_{i\in(k]},\\{A_{i}\\}_{i\in(k]}\big{)}$, where:

  * •

$k$ represents the number of layers (except the input layer);

  * •

$\mathcal{A}ct$ is a set of activation functions;

  * •

for each $i\in[k]$, $\mathcal{S}_{i}$ is a set of nodes of layer $i$, we
assume $\mathcal{S}_{i}\cap\mathcal{S}_{j}=\emptyset$ for $i\neq j$;

  * •

for each $i\in(k]$,
$W_{i}:\mathcal{S}_{i-1}\times\mathcal{S}_{i}\to\mathbb{R}$ is the weight
function that captures the weight on the edges between nodes at layer $i-1$
and $i$;

  * •

for each $i\in(k]$, $b_{i}:\mathcal{S}_{i}\to\mathbb{R}$ is the bias function
that associates a bias with nodes of layer $i$;

  * •

for each $i\in(k]$, $A_{i}:\mathcal{S}_{i}\to\mathcal{A}ct$ is an activation
association function that associates an activation function with each node of
layer $i$.

$\mathcal{S}_{0}$ and $\mathcal{S}_{k}$ are the set of nodes corresponding to
the input and output layers, respectively. We will fix the NN
$\mathcal{N}=\big{(}k,\mathcal{A}ct,\\{\mathcal{S}_{i}\\}_{i\in[k]},\\{W_{i}\\}_{i\in(k]},\\{b_{i}\\}_{i\in(k]},\\{A_{i}\\}_{i\in(k]}\big{)}$
for the rest of the paper.

Figure 1: Neural Network $\mathcal{N}$

###### Example 1

The neural network $\mathcal{N}$ shown in Figure 1 consists of an input layer
with $2$ nodes, $2$ hidden layers with $3$ nodes each, and an output layer.
The weights on the edges are shown, for instance,
$W_{2}(\textit{s}_{1,2},\textit{s}_{2,2})=2$. The biases are all $0$s and the
activation functions are all ReLUs (not shown).

In the sequel, the central notion to the definition of bisimulation will be
the total weight on the incoming edges for a node $\textit{s}^{\prime}$ of the
$i$-th layer from a set of nodes $\mathcal{S}$ of the $i-1$-st layer. We will
capture this using the notion of a pre-sum, denoted
$\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S},\textit{s}^{\prime})$. For
instance,
$\textit{PreSum}_{2}^{\mathcal{N}}(\\{\textit{s}_{1,1},\textit{s}_{1,2}\\},\textit{s}_{2,2})=2+2=4$.

###### Definition 2

Given a set $\mathcal{S}\subseteq\mathcal{S}_{i-1}$ and
$\textit{s}^{\prime}\in\mathcal{S}_{i}$, we define
$\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S},\textit{s}^{\prime})=\sum_{\textit{s}\in\mathcal{S}}W_{i}(\textit{s},\textit{s}^{\prime})$.

Next, we capture the operational behavior of a neural network. A valuation v
for the $i$-th layer of $\mathcal{N}$ refers to an assignment of real-values
to all the nodes in $\mathcal{S}_{i}$, that is,
$\textit{v}:\mathcal{S}_{i}\to\mathbb{R}$. Let $\textit{Val}(\mathcal{S}_{i})$
denote the set of all valuations for the $i$-th layer of $\mathcal{N}$. By the
operational semantics of $\mathcal{N}$, we mean the assignments for all the
layers of $\mathcal{N}$, that are obtained from an assignment for the input
layer. We define $[\\![\mathcal{N}]\\!]_{i}(v)$, which given a valuation $v$
for layer $i-1$, returns the corresponding valuation for layer $i$ according
to the semantics of $\mathcal{N}$. The valuation for the output layer of
$\mathcal{N}$ is then obtained by the composition of the functions
$[\\![\mathcal{N}]\\!]_{i}$.

###### Definition 3

The semantics of the $i$-the layer is the function
$[\\![\mathcal{N}]\\!]_{i}:\textit{Val}(\mathcal{S}_{i-1})\to\textit{Val}(\mathcal{S}_{i})$,
where for any $\textit{v}\in\textit{Val}(\mathcal{S}_{i-1})$,
$[\\![\mathcal{N}]\\!]_{i}(\textit{v})=\textit{v}^{\prime}$, given by

$\forall\textit{s}^{\prime}\in\mathcal{S}_{i},\textit{v}^{\prime}(\textit{s}^{\prime})=A_{i}(\textit{s}^{\prime})\big{(}\sum_{\textit{s}\in\mathcal{S}_{i-1}}W_{i}(\textit{s},\textit{s}^{\prime})\textit{v}(\textit{s})+b_{i}(\textit{s}^{\prime})\big{)}.$

To capture the input-output semantics, we compose these one layer semantics.
More precisely, we define $[\\![\mathcal{N}]\\!]^{i}$ to be the composition of
the first $i$ layers, that is, $[\\![\mathcal{N}]\\!]^{i}(\textit{v})$
provides the valuation of the $i$-th layer given v as input. It is defined
inductively as:

$[\\![\mathcal{N}]\\!]^{1}=[\\![\mathcal{N}]\\!]_{1}$ $\forall
i\in(k]\backslash\\{1\\},[\\![\mathcal{N}]\\!]^{i}=[\\![\mathcal{N}]\\!]_{i}\circ[\\![\mathcal{N}]\\!]^{i-1}$

###### Definition 4

The input-output semantic function, represented by
$[\\![\mathcal{N}]\\!]:\textit{Val}(\mathcal{S}_{0})\to\textit{Val}(\mathcal{S}_{k})$,
is defined as:

$[\\![\mathcal{N}]\\!]=[\\![\mathcal{N}]\\!]^{k}$

The notion of bisimulation requires the notion of a partition of the nodes of
$\mathcal{N}$. We define a partition on $\mathcal{N}$ as an indexed set of
partitions each corresponding to a layer.

###### Definition 5

A partition of an $\text{NN}\ \mathcal{N}$ is an indexed set
$\mathcal{P}=\\{\mathcal{P}_{i}\\}_{i\in[k]}$, where for every $i$,
$\mathcal{P}_{i}$ is a partition of $\mathcal{S}_{i}$.

### A note on Lipschitz Continuity.

A function $f:\mathbb{R}^{m}\to\mathbb{R}^{n}$ is said to be Lipschitz
continuous if there exists a constant $L(f)$, referred to as Lipschitz
constant for $f$, such that for all $x,y\in\mathbb{R}^{m}$,

$|\\!|f(x)-f(y)|\\!|_{\infty}\leq L(f)|\\!|x-y|\\!|_{\infty}.$

Several activation functions including ReLU, Leaky ReLU, SoftPlus, Tanh,
Sigmoid, ArcTan and Softsign are known to be $1$-Lipschitz continuous [18],
that is, satisfy the above constraint with $L(f)=1$. In fact, the function
$[\\![\mathcal{N}]\\!]$ is itself Lipschitz continuous, when the activation
functions are Lipschitz continuous [18]. We will use $L(\mathcal{N})$ to
denote an upper bound on $L([\\![\mathcal{N}]\\!]^{i})$ over all $i$. Hence,
given an input v, we know that
$|\\!|[\\![\mathcal{N}]\\!]^{i}(\textit{v})|\\!|_{\infty}\leq
L(\mathcal{N})|\\!|\textit{v}|\\!|_{\infty}$.

##  4 NN-bisimulation and Semantic Equivalence

In this section, we define a notion of bisimulation on neural networks, which
induces a reduced system that is equivalent to the given network. A partition
of $\mathcal{N}$ is an NN-bisimulation if the biases and activation functions
associated with the nodes in any region are the same, and the pre-sums of
nodes in any region with respect to any region of the previous layer are the
same.

###### Definition 6

An NN-bisimulation for $\mathcal{N}$ is a partition
$\mathcal{P}=\\{\mathcal{P}_{i}\\}_{i\in[k]}$ such that for all $i\in(k]$,
$\mathcal{S}\in\mathcal{P}_{i-1}$ and
$\textit{s}^{\prime}_{1},\textit{s}^{\prime}_{2}\in\mathcal{S}_{i}$ with
$\textit{s}^{\prime}_{1}\mathcal{P}_{i}\textit{s}^{\prime}_{2}$, the following
hold:

  1. 1.

$A_{i}(\textit{s}^{\prime}_{1})=A_{i}(\textit{s}^{\prime}_{2})$,

  2. 2.

$b_{i}(\textit{s}^{\prime}_{1})=b_{i}(\textit{s}^{\prime}_{2})$, and

  3. 3.

$\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S},\textit{s}^{\prime}_{1})=\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S},\textit{s}^{\prime}_{2})$.

Our notion is inspired by the well-known notion of probabilistic bisimulation
[13], where post-sums are used instead of pre-sums to characterize which nodes
have the same branching structure. Though neural networks consist of branching
in both forward and backward directions, surprisingly, just pre-sum
equivalence suffices to guarantee input-output relation equivalence.

Bisimulation naturally induces a reduced system, which corresponds to merging
the nodes in a group of the partition, and choosing a representative node from
the group to assign the activation functions, biases and pre-sums. We
represent the reduced system obtained by taking the quotient of $\mathcal{N}$
with respect to a bisimulation $\mathcal{P}$ as $\mathcal{N}/\mathcal{P}$.

###### Definition 7

Given an NN-bisimulation $\mathcal{P}$ for $\mathcal{N}$, the reduced system
$\mathcal{N}/\mathcal{P}=\big{(}k,\mathcal{A}ct,\\{{\widehat{\mathcal{S}}}_{i}\\}_{i\in[k]},\\{\widehat{W}_{i}\\}_{i\in(k]},\\{\widehat{b}_{i}\\}_{i\in(k]},\\{\widehat{A}_{i}\\}_{i\in(k]}\big{)}$,
where:

  1. 1.

$\forall i\in[k],\widehat{\mathcal{S}}_{i}=\mathcal{P}_{i}$;

  2. 2.

$\forall
i\in(k],\widehat{\textit{s}}\in\widehat{\mathcal{S}}_{i-1},\widehat{\textit{s}}^{\prime}\in\widehat{\mathcal{S}}_{i},\widehat{W}_{i}(\widehat{\textit{s}},\widehat{\textit{s}}^{\prime})=\textit{PreSum}_{i}^{\mathcal{N}}(\widehat{\textit{s}},\textit{s}^{\prime})$
for some $\textit{s}^{\prime}\in\widehat{\textit{s}}^{\prime}$.

  3. 3.

$\forall
i\in(k],\widehat{\textit{s}}^{\prime}\in\widehat{\mathcal{S}}_{i},\widehat{b}_{i}(\widehat{\textit{s}}^{\prime})=b_{i}(\textit{s}^{\prime})$
for some $\textit{s}^{\prime}\in\widehat{\textit{s}}^{\prime}$.

  4. 4.

$\forall
i\in(k],\widehat{\textit{s}}^{\prime}\in\widehat{\mathcal{S}}_{i},\widehat{A}_{i}(\widehat{\textit{s}}^{\prime})=A_{i}(\textit{s}^{\prime})$
for some $\textit{s}^{\prime}\in\widehat{s}^{\prime}$.

Note that though the definition depends on the choice of
$\textit{s}^{\prime}$, the reduced system is unique, since, from the
definition of NN-bisimulation, the values of biases, activation functions and
pre-sums, corresponding to different choices of $\textit{s}^{\prime}$ within a
group are the same. We also use just bisimulation to refer to NN-bisimulation.

In order to formally establish the connection between the NN $\mathcal{N}$ and
its reduction $\mathcal{N}/\mathcal{P}$, we define a mapping from the
valuations of $\mathcal{N}$ to those of $\mathcal{N}/\mathcal{P}$, but only
for certain valuations that are consistent in that they map all the related
nodes in $\mathcal{P}$ to the same value.

###### Definition 8

A valuation $\textit{v}\in\textit{Val}(\mathcal{S}_{i})$ is
$\mathcal{P}$-consistent, if for all
$\textit{s}_{1},\textit{s}_{2}\in\mathcal{S}_{i}$, if
$\textit{s}_{1}\mathcal{P}_{i}\textit{s}_{2}$, then
$\textit{v}(\textit{s}_{1})=\textit{v}(\textit{s}_{2})$.

Our first result is that a consistent input valuation leads to a consistent
output valuation, when $\mathcal{P}$ is a bisimulation. We show this for a
particular layer; the extension to the whole network follows from a simple
inductive reasoning.

###### Lemma 1

Let $\mathcal{P}$ be a bisimulation on $\mathcal{N}$. If
$\textit{v}_{1}\in\textit{Val}(\mathcal{S}_{i-1})$ is
$\mathcal{P}$-consistent, then
$\textit{v}_{2}=[\\![\mathcal{N}]\\!]_{i}(\textit{v}_{1})$ is
$\mathcal{P}$-consistent.

###### Proof

Let $\textit{s}^{\prime},\textit{s}^{\prime\prime}\in\mathcal{S}_{i}$ such
that $\textit{s}^{\prime}\mathcal{P}_{i}\textit{s}^{\prime\prime}$. We need to
show that
$\textit{v}_{2}(\textit{s}^{\prime})=\textit{v}_{2}(\textit{s}^{\prime\prime})$.
$\textit{v}_{2}(\textit{s}^{\prime})=A_{i}(\textit{s}^{\prime})(\sum_{\textit{s}\in\mathcal{S}_{i-1}}W_{i}(\textit{s},\textit{s}^{\prime})\textit{v}_{1}(\textit{s})+b_{i}(\textit{s}^{\prime}))=A_{i}(\textit{s}^{\prime})(\sum_{\mathcal{S}\in\mathcal{P}_{i-1}}\sum_{\textit{s}\in\mathcal{S}}W_{i}(\textit{s},\textit{s}^{\prime})$
$\textit{v}_{1}(\textit{s})+b_{i}(\textit{s}^{\prime}))$. Since,
$\textit{v}_{1}$ is $\mathcal{P}$-consistent, for each $\mathcal{S}$, we have
a value $\textit{v}_{1}^{\mathcal{S}}$ that all elements of $\mathcal{S}$ are
mapped to by $\textit{v}_{1}$, that is,
$\textit{v}_{1}^{\mathcal{S}}=\textit{v}_{1}(\textit{s})$ for all
$\textit{s}\in\mathcal{S}$. Replacing $\textit{v}_{1}(\textit{s})$ for each s,
by $\textit{v}_{1}^{\mathcal{S}}$, we obtain
$\textit{v}_{2}(\textit{s}^{\prime})=A_{i}(\textit{s}^{\prime})(\sum_{\mathcal{S}\in\mathcal{P}_{i-1}}\sum_{\textit{s}\in\mathcal{S}}W_{i}(\textit{s},\textit{s}^{\prime})\textit{v}_{1}^{\mathcal{S}}+b_{i}(\textit{s}^{\prime}))$.
From the definition of pre-sum, we can replace
$\sum_{\textit{s}\in\mathcal{S}}W_{i}(\textit{s},\textit{s}^{\prime})$ by
$\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S},\textit{s}^{\prime})$, which is
also equal to
$\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S},\textit{s}^{\prime\prime})$
from the definition of bisimulation, since $\mathcal{P}$ is a bisimulation and
$\textit{s}^{\prime}\mathcal{P}_{i}\textit{s}^{\prime\prime}$. Also,
$A_{i}(\textit{s}^{\prime})=A_{i}(\textit{s}^{\prime\prime})$ and
$b_{i}(\textit{s}^{\prime})=b_{i}(\textit{s}^{\prime\prime})$. So, we obtain,
$\textit{v}_{2}(\textit{s}^{\prime})=A_{i}(\textit{s}^{\prime\prime})(\sum_{\mathcal{S}\in
P_{i-1}}\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S},\textit{s}^{\prime\prime})\textit{v}_{1}^{\mathcal{S}}+b_{i}(\textit{s}^{\prime\prime}))$.
Expanding back
$\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S},\textit{s}^{\prime\prime})$,
and $\textit{v}_{1}^{\mathcal{S}}=\textit{v}_{1}(\textit{s})$ for all
$\textit{s}\in\mathcal{S}$, we obtain
$\textit{v}_{2}(\textit{s}^{\prime})=A_{i}(\textit{s}^{\prime\prime})(\sum_{\mathcal{S}\in
P_{i-1}}\sum_{\textit{s}\in\mathcal{S}}W_{i}(\textit{s},\textit{s}^{\prime\prime})\textit{v}_{1}(\textit{s})+b_{i}(\textit{s}^{\prime\prime}))=\textit{v}_{2}(\textit{s}^{\prime\prime})$.

Note that if we do not group together the nodes in the input and output
layers, there is a bijection between $\mathcal{S}_{0}$ and
$\widehat{\mathcal{S}}_{0}$ and $\mathcal{S}_{k}$ and
$\widehat{\mathcal{S}}_{k}$, and hence, a bijection between their valuations.
We will show that both $\mathcal{N}$ and $\mathcal{N}/\mathcal{P}$ have the
“same” input-output relation modulo the bijection between their nodes. First,
we define a formal relation between $\mathcal{P}$-consistent valuations of
$\mathcal{N}$ and valuations of $\mathcal{N}/\mathcal{P}$.

###### Definition 9

Let $\mathcal{P}$ be a bisimulation on $\mathcal{N}$, and
$\textit{v}\in\textit{Val}(\mathcal{S}_{i})$ be a $\mathcal{P}$-consistent
valuation. The abstraction of v, denoted,
$\alpha(\textit{v})_{\mathcal{N},\mathcal{P}}\in\textit{Val}(\widehat{\mathcal{S}}_{i})$,
is defined as, for every $\hat{\textit{s}}\in\widehat{\mathcal{S}}_{i}$,
$\alpha(\textit{v})_{\mathcal{N},\mathcal{P}}(\hat{\textit{s}})=\textit{v}(\textit{s})$
for some $\textit{s}\in\hat{\textit{s}}$.

Note that $\alpha(\textit{v})_{\mathcal{N},\mathcal{P}}$ is well defined,
since, from the $\mathcal{P}$-consistency of v, $\textit{v}(\textit{s})$ is
the same for any choice of $\textit{s}\in\hat{\textit{s}}$. When $\mathcal{N}$
and $\mathcal{P}$ are clear from the context, we will drop the subscript and
write $\alpha(\textit{v})_{\mathcal{N},\mathcal{P}}$ as just
$\alpha(\textit{v})$. The next result states that the output of the $i$-th
layer of $\mathcal{N}/\mathcal{P}$ with the abstraction of a
$\mathcal{P}$-consistent valuation v of the $i-1$-st layer of $\mathcal{N}$ as
input, results in a valuation that is the abstraction of the output of the
$i$-th layer of $\mathcal{N}$ on input v. In other words, it says that
propagating a valuation for one-step in $\mathcal{N}$ is the same as
propagating its abstraction in $\mathcal{N}/\mathcal{P}$.

###### Lemma 2

Let $\mathcal{P}$ be a bisimulation on $\mathcal{N}$, and
$\textit{v}\in\textit{Val}(\mathcal{S}_{i})$ be $\mathcal{P}$-consistent.
Then,
$\alpha([\\![\mathcal{N}]\\!]_{i}(\textit{v}))=[\\![\mathcal{N}/\mathcal{P}]\\!]_{i}(\alpha(\textit{v}))$.

###### Proof

From Lemma 1, we know that
$\textit{v}^{\prime}=[\\![\mathcal{N}]\\!]_{i}(\textit{v})$ is
$\mathcal{P}$-consistent. Hence, for any
$\hat{\textit{s}}^{\prime}\in\widehat{\mathcal{S}}_{i}$,
$\alpha(\textit{v}^{\prime})(\hat{\textit{s}}^{\prime})=\textit{v}^{\prime}(\textit{s}^{\prime})$
for some (any) $\textit{s}^{\prime}\in\hat{\textit{s}}^{\prime}$. Let us fix
$\textit{s}^{\prime}\in\hat{\textit{s}}^{\prime}$.

$\alpha(\textit{v}^{\prime})(\hat{\textit{s}}^{\prime})=\textit{v}^{\prime}(\textit{s}^{\prime})=A_{i}(\textit{s}^{\prime})\big{(}\sum_{\textit{s}\in\mathcal{S}_{i-1}}W_{i}(\textit{s},\textit{s}^{\prime})\textit{v}(\textit{s})+b_{i}(s^{\prime})\big{)}$

from the semantics of $\mathcal{N}$. Further,

$\sum_{\textit{s}\in\mathcal{S}_{i-1}}W_{i}(\textit{s},\textit{s}^{\prime})\textit{v}(\textit{s})=\sum_{\mathcal{S}\in\mathcal{P}_{i-1}}\sum_{\textit{s}\in\mathcal{S}}W_{i}(\textit{s},\textit{s}^{\prime})\textit{v}(\textit{s})$

From $\mathcal{P}$-consistency of v,
$\textit{v}(\textit{s})=\alpha(\textit{v})(\mathcal{S})$ for any
$\textit{s}\in\mathcal{S}$. Hence,

$\sum_{\textit{s}\in\mathcal{S}}W_{i}(\textit{s},\textit{s}^{\prime})\textit{v}(\textit{s})=\sum_{\textit{s}\in\mathcal{S}}W_{i}(\textit{s},\textit{s}^{\prime})\alpha(\textit{v})(\mathcal{S})=\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S},\textit{s}^{\prime})\alpha(\textit{v})(\mathcal{S}).$

From the definition of $\mathcal{N}/\mathcal{P}$,
$\widehat{A}_{i}(\hat{\textit{s}}^{\prime})=A_{i}(\textit{s}^{\prime}),\widehat{W}_{i}(\mathcal{S},\hat{\textit{s}}^{\prime})=\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S},\textit{s}^{\prime}),\widehat{b}_{i}(\hat{\textit{s}}^{\prime})=b_{i}(\textit{s}^{\prime}),$
and $\mathcal{P}_{i-1}=\widehat{\mathcal{S}}_{i-1}$. From
$\mathcal{P}$-consistency of v,
$\alpha(\textit{v})(\mathcal{S})=\textit{v}(\textit{s})$ for any
$\textit{s}\in\mathcal{S}$. Therefore, for any
$\hat{\textit{s}}^{\prime}\in\widehat{\mathcal{S}}_{i}$,

$\alpha([\\![\mathcal{N}]\\!]_{i}(\textit{v}))(\hat{\textit{s}}^{\prime})=\alpha(\textit{v}^{\prime})(\hat{\textit{s}}^{\prime})$
$=\widehat{A}_{i}(\hat{\textit{s}}^{\prime})\big{(}\sum_{\mathcal{S}\in\widehat{\mathcal{S}}_{i-1}}\widehat{W}_{i}(\mathcal{S},\hat{\textit{s}}^{\prime})\alpha(\textit{v})(\mathcal{S})+\widehat{b}_{i}(\hat{\textit{s}}^{\prime})\big{)}=[\\![\mathcal{N}/\mathcal{P}]\\!]_{i}(\alpha(\textit{v}))(\hat{\textit{s}}^{\prime}).$

The following theorem follows by composing the results from Lemma 2 for the
different layers.

###### Theorem 4.1

Given $\mathcal{P}$ a bisimulation on $\mathcal{N}$, and
$\textit{v}\in\textit{Val}(\mathcal{S}_{0})$ that is $\mathcal{P}$-consistent,
we have
$\alpha([\\![\mathcal{N}]\\!](\textit{v}))=[\\![\mathcal{N}/\mathcal{P}]\\!](\alpha(\textit{v}))$.

###### Proof

We can show by induction on $i$ that
$\alpha([\\![\mathcal{N}]\\!]^{i}(\textit{v}))=[\\![\mathcal{N}/\mathcal{P}]\\!]^{i}(\alpha(\textit{v}))$.

Figure 2: Reduced System $\mathcal{N}/\mathcal{P}$

###### Example 2

Consider a partition $\mathcal{P}$ for the NN $\mathcal{N}$ in Figure 1 where
each node appears as a region by itself except for the regions
$\mathcal{S}_{1}=\\{\textit{s}_{1,1},\textit{s}_{1,2}\\}$, and
$\mathcal{S}_{2}=\\{\textit{s}_{2,1},\textit{s}_{2,2}\\}$. We can verify that
this is a bisimulation. For instance,
$\textit{PreSum}_{2}^{\mathcal{N}}(\mathcal{S}_{1},\textit{s}_{2,1})=1+3$ and
$\textit{PreSum}_{2}^{\mathcal{N}}(\mathcal{S}_{1},\textit{s}_{2,2})=2+2$,
which are the same. The reduced system is given by the NN
$\mathcal{N}/\mathcal{P}$ in Figure 2. Here,
$\widehat{W}_{2}(\mathcal{S}_{1},\mathcal{S}_{2})=4$.

##  5 $\delta$-NN-bisimulation and Semantic Closeness

NN-bisimulation provides a foundation for reducing a neural network while
preserving the input-output relation. However, existence of such bisimulations
leading to equivalent reduced networks with much fewer neurons is limited in
that for many networks no bisimulation quotient may lump together lot of
nodes. Hence, we relax the notion of bisimulation to an approximate notion
wherein we allow potentially large reductions, however, the reduced systems
may not be semantically equivalent, but only be semantically close to the
given neural network. We quantify the deviation of the reduced system in terms
of the “deviation” of the approximate notion from the exact bisimulation.

The approximation notion of bisimulation we consider is inspired by the notion
of approximate bisimulation in the context of dynamical systems [9, 8]. We
essentially relax the requirement of the NN-bisimulation that the biases and
pre-sums match by allowing them to be within a $\delta$. This is formalized in
the following definition.

###### Definition 10

A $\delta$-NN-bisimulation for an NN $\mathcal{N}$ and $\delta\geq 0$ is a
partition $\mathcal{P}=\\{\mathcal{P}_{i}\\}_{i\in[k]}$ such that for all
$i\in(k]$, $\mathcal{S}\in\mathcal{P}_{i-1}$ and
$\textit{s}^{\prime}_{1},\textit{s}^{\prime}_{2}\in\mathcal{S}_{i}$ with
$\textit{s}^{\prime}_{1}\mathcal{P}_{i}\textit{s}^{\prime}_{2}$, the following
hold:

  1. 1.

$A_{i}(\textit{s}^{\prime}_{1})=A_{i}(\textit{s}^{\prime}_{2})$,

  2. 2.

$|b_{i}(\textit{s}^{\prime}_{1})-b_{i}(\textit{s}^{\prime}_{2})|\leq\delta$,
and

  3. 3.

$|\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S},\textit{s}^{\prime}_{1})-\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S},\textit{s}^{\prime}_{2})|\leq\delta$.

We will also use $\delta$-bisimulation to refer to $\delta$-NN-bisimulation.
The reduced system can be constructed similar to that for NN-bisimulation.
However, the choice of the nodes
$\textit{s}^{\prime}\in\hat{\textit{s}}^{\prime}$ used to construct the
weights and biases of the reduced system could lead to different neural
networks. Hence, we obtain a finite set of possibilities for the reduced
system that we denote by $\mathcal{N}/_{\delta}\mathcal{P}$.

Figure 3: Illustration of $\mathcal{N}^{*}/_{\delta}\mathcal{P}$ on NN
$\mathcal{N}^{*}$

###### Example 3

Consider the NN $\mathcal{N}^{*}$ in Figure 3 (top left) and a partition
$\mathcal{P}=\\{\mathcal{P}_{i}\\}_{i}$, where
$\mathcal{P}_{0}=\\{\\{\textit{s}_{0,1}\\}\\}$,
$\mathcal{P}_{2}=\\{\\{\textit{s}_{2,1}\\}\\}$ and
$\mathcal{P}_{1}=\\{\\{\textit{s}_{1,1},\textit{s}_{1,2}\\},\\{\textit{s}_{1,3}\\}\\}$,
that is, $\mathcal{P}$ merges nodes $\textit{s}_{1,1}$ and $\textit{s}_{1,2}$.
Note that $\mathcal{P}$ is a $\delta$-bisimulation on $\mathcal{N}^{*}$ for
$\delta=0.2$. For instance,
$\textit{PreSum}_{1}^{\mathcal{N}^{*}}(\\{\textit{s}_{0,1}\\},\textit{s}_{1,1})=0.8$
and
$\textit{PreSum}_{1}^{\mathcal{N}^{*}}(\\{\textit{s}_{0,1}\\},\textit{s}_{1,2})=1.0$
whose difference is $\leq 0.2=\delta$. $\mathcal{N}/_{\delta}\mathcal{P}$
consists of $\mathcal{N}^{*}_{1}$ and $\mathcal{N}^{*}_{2}$ in Figure 3 (top
right and bottom), one which is obtained by choosing the pre-sum corresponding
to $\textit{s}_{1,1}$ and other by choosing the pre-sum corresponding to
$\textit{s}_{1,2}$.

Our objective is to give a bound on the deviation of the semantics of any
$\mathcal{N}^{\prime}\in\mathcal{N}/_{\delta}\mathcal{P}$ from that of
$\mathcal{N}$. We start by quantifying this deviation in one step of
computation. For that, we extend the notion of consistent valuations to an
approximate notion, wherein we require the valuations of related states to be
within a bound rather than match exactly.

###### Definition 11

A valuation $\textit{v}\in\textit{Val}(\mathcal{S}_{i})$ is
$\epsilon,\mathcal{P}$-consistent, if for all
$\textit{s}_{1},\textit{s}_{2}\in\mathcal{S}_{i}$ with
$\textit{s}_{1}\mathcal{P}_{i}\textit{s}_{2}$,
$|\textit{v}(\textit{s}_{1})-\textit{v}(\textit{s}_{2})|\leq\epsilon$.

Our next step is to establish a relation between the valuation propagation in
$\mathcal{N}$ and any
$\mathcal{N}^{\prime}\in\mathcal{N}/_{\delta}\mathcal{P}$ analogous to Lemma
2. First, we will need to relax the notion of the abstraction of a valuation,
however, unlike in the previous case, we obtain a set of abstractions
$\alpha^{\epsilon}(\textit{v})$.

###### Definition 12

Let $\mathcal{P}$ be a partition of $\mathcal{N}$, and
$\textit{v}\in\textit{Val}(\mathcal{S}_{i})$. The $\epsilon$-abstraction of v,
denoted, $\alpha^{\epsilon}(\textit{v})_{\mathcal{N},\mathcal{P}}$, consists
of $\hat{\textit{v}}\in\textit{Val}(\mathcal{P}_{i})$ such that for all
$\hat{\textit{s}}\in\mathcal{P}_{i},\textit{s}\in\hat{\textit{s}}$,
$|\hat{\textit{v}}(\hat{\textit{s}})-\textit{v}(\textit{s})|\leq\epsilon$.

When $\mathcal{N}$ and $\mathcal{P}$ are clear from the context, we will drop
the subscript and write
$\alpha^{\epsilon}(\textit{v})_{\mathcal{N},\mathcal{P}}$ as just
$\alpha^{\epsilon}(\textit{v})$. The next result states that the
$\epsilon$-abstraction for any $\epsilon,\mathcal{P}$-consistent valuation is
non-empty.

###### Proposition 1

Let $\textit{v}\in\textit{Val}(\mathcal{S}_{i})$ be an
$\epsilon,\mathcal{P}$-consistent valuation. Then
$\alpha^{\epsilon}(\textit{v})$ is non-empty.

###### Proof

Note that the valuation $\hat{\textit{v}}$, given by
$\hat{\textit{v}}(\hat{\textit{s}})=\textit{v}(\textit{s})$ for some
$\textit{s}\in\hat{\textit{s}}$ gives a valuation in
$\alpha^{\epsilon}(\textit{v})_{\mathcal{N},\mathcal{P}}$.

The converse of the above theorem also holds with a slight modification of the
error.

###### Proposition 2

Let $\textit{v}\in\textit{Val}(\mathcal{S}_{i})$, such that
$\alpha^{\epsilon}(\textit{v})_{\mathcal{N},\mathcal{P}}$ is non-empty. Then,
v is a $2\epsilon,\mathcal{P}$-consistent valuation.

###### Proof

Note that there is some $\hat{\textit{v}}$, such that
$\forall\hat{\textit{s}}\in\mathcal{P}_{i},\textit{s}\in\hat{\textit{s}}$,
$|\hat{\textit{v}}(\hat{\textit{s}})-\textit{v}(\textit{s})|\leq\epsilon$.
Then for all $\textit{s},\textit{s}^{\prime}\in\hat{\textit{s}}$,
$|\textit{v}(\textit{s})-\textit{v}(\textit{s}^{\prime})|\leq 2\epsilon$.

Now, we give a bound on the deviation of the output of the $i$-th layer of
$\mathcal{N}/_{\delta}\mathcal{P}$ from that of $\mathcal{N}$ in terms of the
deviation in their inputs. Let
$L(A_{i})=\max_{\textit{s}^{\prime}\in\mathcal{S}_{i}}L(A_{i}(\textit{s}^{\prime}))$.

###### Lemma 3

Let $\mathcal{P}$ be a $\delta$-bisimulation on $\mathcal{N}$, and
$\textit{v}\in\textit{Val}(\mathcal{S}_{i-1})$ be
$\epsilon,\mathcal{P}$-consistent. Then, for every
$\hat{\textit{v}}\in\alpha^{\epsilon}(\textit{v})$, and
$\mathcal{N}^{\prime}\in\mathcal{N}/_{\delta}\mathcal{P}$,

$[\\![\mathcal{N}^{\prime}]\\!]_{i}(\hat{\textit{v}})\in\alpha^{\epsilon^{\prime}}([\\![\mathcal{N}]\\!]_{i}(\textit{v})),$

where $\epsilon^{\prime}=\textit{a}_{i}\epsilon+\textit{b}_{i}$,
$\textit{a}_{i}=L(A_{i})|\mathcal{S}_{i-1}||\\!|W_{i}|\\!|_{\infty}$, and
$\textit{b}_{i}=L(A_{i})(|\mathcal{P}_{i-1}||\\!|\textit{v}|\\!|_{\infty}+1)\delta$.

###### Proof

Let $\textit{v}^{\prime}=[\\![\mathcal{N}]\\!]_{i}(\textit{v})$ and
$\hat{\textit{v}}^{\prime}=[\\![\mathcal{N}^{\prime}]\\!]_{i}(\hat{\textit{v}})$.
We need to show that
$\hat{\textit{v}}^{\prime}\in\alpha^{\epsilon^{\prime}}(\textit{v}^{\prime})$.
Consider any $\hat{\textit{s}}^{\prime}\in\widehat{\mathcal{S}}_{i}$ and
$\textit{s}^{\prime}\in\hat{\textit{s}}^{\prime}$. We need to show that
$|\hat{\textit{v}}^{\prime}(\hat{\textit{s}}^{\prime})-\textit{v}^{\prime}(\textit{s}^{\prime})|\leq\epsilon^{\prime}$.

Since,
$\hat{\textit{v}}^{\prime}=[\\![\mathcal{N}^{\prime}]\\!]_{i}(\hat{\textit{v}})$,
from the semantics of $\mathcal{N}^{\prime}$, we have

$\hat{\textit{v}}^{\prime}(\hat{\textit{s}}^{\prime})=\widehat{A}_{i}(\hat{\textit{s}}^{\prime})\big{(}\sum_{\hat{\textit{s}}\in\widehat{\mathcal{S}}_{i-1}}\widehat{W}_{i}(\hat{\textit{s}},\hat{\textit{s}}^{\prime})\hat{\textit{v}}(\hat{\textit{s}})+\widehat{b}_{i}(\hat{\textit{s}}^{\prime})\big{)},$

and from the fact that
$\mathcal{N}^{\prime}\in\mathcal{N}/_{\delta}\mathcal{P}$, we have
$\widehat{W}_{i}(\hat{\textit{s}},\hat{\textit{s}}^{\prime})=\textit{PreSum}_{i}^{\mathcal{N}}(\hat{\textit{s}},\textit{s}^{\prime}_{1})$
for some $\textit{s}^{\prime}_{1}\in\hat{\textit{s}}^{\prime}$,
$\widehat{b}_{i}(\hat{\textit{s}}^{\prime})=b_{i}(\textit{s}^{\prime}_{2})$
for some $\textit{s}^{\prime}_{2}\in\hat{\textit{s}}^{\prime}$. Since
$\mathcal{P}$ is a $\delta$-bisimulation,
$|\textit{PreSum}_{i}^{\mathcal{N}}(\hat{\textit{s}},\textit{s}^{\prime}_{1})-\textit{PreSum}_{i}^{\mathcal{N}}(\hat{\textit{s}},\textit{s}^{\prime})|\leq\delta$,
$|b_{i}(\textit{s}^{\prime}_{2})-b_{i}(\textit{s}^{\prime})|\leq\delta$, and
$\widehat{A}_{i}(\hat{\textit{s}}^{\prime})=A_{i}(\textit{s}^{\prime})$.
Therefore,

$\hat{\textit{v}}^{\prime}(\hat{\textit{s}}^{\prime})=A_{i}(\textit{s}^{\prime})\big{(}\sum_{\hat{\textit{s}}\in\mathcal{P}_{i-1}}(\textit{PreSum}_{i}^{\mathcal{N}}(\hat{\textit{s}},\textit{s}^{\prime})+\delta_{\hat{\textit{s}}})\hat{\textit{v}}(\hat{\textit{s}})+b_{i}(\textit{s}^{\prime})+\delta_{\textit{s}^{\prime}}\big{)},$
$=A_{i}(\textit{s}^{\prime})\big{(}\sum_{\hat{\textit{s}}\in\mathcal{P}_{i-1}}\textit{PreSum}_{i}^{\mathcal{N}}(\hat{\textit{s}},\textit{s}^{\prime})\hat{\textit{v}}(\hat{\textit{s}})+b_{i}(\textit{s}^{\prime})+\epsilon_{1}+\delta_{\textit{s}^{\prime}}\big{)},$

where
$\epsilon_{1}=\sum_{\hat{\textit{s}}\in\mathcal{P}_{i-1}}\delta_{\hat{\textit{s}}}\hat{\textit{v}}(\hat{\textit{s}})$
and
$\delta_{\hat{\textit{s}}},\delta_{\textit{s}^{\prime}}\in[-\delta,\delta]$.
We will examine the terms in the above expression in more detail.

$\sum_{\hat{\textit{s}}\in\mathcal{P}_{i-1}}\textit{PreSum}_{i}^{\mathcal{N}}(\hat{\textit{s}},\textit{s}^{\prime})\hat{\textit{v}}(\hat{\textit{s}})=\sum_{\hat{\textit{s}}\in\mathcal{P}_{i-1}}[\sum_{\textit{s}\in\hat{\textit{s}}}W_{i}(\textit{s},\textit{s}^{\prime})\hat{\textit{v}}(\hat{\textit{s}})]$

(Further, since, $\hat{\textit{v}}\in\alpha^{\epsilon}(\textit{v})$, we have
for any $\textit{s}\in\hat{\textit{s}}$,
$|\hat{\textit{v}}(\hat{\textit{s}})-\textit{v}(\textit{s})|\leq\epsilon$.)

$=\sum_{\hat{\textit{s}}\in\mathcal{P}_{i-1}}[\sum_{\textit{s}\in\hat{\textit{s}}}W_{i}(\textit{s},\textit{s}^{\prime})(\textit{v}(\textit{s})+\epsilon_{\textit{s}})]=\sum_{\textit{s}\in\mathcal{S}_{i-1}}W_{i}(\textit{s},\textit{s}^{\prime})(\textit{v}(\textit{s})+\epsilon_{\textit{s}})]$
$=\sum_{\textit{s}\in\mathcal{S}_{i-1}}W_{i}(\textit{s},\textit{s}^{\prime})\textit{v}(\textit{s})+\sum_{\textit{s}\in\mathcal{S}_{i-1}}W_{i}(\textit{s},\textit{s}^{\prime})\epsilon_{\textit{s}}$

Plugging the above into the expression for
$\hat{\textit{v}}^{\prime}(\hat{\textit{s}}^{\prime})$, we obtain

$\hat{\textit{v}}^{\prime}(\hat{\textit{s}}^{\prime})=A_{i}(\textit{s}^{\prime})\big{(}\sum_{\textit{s}\in\mathcal{S}_{i-1}}W_{i}(\textit{s},\textit{s}^{\prime})\textit{v}(\textit{s})+b_{i}(\textit{s}^{\prime})+\epsilon_{1}+\epsilon_{2}+\delta_{\textit{s}^{\prime}}\big{)}$

where
$\epsilon_{2}=\sum_{\hat{\textit{s}}\in\mathcal{P}_{i-1}}\delta_{\hat{\textit{s}}}\hat{\textit{v}}(\hat{\textit{s}})$.
Note that the expression for
$\hat{\textit{v}}^{\prime}(\hat{\textit{s}}^{\prime})$ looks similar to
$\textit{v}^{\prime}(\textit{s}^{\prime})=A_{i}(\textit{s}^{\prime})\big{(}\sum_{\textit{s}\in\mathcal{S}_{i-1}}W_{i}(\textit{s},\textit{s}^{\prime})\textit{v}(\textit{s})+b_{i}(\textit{s}^{\prime}))$
except for the additional error terms
$\epsilon_{1}+\epsilon_{2}+\delta_{\textit{s}^{\prime}}$. From the Lipschitz
continuity of $A_{i}(\textit{s}^{\prime})$, we obtain

$|\hat{\textit{v}}^{\prime}(\hat{\textit{s}}^{\prime})-\textit{v}^{\prime}(\textit{s}^{\prime})|\leq
L(A_{i})(\textit{s}^{\prime})(|\epsilon_{1}+\epsilon_{2}+\delta_{\textit{s}^{\prime}}|)$

Note that $L(A_{i})(\textit{s}^{\prime})\leq L(A_{i})$,
$|\epsilon_{1}|=|\sum_{\textit{s}\in\mathcal{S}_{i-1}}W_{i}(\textit{s},\textit{s}^{\prime})\epsilon_{\textit{s}}|\leq|\mathcal{S}_{i-1}||\\!|W_{i}|\\!|_{\infty}\epsilon$,
$|\epsilon_{1}|=|\sum_{\hat{\textit{s}}\in\mathcal{P}_{i-1}}\delta_{\hat{\textit{s}}}\hat{\textit{v}}(\hat{\textit{s}})|\leq|\mathcal{P}_{i-1}|\delta|\\!|\textit{v}|\\!|_{\infty}$,
and $|\delta_{\textit{s}^{\prime}}|\leq\delta$. Hence,

$|\hat{\textit{v}}^{\prime}(\hat{\textit{s}}^{\prime})-\textit{v}^{\prime}(\textit{s}^{\prime})|\leq
L(A_{i})(\textit{s}^{\prime})(|\epsilon_{1}+\epsilon_{2}+\delta_{\textit{s}^{\prime}}|)\leq
L(A_{i})(|\mathcal{S}_{i-1}||\\!|W_{i}|\\!|_{\infty}\epsilon+|\mathcal{P}_{i-1}|\delta|\\!|\textit{v}|\\!|_{\infty}+\delta)$
$=L(A_{i})|\mathcal{S}_{i-1}||\\!|W_{i}|\\!|_{\infty}\epsilon+L(A_{i})(|\mathcal{P}_{i-1}||\\!|\textit{v}|\\!|_{\infty}+1)\delta=\epsilon^{\prime}$

Lemma 3 provides a bound on the error propagation in one step. The next
theorem provides a global bound on the deviation of the output of the reduced
system with respect to that of the given neural network. Let
$L(A)=\max_{i}L(A_{i})$, $|\mathcal{P}|=\max_{i}|\mathcal{P}_{i}|$,
$|\\!|W|\\!|_{\infty}=\max_{i}|\\!|W_{i}|\\!|_{\infty}$ and
$|\mathcal{S}|=|\max_{i}\mathcal{S}_{i}|$.

###### Theorem 5.1

Let $\mathcal{P}$ be a $\delta$-bisimulation on $\mathcal{N}$, and
$\textit{v}\in\textit{Val}(\mathcal{S}_{0})$ be
$\epsilon,\mathcal{P}$-consistent. Then, for every
$\hat{\textit{v}}\in\alpha^{\epsilon}(\textit{v})$, and
$\mathcal{N}^{\prime}\in\mathcal{N}/_{\delta}\mathcal{P}$,

$[\\![\mathcal{N}^{\prime}]\\!](\hat{\textit{v}})\in\alpha^{\epsilon^{\prime\prime}}([\\![\mathcal{N}]\\!](\textit{v})),$

where $\epsilon^{\prime\prime}=[(2/a)^{k}-1]\textit{b}/(2\textit{a}-1)$,
$\textit{a}=L(A)|\mathcal{S}||\\!|W|\\!|_{\infty}$, and
$\textit{b}=L(A)(|\mathcal{P}|L(\mathcal{N})|\\!|\textit{v}|\\!|_{\infty}+1)\delta$.

###### Proof

Let us define:

$\textit{v}_{0}=\textit{v},\hat{\textit{v}}_{0}=\hat{\textit{v}},\epsilon_{0}=\epsilon^{\prime}_{0}=0$

and for all $i\in(k]$,

$\textit{v}_{i}=[\\![\mathcal{N}]\\!]_{i}(\textit{v}),\hat{\textit{v}}_{i}=[\\![\mathcal{N}^{\prime}]\\!]_{i}(\hat{\textit{v}}).$
$\epsilon^{\prime}_{i}=\textit{a}\epsilon_{i-1}+\textit{b},\epsilon_{i}=2\epsilon^{\prime}_{i}.$

We will show by induction on $i$ that for all $i\in[k]$, $\textit{v}_{i}$ is
$\epsilon_{i},\mathcal{P}$-consistent and
$\hat{\textit{v}}_{i}\in\alpha^{\epsilon^{\prime}_{i}}(\textit{v}_{i})$.

Base case: Base case trivially holds from the assumptions of the theorem
statement.

Induction Step: For $i\in(k]$, we know from Lemma 3, that if
$\textit{v}_{i-1}\in\textit{Val}(\mathcal{S}_{i-1})$ is
$\epsilon_{i-1},\mathcal{P}$-consistent and
$\hat{\textit{v}}_{i-1}\in\alpha^{\epsilon_{i-1}}(\textit{v}_{i-1})$, then
$\hat{\textit{v}}_{i}=[\\![\mathcal{N}^{\prime}]\\!]_{i}(\hat{\textit{v}}_{i-1})\in\alpha^{\epsilon^{\prime}}([\\![\mathcal{N}]\\!]_{i}(\textit{v}_{i-1}))=\alpha^{\epsilon^{\prime}}(\textit{v}_{i})$,
where $\epsilon^{\prime}=\textit{a}_{i}\epsilon_{i-1}+\textit{b}_{i}$.

$\textit{a}_{i}=L(A_{i})|\mathcal{S}_{i-1}||\\!|W_{i}|\\!|_{\infty}\leq
L(A)|\mathcal{S}||\\!|W|\\!|_{\infty}=\textit{a},$
$\textit{b}_{i}=L(A_{i})(|\mathcal{P}_{i-1}||\\!|\textit{v}_{i}|\\!|_{\infty}+1)\delta\leq
L(A)(|\mathcal{P}|L(\mathcal{N})|\\!|\textit{v}|\\!|_{\infty}+1)\delta=\textit{b}$

Hence, $\epsilon\leq\epsilon^{\prime}_{i}$ and
$\hat{\textit{v}}_{i}\in\alpha^{\epsilon^{\prime}_{i}}(\textit{v}_{i})$.
Further from Proposition 2, we obtain $\textit{v}_{i}$ is
$\epsilon_{i},\mathcal{P}$-consistent.

We will show that $\epsilon^{\prime}_{k}=\epsilon^{\prime\prime}$. Unrolling
the recursive equation, we obtain
$\epsilon^{\prime}_{i}=2\textit{a}\epsilon^{\prime}_{i-1}+\textit{b}=(2\textit{a})^{i}\epsilon^{\prime}_{0}+[(2\textit{a})^{i-1}+\cdots+1]\textit{b}=[(2/a)^{i}-1]\textit{b}/(2\textit{a}-1)$.
Hence,

$\epsilon^{\prime}_{k}=[(2/a)^{k}-1]\textit{b}/(2\textit{a}-1)=\epsilon^{\prime\prime}$

We finish the proof by noting that
$[\\![\mathcal{N}^{\prime}]\\!](\hat{\textit{v}})=\hat{\textit{v}}_{k}\in\alpha^{\epsilon^{\prime}_{k}}(\textit{v}_{k})=\alpha^{\epsilon^{\prime\prime}}([\\![\mathcal{N}]\\!](\textit{v}))$.

###### Remark 1

Note that for $\delta=0$, all the notions and results reduce to that of NN-
bisimulation.

##  6 Minimization algorithm

In this section, we show that there is a coarsest NN-bisimulation for a given
NN, that encompasses all other bisimulations. This implies that the induced
reduced network with respect to this coarsest bisimulation is the smallest NN-
bisimulation equivalent network. We will provide an algorithm that outputs the
coarsest NN-bisimulation.

We note that a coarsest $\delta$-NN-bisimulation may not exist in general. For
instance, consider the NN $\mathcal{N}^{*}$ from Figure 3, along with the
$0.2$-bisimulation $\mathcal{P}$ that induces the reduced systems
$\mathcal{N}^{*}_{1}$ and $\mathcal{N}^{*}_{2}$. There is another
$0.2$-bisimulation $\mathcal{P}^{\prime}$ which is obtained by merging
$\textit{s}_{1,2}$ and $\textit{s}_{1,3}$ instead of $\textit{s}_{1,1}$ and
$\textit{s}_{1,2}$ as in $\mathcal{P}$. Note that the reduced networks in
$\mathcal{N}^{*}/_{0.2}\mathcal{P}$ and
$\mathcal{N}^{*}/_{0.2}\mathcal{P}^{\prime}$ have the same size. However,
there is no $0.2$-bisimulation that is coarser than both $\mathcal{P}$ and
$\mathcal{P}^{\prime}$, since, that would require merging
$\textit{s}_{1,1},\textit{s}_{1,2}$ and $\textit{s}_{1,3}$, which would
violate the $0.2$ bound on the difference between the pre-sums of
$\textit{s}_{1,1}$ and $\textit{s}_{1,3}$.

The broad algorithm for minimization consists of starting with a partition in
which all the nodes in a layer are merged together and then splitting them
such that the regions in the partition respect the activation functions,
biases and the pre-sums. We use the function
$\textit{SplitActBias}(\mathcal{S})$ in the algorithm that splits a set of
nodes $\mathcal{S}$ into maximal groups such that the elements in each group
agree on the activation functions and the biases. More precisely,
$\textit{SplitActBias}(\mathcal{S})$ takes
$\mathcal{S}\subseteq\mathcal{P}_{i}$ as input and returns a partition
$\mathcal{P}_{\mathcal{S}}$ such that for all
$\textit{s}_{1},\textit{s}_{2}\in\mathcal{S}$,
$\textit{s}_{1}\mathcal{P}_{\mathcal{S}}\textit{s}_{2}$ if and only if
$A_{i}(\textit{s}_{1})=A_{i}(\textit{s}_{2})$ and
$b_{i}(\textit{s}_{1})=b_{i}(\textit{s}_{2})$. Further, we split those regions
that have nodes with inconsistent pre-sums. Next, we define inconsistent pairs
of regions with respect to pre-sums and the corresponding splitting
operations.

###### Definition 13

Given a partition $\mathcal{P}=\\{\mathcal{P}_{i}\\}_{i}$ of NN $\mathcal{N}$,
a region $\mathcal{S}^{\prime}\in\mathcal{P}_{i}$ is inconsistent in
$\mathcal{N}$ with respect to $\mathcal{S}\in\mathcal{P}_{i-1}$, written
$(\mathcal{S}^{\prime},\mathcal{S})$ inconsistent, if there exist
$\textit{s}^{\prime}_{1},\textit{s}^{\prime}_{2}\in\mathcal{S}^{\prime}$, such
that
$\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S},\textit{s}^{\prime}_{1})\not=\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S},\textit{s}^{\prime}_{2})$.

The algorithm searches for inconsistent pairs
$(\mathcal{S}^{\prime},\mathcal{S})$ and splits $\mathcal{S}^{\prime}$ into
maximal groups such that all nodes in a group have the same pre-sum with
respect to $\mathcal{S}$. More precisely,
$\textit{SplitPre}(\mathcal{S}^{\prime},\mathcal{S})$ takes
$\mathcal{S}^{\prime}$ and $\mathcal{S}$ as input and returns a partition
$\mathcal{P}^{\prime}$ of $\mathcal{S}^{\prime}$ such that
$\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S},\textit{s}^{\prime}_{1})=\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S},\textit{s}^{\prime}_{1})$
if and only if
$\textit{s}^{\prime}_{1}\mathcal{P}^{\prime}\textit{s}^{\prime}_{2}$.

Input: A NN $\mathcal{N}$

Output: Coarsest Bisimulation $\mathcal{P}$, and Minimized NN
$\mathcal{N}/\mathcal{P}$

1 begin

2 $\mathcal{P}=\\{\mathcal{S}_{0}\\}$

3 for  _$i\in(k]$_ do

4 $\mathcal{P}=\mathcal{P}\cup\textit{SplitActBias}(\mathcal{S}_{i})$

5 while  _Exists $\mathcal{S},\mathcal{S}^{\prime}\in\mathcal{P}$, such that
$(\mathcal{S},\mathcal{S}^{\prime})$ inconsistent_ do

6
$\mathcal{P}=\mathcal{P}\backslash\\{\mathcal{S}^{\prime}\\}\cup\textit{SplitPre}(\mathcal{S}^{\prime},\mathcal{S})$

7

8 return Return $\mathcal{P}$ and $\mathcal{N}/\mathcal{P}$

9

Algorithm 1 MinNN: Minimization Algorithm

Next, we show that Algorithm 1 returns the coarsest bisimulation, and hence,
the reduced network is the smallest bisimulation equivalent network.

###### Definition 14

A partition $\mathcal{P}$ of $\mathcal{N}$ is the coarsest bisimulation, if it
is an NN bisimulation and it is coarser than every NN-bisimulation
$\mathcal{P}^{\prime}$ of $\mathcal{N}$.

###### Theorem 6.1

Algorithm 1 terminates and returns the coarsest bisimulation $\mathcal{P}$ of
$\mathcal{N}$.

###### Proof

Termination of the algorithm is straightforward, since, if there exists an
inconsistent pair $(\mathcal{S}^{\prime},\mathcal{S})$, then
$\textit{SplitPre}(\mathcal{S}^{\prime},\mathcal{S})$ splits
$\mathcal{S}^{\prime}$ into at least two regions. Hence, the number of regions
in $\mathcal{P}$ strictly increases. However, since, $\mathcal{N}$ has
finitely many nodes, the number of regions in $\mathcal{P}$ is upper-bounded.

Next, we will argue that $\mathcal{P}$ that is returned is an NN-bisimulation.
After the $\textit{SplitActBias}(\mathcal{S}_{i})$ operations, $\mathcal{P}$
only consists of regions which agree on the activation functions and biases.
When the while loop terminates, there are no inconsistent pairs, that is, the
pre-sum condition of the bisimulation definition is satisfied. Hence, the
value of $\mathcal{P}$ when exiting the while loop is an NN-bisimulation.

To show that $\mathcal{P}$ is the coarsest bisimulation, it remains to show
that $\mathcal{P}$ is coarser than any bisimulation of $\mathcal{N}$. Let
$\mathcal{P}^{\prime}$ be any bisimulation of $\mathcal{N}$. We will show that
$\mathcal{P}^{\prime}$ is finer than $\mathcal{P}$ at every stage of the
algorithm.

Note that after exiting the for loop, $\mathcal{P}$ contains the maximal
groups which agree on both the activation functions and biases. Every region
of $\mathcal{P}^{\prime}$ has to agree on the activation functions and biases,
since it is a bisimulation. So, every region of $\mathcal{P}^{\prime}$ is
contained in some regions of $\mathcal{P}$, that is,
$\mathcal{P}^{\prime}\preceq\mathcal{P}$.

Next, we show that $\mathcal{P}^{\prime}\preceq\mathcal{P}$ is an invariant
for the while loop, that is, if it holds at the beginning of the loop, then it
also holds at the end of the loop. So, when the while loop exits, we still
have $\mathcal{P}^{\prime}\preceq\mathcal{P}$. More precisely, we need to show
that if $\mathcal{P}^{\prime}\preceq\mathcal{P}$, then replacing
$\mathcal{S}^{\prime}$ by
$\textit{SplitPre}(\mathcal{S}^{\prime},\mathcal{S})$ will still result in a
partition that is coarser than $\mathcal{P}^{\prime}$. In particular, we need
to ensure that each region of $\mathcal{P}^{\prime}$ that is contained in
$\mathcal{S}^{\prime}$ is not split by the
$\textit{SplitPre}(\mathcal{S}^{\prime},\mathcal{S})$ operation. Suppose a
region $\mathcal{S}^{\prime\prime}\subseteq\mathcal{S}^{\prime}$ of
$\mathcal{P}^{\prime}$ is split, then there exists
$\textit{s}^{\prime\prime}_{1},\textit{s}^{\prime\prime}_{2}\in\mathcal{S}^{\prime\prime}$
such that
$\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S},\textit{s}^{\prime\prime}_{1})\not=\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S},\textit{s}^{\prime\prime}_{1})$.
But $\mathcal{S}$ is the disjoint union of some sets
$\\{\mathcal{S}^{\prime\prime}_{1},\cdots,\mathcal{S}^{\prime\prime}_{l}\\}$
of $\mathcal{P}^{\prime}$. Hence,
$\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S}^{\prime\prime}_{i},\textit{s}^{\prime\prime}_{1})\not=\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S}^{\prime\prime}_{i},\textit{s}^{\prime\prime}_{1})$
for some $i$, since
$\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S},\textit{s}^{\prime\prime})=\sum_{i}\textit{PreSum}_{i}^{\mathcal{N}}(\mathcal{S}^{\prime\prime}_{i},\textit{s}^{\prime\prime})$.
However, this contradicts the fact that $\mathcal{P}^{\prime}$ is an NN-
bisimulation.

Next, we present some complexity results on checking if a partition is a
bisimulation/$\delta$-bisimulation, complexity of constructing reduced systems
from a bisimulation/$\delta$-bisimulation and the complexity of computing the
coarsest bisimulation.

###### Theorem 6.2

Given an NN $\mathcal{N}$, a partition $\mathcal{P}$ and $\epsilon\geq 0$,
checking if $\mathcal{P}$ is a bisimulation and checking if $\mathcal{P}$ is
an $\delta$-NN-bisimulation both take time $\textit{O}(m)$, where $m$ is the
number of edges of $\mathcal{N}$. Further, constructing
$\mathcal{N}/\mathcal{P}$ for some
$\mathcal{N}^{\prime}\in\mathcal{N}/_{\delta}\mathcal{P}$ takes time
$\textit{O}(m)$ as well.

###### Proof

To check if $\mathcal{P}$ is a bisimulation, we can iterate over all the nodes
in a region to check if they have same activation function, bias, and pre-sums
with respect to every region of $\mathcal{P}_{i-1}$. In doing so, we need to
access each node and each edge at most once, hence, the complexity is bounded
by $\textit{O}(m)$. For the $\delta$-bisimulation, we need to check if the
biases and pre-sums are within $\epsilon$. We can compute the biases and pre-
sums in one pass over the network in time $\textit{O}(m)$ as before. Then we
can find the max and min values of the bias/pre-sum values within each region,
and check if the max and min values are within $\epsilon$, this will take time
$\textit{O}(m)$. For constructing the reduced system, we need to find the
activation functions and biases of all the nodes in the reduced system, and
the weight on the edge between two groups. The total computation needs to
access each edge at most once.

###### Theorem 6.3

The minimization algorithm has a time complexity of
$\textit{O}(\hat{n}(m+n\log n))$, where $n$ is the number of nodes and $m$ is
the number of edges of $\mathcal{N}$, and $\hat{n}$ is the number of nodes in
the minimized neural network.

###### Proof

$\textit{SplitActBias}(\mathcal{S}_{i})$ needs to sort the elements in every
group by the activation function/bias values, hence, takes time
$\textit{O}(n\log n)$. Finding an inconsistent pair takes the same time as
checking whether $\mathcal{P}$ is a bisimulation, that is, $\textit{O}(m)$.
$\textit{SplitPre}(\mathcal{S}^{\prime},\mathcal{S})$ take time at most
$\textit{O}(m)$ to compute the pre-sums and $\textit{O}(n\log n)$ to split.
Replacing $\mathcal{S}^{\prime}$ by
$\textit{SplitPre}(\mathcal{S}^{\prime},\mathcal{S})$ takes time at most
$\textit{O}(\hat{n})$ which is upper-bounded by $\textit{O}(n)$. So, each loop
takes time $\textit{O}(m+n\log n)$. The number of iterations of the while loop
is upper bounded by the number of regions in the minimized neural network,
that is, $\textit{O}(\hat{n})$. Hence, the minimization algorithm has a
runtime of $\textit{O}(\hat{n}(m+n\log n))$.

##  7 Conclusions

We presented the notions of bisimulation and approximate bisimulation for
neural networks that provide semantic equivalence and semantic closeness,
respectively, and are applicable to neural networks with a wide range of
activation functions. These provide foundational theoretical tools for
exploring the trade-off between the amount of reduction and the semantic
deviation in an approximation based verification paradigm for neural networks.
Our future work will focus on experimental analysis of this trade-off on large
scale neural networks. The notions of bisimulation explored are syntactic in
nature, and we will explore semantic notions in the future. We provide a
minimization algorithm for finding the smallest NN that is bisimilar to a
given neural network. Though a unique minimal network does not exist with
respect to $\delta$-bisimulations, we will explore heuristics for constructing
small networks that are $\delta$-bisimilar.

## References

  * [1] Ashok, P., Hashemi, V., Kretinsky, J., Mohr, S.: Deepabstract: Neural network abstraction for accelerating verification (2020)
  * [2] Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind Series). The MIT Press (2008)
  * [3] Bunel, R., Turkaslan, I., Torr, P.H.S., Kohli, P., Kumar, M.P.: Piecewise linear neural network verification: A comparative study. CoRR (2017)
  * [4] Cheng, Y., Wang, D., Zhou, P., Zhang, T.: A survey of model compression and acceleration for deep neural networks. CoRR (2017)
  * [5] Deng, L., Li, G., Han, S., Shi, L., Xie, Y.: Model compression and hardware acceleration for neural networks: A comprehensive survey. Proceedings of the IEEE 108(4), 485–532 (2020)
  * [6] Dutta, S., Jha, S., Sankaranarayanan, S., Tiwari, A.: Output range analysis for deep feedforward neural networks. In: Dutle, A., Muñoz, C., Narkawicz, A. (eds.) NASA Formal Methods. pp. 121–138. Springer International Publishing (2018)
  * [7] Elboher, Y.Y., Gottschlich, J., Katz, G.: An abstraction-based framework for neural network verification. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I. Lecture Notes in Computer Science, vol. 12224, pp. 43–65. Springer (2020)
  * [8] Girard, A., Julius, A.A., Pappas, G.J.: Approximate simulation relations for hybrid systems. Discrete Event Dynamic Systems 18(2), 163–179 (2008)
  * [9] Girard, A., Pappas, G.J.: Approximate bisimulation relations for constrained linear systems. Automatica 43(8), 1307–1317 (2007)
  * [10] Girard, A., Pola, G., Tabuada, P.: Approximately bisimilar symbolic models for incrementally stable switched systems. In: Proceedings of the International Conference on Hybrid Systems: Computation and Control. pp. 201–214 (2008)
  * [11] Huang, X., Kroening, D., Kwiatkowska, M.Z., Ruan, W., Sun, Y., Thamo, E., Wu, M., Yi, X.: Safety and trustworthiness of deep neural networks: A survey. CoRR abs/1812.08342 (2018)
  * [12] Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An efficient SMT solver for verifying deep neural networks. CoRR (2017)
  * [13] Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)
  * [14] Milner, R.: Communication and Concurrency. Prentice-Hall, Inc (1989)
  * [15] Prabhakar, P., Afzal, Z.R.: Abstraction based output range analysis for neural networks (2019)
  * [16] Pulina, L., Tacchella, A.: An abstraction-refinement approach to verification of artificial neural networks. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification. pp. 243–257. Springer Berlin Heidelberg, Berlin, Heidelberg (2010)
  * [17] Sotoudeh, M., Thakur, A.: Abstract neural networks. In: Static Analysis Symposium (2020)
  * [18] Virmaux, A., Scaman, K.: Lipschitz regularity of deep neural networks: analysis and efficient estimation. In: Bengio, S., Wallach, H., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems 31, pp. 3835–3844. Curran Associates, Inc. (2018)
  * [19] Xiang, W., Musau, P., Wild, A.A., Lopez, D.M., Hamilton, N., Yang, X., Rosenfeld, J.A., Johnson, T.T.: Verification for machine learning, autonomy, and neural networks survey. CoRR abs/1810.01989 (2018)
  * [20] Xiang, W., Tran, H., Johnson, T.T.: Output reachable set estimation and verification for multi-layer neural networks. CoRR abs/1708.03322 (2017)