11institutetext: BTU Cottbus-Senftenberg, Lehrstuhl Theoretische Informatik,
Platz der Deutschen Einheit 1, 03046 Cottbus, Germany, https://www.b-tu.de/
11email<EMAIL_ADDRESS>
# Robustness Verification in Neural Networks

Adrian Wurm ID

Abstract: In this paper we investigate formal verification problems for Neural
Network computations. Of central importance will be various robustness and
minimization problems such as: Given symbolic specifications of allowed inputs
and outputs in form of Linear Programming instances, one question is whether
there do exist valid inputs such that the network computes a valid output? And
does this property hold for all valid inputs? Do two given networks compute
the same function? Is there a smaller network computing the same function?

The complexity of these questions have been investigated recently from a
practical point of view and approximated by heuristic algorithms. We
complement these achievements by giving a theoretical framework that enables
us to interchange security and efficiency questions in neural networks and
analyze their computational complexities. We show that the problems are
conquerable in a semi-linear setting, meaning that for piecewise linear
activation functions and when the sum- or maximum metric is used, most of them
are in P or in NP at most.

##  1 Introduction

Neural networks are widely used in all kinds of data processing, especially on
seemingly unfeasible tasks such as image[15] and language recognition[10], as
well as applications in medicine [16], and prediction of stock markets [6],
just to mention a few. Khan et al. [14] provide a survey of such applications,
a mathematically oriented textbook concerning structural issues related to
Deep Neural Networks is provided by [3].

Neural networks are nowadays also made use of in safety-critical systems like
autonomous driving[8] or power grid management. In such a setting, when
security issues become important, aspects of certification come into play [11,
7, 17]. If we for example want provable guarantees for certain scenarios to be
unreachable, we first need to formulate them as constraints and precisely
state for which property of a network we want verification.

In the present paper we are interested in studying certain verification
problems for NNs in form of particular robustness and minimization problems
such as: How will a network react to a small perturbation of the input[9]? And
how likely is a network to change the classification of an input that is
altered a little? These probabilities are crucial when for example a self-
driving car is supposed to recognize a speed limit, and they have already been
tackled in practical settings by simulations and heuristic algorithms. These
approaches however will never guarantee safety, because the conditions under
which seemingly correct working nets suddenly tend to decide irrationally
often seem arbitrary and unpredictable [2, 4, 20].

Key results will be that a lot of these questions behave very similar under
reasonable assumptions. Note that the network in principle is allowed to
compute with real numbers, so the valid inputs we are looking for belong to
some space $\mathbb{R}^{n}$, but the network itself is specified by its
discrete structure and rational weights defining the linear combinations
computed by its single neurons.

A huge variety of networks arises when changing the underlying activation
functions. There are of course many activations frequently used in NN
frameworks, and in addition we could extend verification questions to nets
using all kinds of activation. One issue to be discussed is the computational
model in which one argues. If, for example, the typical sigmoid activation
$f(x)=1/(1+e^{-x})$ is used, it has to be specified in which sense it is
computed by the net: For example exactly or approximately, and at which costs
these operations are being performed. In this paper we will cover the most
common activation functions, especially $ReLU$.

The paper is organized as follows: In Section 2 we collect basic notions,
recall the definition of feedforward neural nets as used in this paper as well
as for the metrics that we use. Section 3 studies various robustness
properties and their comparison to each other when using different network
structures and metrics. In Section 4, we give criteria on whether a network is
as small as possible, or if it can be replaced by a smaller network that is
easier to evaluate.

The paper ends with some open questions.

##  2 Preliminaries and Network Decision Problems

We start by defining the problems we are interested in; here, we follow the
definitions and notions of [21] and [19] for everything related to neural
networks. The networks considered are exclusively feedforward. In their most
general form, they can process real numbers and contain rational weights. This
will later on be restricted when necessary.

###### Definition 1

A (feedforward) neural network N is a layered graph that represents a function
of type $\mathbb{R}^{n}\rightarrow\mathbb{R}^{m}$, for some
$n,m\in\mathbb{N}$. The first layer with label $\ell=0$ is called the _input
layer_ and consists of $n$ nodes called _input nodes_. The input value $x_{i}$
of the $i$-th node is also taken as its output $y_{0i}:=x_{i}$. A layer
$1\leq\ell\leq L-2$ is called _hidden_ and consists of $k(\ell)$ nodes called
_computation nodes_. The $i$-th node of layer $\ell$ computes the output
$y_{{\ell}i}=\sigma_{{\ell}i}(\sum\limits_{j}c_{ji}^{({\ell}-1)}y_{({\ell}-1)j}+b_{{\ell}i}))$.
Here, the $\sigma_{{\ell}i}$ are (typically nonlinear) _activation_ functions
(to be specified later on) and the sum runs over all output neurons of the
previous layer. The $c^{({\ell}-1)}_{ji}$ are real constants which are called
_weights_ , and $b_{{\ell}i}$ is a real constant called _bias_. The outputs of
all nodes of layer $\ell$ combined gives the output $(y_{l0},...,y_{l(k-1)})$
of the hidden layer. The final layer $L-1$ is called _output layer_ and
consists of $m$ nodes called _output nodes_. The $i$-th node computes an
output $y_{(L-1)i}$ in the same way as a node in a hidden layer. The output
$(y_{(L-1)0},...,y_{(L-1)(m-1)})$ of the output layer is considered the output
$N(x)$ of the network $N$.

Note that above we allow several different activation functions in a single
network. This basically is because for some results technically the identity
is necessary as a second activation function beside the ’main’ activation
function used. All of our results hold for this scenario already.

Since we want to study its complexity in the Turing model, we restrict all
weights and biases in a NN to be rational numbers. The problem NNReach
involves two Linear Programming LP instances in a decision version, therefore
recall that such an instance consists of a system of (componentwise) linear
inequalities $A\cdot x\leq b$ for rational matrix $A$ and vector $b$ of
suitable dimensions. The decision problem asks for the existence of a real
solution vector $x.$ As usual, we refer to this problem as Linear Program
Feasibility LPF. By abuse of notation, we denote by $A$ also the set described
by the pair $(A,b)$.

As usual for neural networks, we consider different choices for the activation
functions used, but concentrate the most frequently used one, namely
$ReLU(x)=max\\{0,x\\}$. We name nodes after their internal activation
function, so we call nodes with activation function $\sigma(x)=x$ identity
nodes and nodes with activation function $\sigma(x)=ReLU(x)$ $ReLU$-nodes for
example.

We next recall from [21] the definition of the decision problems NNReach, VIP
and NE. These problems have been investigated in [11] and [1], specifically
NNReach in [21], [19] and [13].

###### Definition 2

a) Let $F$ be a set of activation functions from $\mathbb{R}$ to $\mathbb{R}$.
An instance of the _reachability problem for neural networks_ NNReach$(F)$
consists of a (feedforward) neural network $N$ with all its activation
functions belonging to $F$, rational data as weights and biases, and two
instances $A$ and $B$ of LP in decision version with rational data, one with
the input variables of $N$ as variables, and the other with the output
variables of $N$ as variables. These instances are also called _input_ and
_output specifications_ , respectively. The problem is to decide if there
exists an $x\in\mathbb{R}^{n}$ that satisfies the input specifications such
that the output $N(x)$ satisfies the output specifications.

b) The problem _verification of interval property_ $\operatorname{VIP}(F)$
consists of the same instances. The question is whether for all
$x\in\mathbb{R}^{n}$ satisfying the input specifications, $N(x)$ will satisfy
the output specifications.

c) The problem _network equivalence_ $\operatorname{NE}(F)$ is the question
whether two $F$-networks $N_{1}$ and $N_{2}$ compute the same function or not.

d) The size of a network is $T\cdot L$; here, $T$ denotes the number of
neurons in the net $N$ and $L$ is the maximal bit-size of any of the weights
and biases. The size of an instance of NNReach, VIP or NE is sum of the
network size and the usual bit-sizes of the LP-instances.

We omit $F$ in the notation if it is obvious from the context and write
VIP$(N,A,B)$ if VIP$(F)$ holds for the instance $(N,A,B)$. The notations for
the other problems are similar.

We additionally define certain robustness properties that were examined for
example in [18] and use them to assess the computed function in a more metric
way similar to [5].

###### Definition 3

Let $N$ be a NN, $N_{i}$ the projection of $N$ on the $i$-th output dimension,
$1\leq j\leq m$ an output dimension, $\bar{x}\in\mathbb{R}^{n}$,
$\varepsilon,\delta\in\mathbb{Q}_{\geq 0}\cup\\{\infty\\}$ and $d$ a metric on
${\mathbb{R}}^{n}$ as well as ${\mathbb{R}}^{m}$.

a) The classification of a network input $x$ is the output dimension $1\leq
i\leq m$ with the biggest value $N_{i}(x)$, which is interpreted as the
attribute that the input is most likely to have. We say that $N$ has
$\varepsilon$-_classification robustness_ in $\bar{x}$ with respect to $d$ iff
the classification of every input $x$ that is $\varepsilon$-close to $\bar{x}$
is the same as for $\bar{x}$, meaning

$\operatorname{CR}_{d}(N,\varepsilon,\bar{x},j):\Leftrightarrow\forall
x:d(x,\bar{x})\leq\varepsilon\Rightarrow\text{arg}\,\max\limits_{i}N_{i}(x)=j$

and _arbitrary_ $\varepsilon$-_classification robustness_ iff

$\operatorname{aCR}_{d}(N,\varepsilon,\bar{x}):\Leftrightarrow\exists
j\in\\{1,...,m\\}:\operatorname{CR}_{d}(N,\varepsilon,\bar{x},j)$

b) We say that $N$ has $\varepsilon$-$\delta$-_standard robustness_ in
$\bar{x}$ with respect to $d_{\lambda}$ iff $N$ interpreted as a function is
$\varepsilon$-$\delta$-continuous in $\bar{x}$, meaning

$\operatorname{SR}_{d}(N,\varepsilon,\delta,\bar{x}):\Leftrightarrow\forall
x:d(x,\bar{x})\leq\varepsilon\Rightarrow d(N(\bar{x}),N(x))\leq\delta$

c) We say that $N$ has $\varepsilon$-$L$-_Lipschitz robustness_ in $\bar{x}$
with respect to $d$ iff

$\operatorname{LR}_{d}(N,\varepsilon,L,\bar{x}):\Leftrightarrow\forall
x:d(x,\bar{x})\leq\varepsilon\Rightarrow d(N(\bar{x}),N(x))\leq L\cdot
d(\bar{x},x)$

d) For a specific set $F$ of activation functions, by abuse of notation we
denote by $\operatorname{CR}_{d}(F)$ the decision problem whether
$\operatorname{CR}_{d}(N,\varepsilon,\bar{x},j)$ holds where we allow as input
only networks $N$ that use functions from $F$ as activations, the notations
for the other problems are defined similarly.

We denote by $d_{p}$ the metric induced by the $p$-Norm, meaning
$d_{p}(x,y)=(\sum\limits_{i=1}^{n}(x_{i}-y_{i})^{p})^{\frac{1}{p}}$.

Note that $d_{1}$ and $d_{\infty}$ share the property that all
$\varepsilon$-balls $B_{\varepsilon,d}(x)$ are semi-linear sets and that they
can also be described as instances of LPF.

The property $\operatorname{aCR}$ seems redundant and unnatural at first, it
is however not equivalent to $\operatorname{CR}$ at an extent that one could
hastily assume. Note that it is in general already very hard to calculate the
solution of just one network computation $N(x)$ for given $N$ and $x$ for
certain activation functions, the result does not even have to be rational or
algebraic any more. It might even be impossible to determine the biggest
output dimension, i.e., to tell whether $N(x)_{i}\geq N(x)_{j}$, for in the
Turing model, one is not capable of precisely computing certain sigmoidal
functions, which is why seemingly obvious reductions from $\operatorname{CR}$
to $\operatorname{aCR}$ fail. Assume for example that an activation similar to
the exponential function is included, in this case the problem might become
hard for Tarskis exponential problem, which is not even known to be decidable.
Checking the properties $\operatorname{aCR}$ and $\operatorname{CR}$ is
therefore not necessarily of the same computational complexity. We also need
$\operatorname{aCR}$ in reduction proofs later on.

##  3 Complexity Results for Robustness

In network decision problems, $d_{1}$ and $d_{\infty}$ behave fundamentally
different than the other $p$-metrics, for they are the only ones that lead to
linear constraints. General polynomial systems tend have a higher
computational complexity than linear ones, compare for example
$\exists{\mathbb{R}}$ (NP-hard) with LP (in P) or Hilberts tenth problem
(undecidable) with integer linear systems (NP-complete). The following
proposition partially covers the linear part of our network decision problems.

###### Proposition 1

Let $F$ be a set of piecewise linear activation functions.

a)

The problems $\operatorname{VIP}(F)$ and $\operatorname{NE}(F)$ are in co-NP

b)

Let $d\in\\{d_{1},d_{\infty}\\}$. Then $\operatorname{SR}_{d}(F)$,
$\operatorname{CR}_{d}(F)$ and $\operatorname{LR}_{d}(F)$ are in co-NP.

This is specifically the case for $F=\\{ReLU\\}$.

###### Proof

Finding a witness for violation of the conditions works essentially the same
for all the above problems, we will perform it for $\operatorname{VIP}$.

The idea of the proof is that an instance is not satisfiable iff there exists
an $x\in\mathbb{R}^{n}$ fulfilling the input specifications so that $N(x)$
does not fulfill the output specifications, meaning at least one of the
equations does not hold. We then guess this equation along with some data that
narrows down how the computation on such an $x$ could behave.

For a no-instance, let $x$ be an input violating the specifications. The
certificate for the instance not to be solvable is not $x$ itself, because we
would need to guarantee that it has a short representation. Instead, the
certificate provides the information for every computation node, in which of
the linear intervals its input is (for ReLU-nodes for example whether it
returns zero or a positive value) when the network computes $N(x)$ together
with the index of the violated output specification. This leaves us with a
system like Linear Programming of linear inequalities that arise in the
following way:

All of the input specifications $\sum\limits_{i=1}^{n}a_{i}x_{i}\leq b$ and
the violated output specification $\sum\limits_{i=1}^{m}a_{i}N(x)_{i}>b$ are
already linear. For each $\sigma$-node computing

$y_{{\ell}i}=\sigma(\sum\limits_{j}c_{ji}^{({\ell}-1)}y_{({\ell}-1)j}+b_{{\ell}i}))$

that is by the certificate on an interval $[\alpha,\beta]$ where $\sigma(x)$
coincides with $a\cdot x+b$, we add the linear conditions

$\alpha\leq\sum\limits_{j}c_{ji}^{({\ell}-1)}y_{({\ell}-1)j}+b_{{\ell}i}\leq\beta$

and

$y_{{\ell}i}=a\cdot\sum\limits_{j}c_{ji}^{({\ell}-1)}y_{({\ell}-1)j}+b_{{\ell}i}+b$

The only difference to linear programming is that some of the equations are
strict and some are not. This decision problem is also well known to still be
in P by[12], Lemma 14.

The proof works in the same way for the other problems, as the falsehood of
their instances can also formulated as a linear programming instance. For
network equivalence for example, one would guess the output dimension that is
unequal at some point, encode the computation of both networks, and demand
that the outputs in the guessed dimensions are not the same, which is a linear
inequality.$\hfill\blacksquare$

The proof fails for non-linear metrics such as $d_{2}$, for the resulting
equation system is not linear any more.

###### Lemma 1

Let $F$ be a set of activations containing ReLU. For any
$\lambda\in[1,\infty]$, there are polynomial time reductions from
$d=d_{\infty}$ or $d=d_{1}$ to $d=d_{\lambda}$ for
$\operatorname{CR}_{d}(F),\operatorname{aCR}_{d}(F)$ and
$\operatorname{SR}_{d}(F)$.

###### Proof

We will show how to reduce from $d_{1}$ for a network $N$ by constructing a
network $N^{\prime}$ that shows the same behavior in
$\mathbb{B}_{\varepsilon,1}(\bar{x})$ as the given network and a sufficiently
similar behavior on $\mathbb{B}_{\varepsilon,\lambda}(\bar{x})$. The proof for
$d_{\infty}$ is analogous, as it only relies on the $\varepsilon$-ball to be a
convex semi-linear set.

The idea for all three problems is to first retract a superset of the
$\varepsilon$-ball to it so that $N^{\prime}=N\circ T$, where
$T(B_{\varepsilon,\lambda}(\bar{x}))=B_{\varepsilon,1}(\bar{x})$.

Let $(N,\varepsilon,\bar{x},j)$ be an instance of $\operatorname{CR}_{1}(F)$.
The equivalent instance $(N^{\prime},\varepsilon,\bar{x},j)$ of
$\operatorname{CR}_{\lambda}(F)$ is constructed as follows:

We first insert $n$ new layers before the initial input layer, the first of
them becomes the new input layer. These layers perform a transformation $T$
that has the following properties:

$\forall x\in\mathbb{B}_{\varepsilon,1}(\bar{x}):T(x)=x$. This ensures that if
the initial instance failed the property $\operatorname{CR}_{1}(F)$, the new
one fails $\operatorname{CR}_{\infty}(F)$.

$\forall
x\in\mathbb{B}_{\varepsilon,\lambda}(\bar{x}):T(x)\in\mathbb{B}_{\varepsilon,1}(\bar{x})$.
This ensures that if the initial instance fulfilled the property
$\operatorname{CR}_{1}(F)$, the new one fulfills
$\operatorname{CR}_{\infty}(F)$.

Such a function is for example

$\displaystyle T(x)_{i}=$ $\displaystyle
ReLU(x_{i})-ReLU(x_{i}+\sum\limits_{j=1}^{i-1}|T(x)_{j}|-\varepsilon)$
$\displaystyle-$
$\displaystyle(ReLU(-x_{i})+ReLU(-x_{i}+\sum\limits_{j=1}^{i-1}|T(x)_{j}|-\varepsilon))$

because
$\mathbb{B}_{\varepsilon,1}(\bar{x})\subseteq\mathbb{B}_{\varepsilon,\lambda}(\bar{x})$
and $T(x)\in\mathbb{B}_{\varepsilon,1}(\bar{x})\forall x\in\mathbb{R}^{n}$.

For $\operatorname{CR}$ the reduction is complete, for $\operatorname{aCR}$ it
is essentially the same. For $\operatorname{SR}_{\lambda}$ we perform as one
further step a transformation $P$ of $N(x)$ into a one-dimensional output,
namely $P(N(x))=\sum\limits_{i=1}^{m}|N(x)_{i}|$. It is easily seen that
$N(x)\in\mathbb{B}_{1}(\varepsilon)\Leftrightarrow
P(N(x))\in\mathbb{B}_{1}(\varepsilon)=[0,\varepsilon]$. $\hfill\blacksquare$

The previous Theorem as well as the following Proposition rely on the semi-
linearity of the final sets, a crucial property when using the Ellipsoid
Method or the ReLU function. When . This is the reason why we are restricted
to metrics where balls are semi-linear sets. When moving on to $d_{\lambda}$
for arbitrary $\lambda$, we cross the presumably large gap in computational
complexity between $NP$ and $\exists\mathbb{R}$.

###### Proposition 2

Let $\lambda\in\\{1,\infty\\}$. Then $\operatorname{VIP}(\\{id\\})$,
$\operatorname{NNReach}(id)$, $\operatorname{NE}(id)$,
$\operatorname{SR}_{\lambda}(\\{id\\})$,
$\operatorname{CR}_{\lambda}(\\{id\\})$,
$\operatorname{aCR}_{\lambda}(\\{id\\})$ and
$\operatorname{LR}_{\lambda}(\\{id\\})$ are in P.

###### Proof

${\sc NNReach}(id)$ is a special case of Linear Programming Feasibility. For
the other problems, we argue that their complements are in P=co-P. Note that
LPF is still in P if we allow strict linear inequalities. The complements of
${\sc VIP}(\\{id\\})$, ${\sc NE}(id)$,
$\operatorname{SR}_{\lambda}(\\{id\\})$,
$\operatorname{CR}_{\lambda}(\\{id\\})$,
$\operatorname{aCR}_{\lambda}(\\{id\\})$ and
$\operatorname{LR}_{\lambda}(\\{id\\})$ are global disjunctions of LP-
instances of linear size, so all of these Problems are in
P.$\hfill\blacksquare$

The following Lemma proved in [21] allows us to strengthen a couple of results
on complexities in the semi-linear range of network verification.

###### Lemma 2

An identity node can be expressed by two ReLU nodes without changing the
computed function.

The Lemma looks somewhat trivial, however for all our decision problems it
shows that adding $id$ to the set $F$ of allowed activations already
containing ReLU does not change the computational complexity. Furthermore,
when reducing one such problem to another one, we can assume $id$ to be among
the activations and freely use it in the reductions, as for example in the
next Lemma.

###### Lemma 3

Let $F$ be a set of activation functions.

i) $\operatorname{aCR}_{d}(F)$ is polynomial time reducible to
$\operatorname{CR}_{d}(F)$.

ii) If $d$ is induced by a $p$-norm and if $ReLU\in F$, then
$\operatorname{CR}_{d}(F)$ is polynomial time reducible to
$\operatorname{aCR}_{d}(F)$.

###### Proof

i) To see if $aCR_{d}(N,\varepsilon,\bar{x})$ holds, check
$\operatorname{CR}_{d}(N,\varepsilon,\bar{x},j)$ for all possible $j$ and see
if one of them holds.

ii) For the reverse direction, let $(N,\varepsilon,\bar{x},j)$ be an instance
of $\operatorname{CR}_{d}(F)$. We will construct an instance
$(N_{h},\varepsilon,\bar{x})$ of $aCR$ so that

$\operatorname{CR}_{d}(N,\varepsilon,\bar{x},j)\Leftrightarrow\operatorname{aCR}_{d}(N_{h},\varepsilon,\bar{x})$

The idea is to apply a function $f$ on the output that collects any possible
overlap of all dimensions other than $j$. This function is then modified to a
function $h$ with 3 output dimensions described by a network $N_{h}$, where
one dimension is the constant zero function, and it is guaranteed to be
negative in both remaining dimensions at some point. Also, iff $f$ was at some
point positive, which happens exactly if there was an overlap, so should at
least one component of $h$ be. Since $h$ is at some point negative in the
second and third dimension, the only candidate for the pointwise biggest
output dimension is the first, and this is the case iff there was an overlap
in the output of the initial network. This means that
$\operatorname{CR}_{d}(N,\varepsilon,\bar{x},j)\Leftrightarrow\operatorname{CR}_{d}(N_{h},\varepsilon,\bar{x},1)\Leftrightarrow\operatorname{aCR}_{d}(N_{h},\varepsilon,\bar{x})$.
It remains to show that such functions $f,h$ exist and that they can be
described by a network $N_{h}$.

Note that the following functions can be computed by neural networks that are
modifications of $N$:

$f(x)=\sum\limits_{i=1}^{m}ReLU(N(x)_{i}-N(x)_{j})$ $g(x)=f(x)-ReLU(f(x)-1)$

Note that $f(x)\geq 0$ and $f(x)=0$ iff $j$ is the index for a maximal
component. Furthermore if $f(x)\geq 1$, then $g(x)=1$ and if $f(x)\in[0,1]$
then $g(x)=f(x)$. Thus, $g\equiv 0$ iff
$\operatorname{CR}_{d}(N,\varepsilon,\bar{x},j)$. Now define $h$ as

$h(x)=(0,g(x)-\frac{2}{\delta}ReLU(x_{1}-\bar{x}_{1}),g(x)-\frac{2}{\delta}ReLU(\bar{x}_{1}-x_{1})).$

Where $\delta\in\mathbb{Q}$ is chosen so that $\delta<\varepsilon$, meaning
$\bar{x}+\delta e_{1},\bar{x}-\delta
e_{1}\in\mathbb{B}_{\varepsilon,d}(\bar{x})$ where $e_{1}=(1,0,...,0)$.

Let $N_{h}$ be the network computing $h$. When asked if
$aCR_{\lambda}(N_{h},\varepsilon,\bar{x})$, the second and third dimensions of
$h$ cannot be the pointwise biggest, the only possible candidate is 0 (j=1)
because $h_{2}(\bar{x}+\delta e_{1}),h_{3}(\bar{x}-\delta e_{1})\leq-1$. Also,
$g$ is constantly 0 iff $\operatorname{CR}_{\lambda}(N,\varepsilon,\bar{x},j)$
holds, on the other hand $g\equiv 0$ holds iff
$aCR_{\lambda}(N_{h},\varepsilon,\bar{x})$, so
$\operatorname{CR}_{\lambda}(N,\varepsilon,\bar{x},j)\Leftrightarrow
aCR_{\lambda}(N_{h},\varepsilon,\bar{x})$.$\hfill\blacksquare$

###### Theorem 3.1

Let $F$ be a set of activation functions. We have that

i) $\operatorname{SR}_{\infty}$($F$) is linear time reducible to ${\sc
VIP}(F)$,

ii) $\operatorname{CR}_{\infty}$($F$) is linear time reducible to ${\sc
VIP}(F)$,

iii) if $id\in F$, then $\operatorname{SR}_{\infty}$($F$) is linear time
reducible to $\operatorname{CR}_{\infty}(F$),

iv) if $ReLU\in F$, then $\operatorname{CR}_{d}(F$) is linear time reducible
to $\operatorname{SR}_{d}(F$) for any metric $d$.

###### Proof

i) Let $(N,\varepsilon,\delta,\bar{x})$ be an instance of SR∞($F$). To
construct an equivalent instance of ${\sc VIP}(F)$, we introduce two copies of
the network $N$ and view them as one big network $N^{\prime}$ with an input
dimension twice the input dimension of $N$. We demand by input specification
that the input of the first copy of $N$ is $\bar{x}$ and the input of the
second copy is in the $\varepsilon$-ball of $\bar{x}$ with respect to
$\|\cdot\|_{\infty}$, which is equivalent to $\forall
i\in\\{1,...,n\\}:-\varepsilon\leq\bar{x}_{i}-x_{i}\leq\varepsilon$, a linear
equation system that we denote $A$. Similarly, we demand by output
specification that $N(x)$ is in the $\delta$-ball of $N(\bar{x})$, which is
equivalent to $\forall i\in\\{1,...,m\\}:-\delta\leq
N(\bar{x})_{i}-N(x)_{i}\leq\delta$, we denote this system $B$. This gives us
the ${\sc VIP}(F)$-instance $(N^{\prime},A,B)$ for which we have ${\sc
VIP}(N^{\prime},A,B)\Leftrightarrow\operatorname{SR}(N,\varepsilon,\delta,\bar{x})$.

ii) Let $(N,\varepsilon,\bar{x},j)$ be an instance of
$\operatorname{CR}_{\infty}(F)$. We construct an equivalent instance of ${\sc
VIP}(F)$ as follows. The network remains $N$, the input specifications are
$\forall i\in\\{1,...,n\\}:\bar{x}_{i}-\varepsilon\leq
x_{i}\leq\bar{x}_{i}+\varepsilon$ and the output specification is
$\bigwedge\limits_{i=1}^{m}N(x)_{i}\leq N(x)_{j}$.

iii) Let $(N,\varepsilon,\delta,\bar{x})$ be an instance of
$\operatorname{SR}_{\infty}$($F$) with $m$ the output dimension of $N$. To
construct an equivalent instance $(N^{\prime},\varepsilon,\bar{x},2m+1)$ of
$\operatorname{CR}_{\infty}(F)$, we perform the computation of two copies of
the network $N$ in parrallel, which constitutes a new network $N^{\prime}$ as
follows:

Figure 1: Idea iii)

The first copy is shifted by one layer, so the layer that was the input layer
is now in the first hidden layer with no incoming connections and the bias of
node $i$ is $\bar{x}_{i}$, so that first copy just computes the value
$N(\bar{x})$. The input layer of $N^{\prime}$ is the input layer of the second
copy, so the second copy of $N$ computes $N(x)$. We add a layer of id-nodes at
the end of it that does not change the output but let it have the same number
of layers as the first copy. We add one layer connecting both copies after the
old output layer, this one becomes the new output layer, and it computes

$(N(x)_{1}-N(\bar{x})_{1},...,N(x)_{m}-N(\bar{x})_{m},N(\bar{x})_{1}-N(x)_{1},...,N(\bar{x})_{m}-N(x)_{m},\delta).$

The node corresponding to the last value $N^{\prime}(x)_{2m+1}=\delta$ has no
incoming connections and bias $\delta$. We have that $\forall
i\in\\{1,...,m\\}:|N(\bar{x})_{i}-N(x)_{i}|\leq\delta$ iff $\forall
i\in\\{1,...,m\\}:N(\bar{x})_{i}-N(x)_{i}\leq\delta\land
N(x)_{i}-N(\bar{x})_{i}\leq\delta$, so the two instances are in fact
equivalent.

iv) Let $(N,\varepsilon,\bar{x},j)$ be an instance of
$\operatorname{CR}_{d}(F)$. We construct an equivalent instance
$(N^{\prime},\varepsilon,0,\bar{x})$ of $\operatorname{SR}_{d}(F)$ as follows:
We add two additional layers after the old output layer. The first one
computes $\alpha_{i}=ReLU(N(x)_{i}-N(x)_{j})$ for all $i$, these values are
all 0 everywhere on $B_{d,\varepsilon}(\bar{x})$ iff
$\operatorname{CR}_{d}(N,\varepsilon,\bar{x},j)$ holds. The next added layer
computes $\beta=ReLU(\sum\limits_{i=1}^{m}\alpha_{i})$, this value is 0
everywhere on $B_{d,\varepsilon}(\bar{x})$ iff
$\operatorname{CR}_{d}(N,\varepsilon,\bar{x},j)$ holds. Now we have that
$\operatorname{CR}_{d}(N,\varepsilon,\bar{x},j)\Leftrightarrow\operatorname{SR}_{d}(N^{\prime},\varepsilon,0,\bar{x})\land
N^{\prime}(\bar{x})=0$, so it remains to encode that last condition as a
$\operatorname{SR}_{d}(F)$-instance. The function

$f(x):=\sum\limits_{i=1}^{n}ReLU(x_{i}-\bar{x}_{i})+ReLU(\bar{x}_{i}-x_{i})$

is 0 in $\bar{x}$ and strictly positive everywhere else and there exists an
$F$-network $N_{f}$ computing $f$. The networks $N^{\prime}$ and $N_{f}$ can
be combined to an $F$-network $N^{\prime\prime}$ computing
$g(x)=ReLU(N^{\prime}-N_{f})(x)$. If
$\operatorname{SR}_{d}(N^{\prime},\varepsilon,0,\bar{x})$ holds, then

$N^{\prime}(\bar{x})=0\Leftrightarrow g(x)=0\forall x\in
B_{\varepsilon}(\bar{x})\Leftrightarrow\operatorname{SR}_{d}(N^{\prime\prime},\varepsilon,0,\bar{x}).$

The conditions $\operatorname{SR}_{d}(N^{\prime},\varepsilon,0,\bar{x})$ and
$\operatorname{SR}_{d}(N^{\prime\prime},\varepsilon,0,\bar{x})$ can be
formalized as a single $\operatorname{SR}_{d}$ instance by merging both nets
$N^{\prime}$ and $N^{\prime\prime}$ into a single larger one, so the reduction
is in fact many-one.$\hfill\blacksquare$

###### Proposition 3

Let $F$ be a set of activation functions. If $id\in F$, then ${\sc NE}(F)$ is
linear time reducible to $\operatorname{CR}_{d}(F)$ for any metric $d$.

###### Proof

Let $(N,N^{\prime})$ be an instance of ${\sc NE}(F)$. We merge both networks
$N$ and $N^{\prime}$ into one network $N^{\prime\prime}$ by
identifying/contracting their corresponding inputs and subtracting their
corresponding outputs both ways to obtain the output layer

$(N(x)_{1}-N^{\prime}(x)_{1},...,N(x)_{m}-N^{\prime}(x)_{m},N^{\prime}(x)_{1}-N(x)_{1},...,N^{\prime}(x)_{m}-N(x)_{m},0).$

The last output node is always 0, this can be forced by introducing an id-node
that has bias 0 and no incoming connections. Now

${\sc
NE}(N,N^{\prime})\Leftrightarrow\operatorname{CR}_{d}(N^{\prime\prime},\infty,0,2m+1),$

which concludes the proof. $\hfill\blacksquare$

Note that for Lipschitz robustness and standard robustness also global
variants make sense:

###### Definition 4

Let $N$ be a NN, $\bar{x}\in\mathbb{R}^{n}$ and
$\varepsilon,\delta\in\mathbb{Q}_{\geq 0}$. We say that $N$ has (global)
$\varepsilon$-$\delta$-_standard robustness_ wrt the metric $d$ iff it has
$\varepsilon$-$\delta$-standard robustness in every
$\bar{x}\in\mathbb{R}^{n}$:

$\operatorname{glob-SR}_{d}(N,\varepsilon,\delta):=\forall
x,\bar{x}:d(x-\bar{x}|)\leq\varepsilon\Rightarrow
d(N(\bar{x})-N(x))\leq\delta.$

We define $\operatorname{glob-LR}_{d}$ analogously, note that it coincides
with $L$-Lipschitz continuity independent of $\varepsilon$.

This equivalence does not hold for local Lipschitz robustness: The function
$x\cdot\chi_{\mathbb{Q}}(x)$ is $\varepsilon$-$1$-Lipschitz robust in 0 for
every $\varepsilon$, but not Lipschitz-continuous in any $\varepsilon$-ball
around 0.

###### Remark 1

Global arbitrary $\varepsilon$-_classification robustness_
$\operatorname{glob-aCR}_{d}$ for a network $N$, meaning it has arbitrary
$\varepsilon$-classification robustness in every input $x\in{\mathbb{R}}^{n}$,
hardly ever happens at all. We have that only very artificial functions map
inputs to different classes and still have global (arbitrary) classification
robustness, for between two areas of different classification, there must be a
dividing strip of diameter $\varepsilon$ in which both classifications must be
choosable. The function $f:\mathbb{R}\rightarrow\mathbb{R}^{2}$ where

$f=\begin{pmatrix}f_{1}\\\ f_{2}\end{pmatrix}\text{ where
}f_{1}(x)=\left\\{\begin{array}[]{ll}0,&\text{for }x\leq-1\\\ x+1,&\text{for
}-1\leq x\leq-\frac{1}{2}\\\ \frac{1}{2},&\text{for }-\frac{1}{2}\leq
x\leq\frac{1}{2}\\\ x-1,&\text{for }\frac{1}{2}\leq x\leq 1\\\ 1,&\text{for
}1\leq x\end{array}\right.,\ \ \ \ \ f_{2}(x)=1-f_{1}(x)$

for example is globally 1-classification robust. Such functions however are
unlikely for a network of "natural origin" for these areas of equal
classification do not occur in usual training methods.

###### Theorem 3.2

Let $F$ be a set of activation functions containing $ReLU$. Then:

i) $\operatorname{glob-SR}_{\infty}(F)$ reduces to ${\sc NE}(F)$.

ii) $\operatorname{glob-SR}_{\infty}(F)$, $\operatorname{LR}_{\infty}(F)$ and
$\operatorname{glob-LR}_{\infty}(F)$ are co-NP-hard.

###### Proof

$i)$ We reduce an instance $(N,\varepsilon,\delta)$ of $\operatorname{glob-
SR}_{\infty}(F)$ to an instance $(N^{\prime},N^{\prime\prime})$ of ${\sc
NE}(F)$ by using the ReLU-function to check whether certain values are
positive or not and by forcing the differences
$\|\bar{x}_{i}-x_{i}\|_{\infty}$ to be smaller than $\varepsilon$, again with
the use of ReLU-nodes. We construct the network $N^{\prime}$ as follows: The
input $(x,y)=(x_{1},...,x_{n},y_{1},...,y_{n})$ has twice the dimension of the
input of $N$. On the first half $(x_{1},...,x_{n})$ we execute $N$ to obtain
$N(x)$. For each of the $y_{i}$ in the second half, we compute

$f(y_{i})=\varepsilon\cdot(ReLU(y_{i})-ReLU(y_{i}-1)-\frac{1}{2})$

by ReLU-nodes in the first hidden layer, a bias of $-\frac{1}{2}$ in the
second and a weight of $\varepsilon$ in the third. Note that
$im(f)=[-\varepsilon,\varepsilon]$, we interpret $f(y_{i})$ as
$\bar{x}_{i}-x_{i}$. We now execute $N$ again, this time on
$(x_{1}+f(y_{1}),...,x_{n}+f(y_{n}))$ to obtain $N(x+\bar{x}-x)=N(\bar{x})$.
We compute both $N(x)-N(\bar{x})$ and $N(\bar{x})-N(x)$ by ReLU-nodes with
bias $-\delta$ to obtain

$N^{\prime}(x,y)=(ReLU(N(\bar{x})_{1}-N(x)_{1}-\delta),ReLU(N(x)_{1}-N(\bar{x})_{1}-\delta),...,$
$ReLU(N(\bar{x})_{m}-N(x)_{m}-\delta),ReLU(N(x)_{m}-N(\bar{x})_{m}-\delta)).$

$\operatorname{SR}^{G}_{\infty}(N,\varepsilon,\delta)$ holds iff $N^{\prime}$
is constantly 0. The second network $N^{\prime\prime}$ consists of $2n$ input
nodes, no hidden layer and $2m$ output nodes with all weights and biases 0.
This network will compute 0 independently of the input, so

$\operatorname{SR}^{G}_{\infty}(N,\varepsilon,\delta)\Leftrightarrow{\sc
NE}(N^{\prime},N^{\prime\prime}).$

$ii)$ We reduce an instance $\varphi$ of 3-SAT with $n$ clauses to an instance
$(N,\infty,n-\frac{1}{2})$ of the complement of $\operatorname{glob-
SR}_{\infty}(\\{ReLU\\})$. The idea is to associate pairs of literals and
their negations with pairs of nodes with the property that at least one of
these nodes must have the value zero. We then interpret the zero-valued node
as false and the other one, that may have any value in $[0,1]$, as true and
replace $\land$ and $\lor$ by gadgets that work with the function
$\Psi:\mathbb{R}\rightarrow[0,1]$ defined as $x\mapsto ReLU(x)-ReLU(x-1)$.
Note that it is easily constructable in a ReLU-network and
$\Psi|_{[0,1]}=id|_{[0,1]}$.

For the reduction, introduce for each variable $a$ in$\varphi$ an input
variable $\alpha_{1}$ and use the first two hidden layers to compute
$\alpha_{2}:=\Psi(\alpha_{1})$. Use the third hidden layer to propagate
$\alpha_{2}$ as well as to compute $\lnot\alpha_{2}:=1-\alpha_{2}$. In the
fourth hidden layer compute $\alpha:=2\cdot ReLU(\alpha_{2}-\frac{1}{2})$ for
every atom as well as for the negations. Note that $\alpha=0$ or
$\lnot\alpha=0$ and the other one can be anything in $[0,1]$. In the fifth and
sixth hidden layer compute for every clause $(a,b,c)$ the value
$\Psi(\alpha+\beta+\gamma)$. In the seventh layer, add all nodes from the
sixth layer, this is the overall output of the network. If the instance of
3-SAT is solvable, then $N(x)=n$ is reachable via setting the true atoms to 1
and the false ones to 0. The value $N(y)=0$ is always reachable, just assign
every variable the value $\frac{1}{2}$. This means that if the 3-SAT instance
is solvable, then $x$ and $y$ are witnesses that $\operatorname{glob-
SR}_{\infty}(N,\infty,n-\frac{1}{2})$ is false. On the other hand, if the
3-SAT instance is not solvable, then for every input
$\Psi(\alpha+\beta+\gamma)=0$ for at least one of the clauses, so $N(x)\leq
n-1$. Now we always have that $N(y)\geq 0$ because $\Psi\geq 0$, so
$|N(x)-N(y)|\leq n-1$ and $\operatorname{glob-
SR}_{\infty}(N,\infty,n-\frac{1}{2})$ is true.

We reduce 3-SAT to $\operatorname{LR}_{\infty}(F)$ and $\operatorname{glob-
LR}_{\infty}(F)$ in the same way, the instance for
$\operatorname{LR}_{\infty}(F)$ is
$(N,\frac{1}{2},2n-1,(\frac{1}{2},...,\frac{1}{2}))$ with the same network $N$
as constructed above for $\operatorname{glob-SR}_{\infty}(\\{ReLU\\})$. We
chose $n-1<\frac{1}{L}\cdot\varepsilon<n$ so that
$\operatorname{LR}_{\infty}(N,\frac{1}{2},2n-1,(\frac{1}{2},...,\frac{1}{2}))$
is equivalent to $\operatorname{glob-SR}_{\infty}(N,\infty,n-\frac{1}{2})$.
This is true because the minimum of $N(x)$ is $0$ attained in
$(\frac{1}{2},...,\frac{1}{2})$ and the maximum is either $n$ if the 3-SAT
instance is satisfiable or at most $n-1$ if it is not, taken on the boundary
of the unit hypercube. The growth between the minimum and the maximum is
linear because the intersection points where ReLU is not differentiable are in
$(\frac{1}{2},...,\frac{1}{2})$ and on the boundary of the unit hypercube, but
never in between.

The instance $(N,\frac{1}{2},2n-1)$ constructed by the reduction to
$\operatorname{glob-LR}_{\infty}(F)$ is the same, because no other pair of
points $x,\bar{x}$ will lead to a steeper descent if the network was derived
from a SAT-instance that is not satisfiable. This is because the steepest
descent must necessarily point to the minimum if the function is linear along
the connecting line and no other local minimum exists. $\hfill\blacksquare$

###### Corollary 1

$\operatorname{glob-SR}_{\infty}(\\{ReLU\\})$, ${\sc NE}(\\{ReLU\\})$,
$\operatorname{CR}_{\infty}(\\{ReLU\\})$,
$\operatorname{SR}_{\infty}(\\{ReLU\\})$,
$\operatorname{LR}_{\infty}(\\{ReLU\\})$ and ${\sc VIP}(\\{ReLU\\})$ are co-
NP-complete.

###### Proof

${\sc VIP}(\\{ReLU\\})$ is in co-NP by Theorem 1 and $\operatorname{glob-
SR}_{\infty}(\\{ReLU\\})$ is co-NP hard by Theorem 3.2, $ii)$. The chain of
reductions in between is provided by Theorem 3.2 $i)$, Theorem 3, and Theorem
3.1 $iv),i)$. $\hfill\blacksquare$

##  4 Network Minimization

In this section, we want to analyze different criteria on whether a network is
unnecessarily huge. The evaluation of a function given as a network becomes
easier and faster for small networks, it is therefore desirable to look for a
tradeoff between accuracy and runtime performance. In the worst case, a long
computation in an enormously big network that was assumed to be more accurate
due to its size, could lead to rounding errors in both the training and the
evaluation, making the overall accuracy worse than in a small network.

###### Definition 5

Let $F$ be a set of activations, $N$ an $F$-network and $K$ the set of nodes
of $N$.

a) $N$ is called minimal, if no other $F$-network with less many nodes than
$N$ computes the same function. The decision problem $\operatorname{MIN}(F)$
asks whether a given $F$-network $N$ is minimal, in that case we write
$\operatorname{MIN}(N)$.

b) Let $Y\subseteq K$ be a subset of the nodes, $G_{N}$ the underlying graph
of $G$ and $G_{N}^{\prime}$ its subgraph induced by $K\backslash Y$. The
network $N^{\prime}$ whose underlying is $G_{N}^{\prime}$ and where all
activations, biases and weights are the same as in the corresponding places in
$N$, is said to be obtained from $N$ by deleting the nodes in Y. By abuse of
notation we denote it by $N\backslash K:=N^{\prime}$.

c) A subset $Y\subseteq K$ of hidden nodes of a network $N$ is called
unnecessary, if the network $N\backslash Y$ produced by deleting these nodes
still computes the same function and otherwise necessary. The problem to
decide whether sets of nodes are necessary is NECE$(F)$, we write NECE$(N,Y)$
if $Y$ is necessary.

d) If NECE$(N,Y)$ for all non-empty subsets $Y\subseteq K$ of nodes, we write
ANECE$(N)$, this also defines a decision problem in the obvious way.

It obviously holds that
$\operatorname{MIN}(N)\Rightarrow\operatorname{ANECE}(N)$, the reverse
direction however does not hold in general:

###### Example 1

A network can contain only necessary nodes and still not be minimal. Consider
for example the $\\{id,ReLU\\}$-network $N$ that consists of an input node
$x$, two hidden nodes $y_{1,1}=ReLU(x)$ and $y_{1,2}=ReLU(-x)$ and one output
node with weights 1 and -1 and bias 0, so it computes
$y_{2}=id(y_{1,1}-y_{1,2})=x$. The network represents the identity map and is
not minimal, because the smallest $\\{id,ReLU\\}$-network $M$ computing the
identity consists of an input node, no hidden nodes and one output node with
activation $id$, weight 1 and bias 0. However every non-empty subset of hidden
nodes in $N$ is necessary; if we delete $y_{1,1}$, the remaining network
computes the negative part $x^{-}=min\\{0,x\\}$ of the input, if we delete
$y_{1,2}$ it computes the positive part and if we delete both it computes the
zero-function for the last node has no more incoming nodes at all and thus
returns the empty sum. We call this network $Q$. 111This also illustrates that
the smallest network $M$ that is equivalent to $N$ is in general not
isomorphic to a substructure of $N$.

Also consider the net $K$ computing the zero-function in the following way: In
the first hidden layer, compute $y_{1,1}=y_{1,2}=ReLU(x)$, the output-node is
connected to both with weights 1 and -1, respectively, and bias 0, so it
computes $0=ReLU(x)-ReLU(x)$. In $K$, both hidden nodes on their own are
necessary, the subset containing both however is not, because when deleting
those two, we remain with the network $Q$ that also computes the zero-
function.

###### Theorem 4.1

Let $id\in F$, then the complement of NECE$(F)$ and NE$(F)$ are linear-time
equivalent.

###### Proof

The first reduction is trivial,

$\operatorname{NECE}(N,\\{y_{1},...,y_{k}\\})\Leftrightarrow\lnot\operatorname{NE}(N,N\backslash\\{y_{1},...,y_{k}\\})$

For the other direction, let $M,N$ be two $F$-networks. We construct an
instance of NECE$(F)$ that is equivalent to $\lnot\operatorname{NE}(N,M)$ as
follows:

First, we merge $N$ and $M$ into a network $P$ that computes $N(x)$ and
$M(x)$, then computes $y=N(x)-M(x)$ in the last hidden layer and then
propagates the value $P(x)=id(y)$ to the output layer. Now if $y$ is deleted,
$P\backslash\\{y\\}\equiv 0$, because then the output node would have no
incoming edges at all, so it would compute the identity over the empty sum,
which is 0. It follows that $y$ is unnecessary iff $P\equiv 0$, which in turn
is the case iff $N\equiv M$ meaning NE$(N,M)$, so we have that
$\lnot\operatorname{NE}(N,M)\Leftrightarrow\operatorname{NECE}(P,\\{y\\})$.
$\hfill\blacksquare$

###### Theorem 4.2

Let $F$ only contain semi-linear functions. Then

i)

MIN$(F)$ is in $\Pi_{2}^{P}$.

ii)

ANECE$(F)$ is in $\Pi_{2}^{P}$.

###### Proof

i)

We argue that co-MIN is in $\Sigma_{2}^{P}$. The algorithm non-
deterministically guesses a smaller representation $M$ of the function/network
$N$ and then proves that NE$(N,M)$, which is co-NP-complete, see [21].

ii)

In the same way, observe that co-ANECE$(F)$ can be solved by non-
deterministically guessing an unnecessary subset $Y$ and then showing that the
network remaining after deleting $Y$ is equivalent to the original
net.$\hfill\blacksquare$

###### Theorem 4.3

If id is among the activations, NE reduces to ANECE in polynomial time.

###### Proof

Let $(N,M)$ be an instance of NE. First, merge both $N$ and $M$ into one
network by subtracting their corresponding output nodes. Then delete all nodes
that are constantly zero. These are detected layer-wise starting with the
nodes right after the input layer. For each node $n$, delete all nodes that do
not affect it in the sense that they are in subsequent layers, in the same
layer, or in a previous layer but with no connection or connection with
weights 0 towards $n$. Then allocate one additional id-node in the following
layer and connect it to $n$ with weight 1 and no bias.$\hfill\blacksquare$

##  5 Conclusion

We examined the computational complexity of various verification problems such
as robustness and minimality for neural networks in dependence of the
activation function used. We explained the connection between the distance
function in use and the complexity of the resulting problem. We provided a
framework for minimizing networks and examined the complexities of those
questions as well.

Further open questions are:

1.)

Is $\operatorname{LR}_{1}(ReLU)$ complete for co-NP? Are
$\operatorname{LR}_{1}(F)$ and $\operatorname{LR}_{\infty}(F)$ in general
reducible on each other?

2.)

Do sets described by functions computed by networks using only $ReLU$ (or only
semi-linear activations) have more structure than just any semi-linear set?
Can this structure be exploited to calculate or approximate the measure of
such a set quicker than with the known algorithms?

3.)

Are ANECE and MIN$(F)$ $\Pi_{2}^{P}$-complete if $F$ only contains semi-linear
functions?

4.)

Several results rely on the identity activation. Can this be omitted? Or is
there a problem that becomes substantially easier when the identity map is
dropped?

Acknowledgment: I want to thank Klaus Meer for helpful discussion and the
anonymous referees for various hints improving the writing.

## References

  * [1] Aws Albarghouthi.  Introduction to Neural Network Verification.  2021\.
  * [2] Anish Athalye, Nicholas Carlini, and David Wagner.  Obfuscated gradients give a false sense of security: Circumventing defenses to adversarial examples, 2018.
  * [3] Ovidiu Calin.  Deep Learning Architectures - A Mathematical Approach.  Springer, 2020.
  * [4] Nicholas Carlini, Chang Liu, Úlfar Erlingsson, Jernej Kos, and Dawn Song.  The secret sharer: Evaluating and testing unintended memorization in neural networks, 2019.
  * [5] Marco Casadio, Ekaterina Komendantskaya, Matthew L. Daggitt, Wen Kokke, Guy Katz, Guy Amir, and Idan Refaeli.  Neural Network Robustness as a Verification Property: A Principled Case Study.  2021\.
  * [6] Matthew Dixon, Diego Klabjan, and Jin Hoonc Bang.  Classification-based financial markets prediction using deep neural networks.  Algorithmic Finance, 6:67–77, 2017.
  * [7] Tommaso Dreossi, Shromona Ghosh, Alberto Sangiovanni-Vincentelli, and Sanjit A. Seshia.  A formalization of robustness for deep neural networks, 2019.
  * [8] Sorin Grigorescu, Bogdan Trasnea, Tiberiu Cocias, and Gigel Macesanu.  A survey of deep learning techniques for autonomous driving.  Journal of Field Robotics, 37:362–386, 2019.
  * [9] Xingwu Guo, Ziwei Zhou, Yueling Zhang, Guy Katz, and Min Zhang.  Occrob: Efficient smt-based occlusion robustness verification of deep neural networks, 2023.
  * [10] Geoffrey Hinton, Li Deng, Dong Yu, George E. Dahl, Abdel-rahman Mohamed, Navdeep Jaitly, Andrew Senior, Vincent Vanhoucke, Patrick Nguyen, Tara N. Sainath, and Brian Kingsbury.  Deep neural networks for acoustic modeling in speech recognition: the shared views of four research groups.  IEEE Signal Process, 29:82–97, 2012.
  * [11] Xiaowei Huang, Daniel Kroening, Wenjie Ruan, James Sharp, Youcheng Sun, Emese Thamo, Min Wu, and Xinping Yi.  A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability.  Computer Science Review, 37, 2020.
  * [12] Peter Jonsson and Christer Bäckström.  A unifying approach to temporal constraint reasoning.  Artificial Intelligence, 102(1):143–155, 1998.
  * [13] Guy Katz, Clark Barrett, David Dill, Kyle Julian, and Mykel Kochenderfer.  Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks.  Computer Aided Verification, 10426:97–117, 2017.
  * [14] Asifullah Khan, Anabia Sohail, Umme Zahoora, and Aqsa Saeed Qureshi.  A survey of the recent architectures of deep convolutional neural networks.  Artificial Intelligence Review, 53:5455–5516, 2020.
  * [15] Alex Krizhevsky, Ilya Sutskever, and Geoffrey E. Hinton.  ImageNet Classification with Deep Convolutional Neural Networks.  Association for Computing Machinery, 2017.
  * [16] Geert Litjens, Thijs Kooi, Babak Ehteshami Bejnordi, Arnaud Arindra Adiyoso Setio, Francesco Ciompi, Mohsen Ghafoorian, Jeroen A.W.M. van der Laak, Bram van Ginneken, and Clara I. Sánchez.  A survey on deep learning in medical image analysis.  Medical Image Analysis, 42:60–88, 2017.
  * [17] Saeed Mahloujifar and Mohammad Mahmoody.  Can adversarially robust learning leverage computational hardness?, 2018\.
  * [18] Wenjie Ruan, Xiaowei Huanga, and Marta Kwiatkowska.  Reachability Analysis of Deep Neural Networks with Provable Guarantees.  Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI, pages 2651–2659, 2018.
  * [19] Marco Sälzer and Martin Lange.  Reachability is NP-Complete Even for the Simplest Neural Networks.  International Conference on Reachability Problems, 13035:149–164, 2021.
  * [20] Jonathan Uesato, Brendan O’Donoghue, Aaron van den Oord, and Pushmeet Kohli.  Adversarial risk and the dangers of evaluating against weak attacks, 2018\.
  * [21] Adrian Wurm.  Complexity of Reachability Problems in Neural Networks.  International Conference on Reachability Problems, 2023.