11institutetext: School of Electr. Eng. and Computer Science, University of
Kassel, Germany
https://www.uni-kassel.de/eecs/fmv
11email<EMAIL_ADDRESS>
# Reachability Is NP-Complete Even for the Simplest Neural Networks

Marco Sälzer  0000-0002-8012-5465 Martin Lange  0000-0002-1621-0972

###### Abstract

We investigate the complexity of the reachability problem for (deep) neural
networks: does it compute valid output given some valid input? It was recently
claimed that the problem is NP-complete for general neural networks and
conjunctive input/output specifications. We repair some flaws in the original
upper and lower bound proofs. We then show that NP-hardness already holds for
restricted classes of simple specifications and neural networks with just one
layer, as well as neural networks with minimal requirements on the occurring
parameters.

###### Keywords:

machine learning computational complexity formal specification and
verification

##  1 Introduction

Deep learning has proved to be very successful for highly challenging or even
otherwise intractable tasks in a broad range of applications such as image
recognition [11] or natural language processing [5] but also safety-critical
applications like autonomous driving [4], medical applications [12], or
financial matters [2]. These naturally come with safety concerns and the need
for certification methods. Recent such methods can be divided into (i)
Adversarial Attack and Defense, (ii) Testing, and (iii) Formal Verification. A
comprehensive survery about all three categories is given in [6].

The former two cannot guarantee the absence of errors. Formal verification of
neural networks (NN) is a relatively new area of research which ensures
completeness of the certification procedure. Recent work on sound and complete
verification algorithms for NN are mostly concerned with efficient solutions
to their reachability problem NNReach [8, 3, 13, 1]: given an NN and symbolic
specifications of valid inputs and outputs, decide whether there is some valid
input such that the corresponding output is valid, too. This corresponds to
the understanding of reachability in classical software verification: valid
sets of inputs and outputs are specified and the question is whether there is
a valid input that leads to a valid output. Put differently, the question is
whether the set of valid outputs is reachable from the set of valid inputs.
The difference to classical reachability problems in discrete state-based
programs is that there reachability is a matter of _lengths_ of a connection.
In NN this is given by the number of layers, and it is rather the _width_ of
the continuous state space which may cause unreachability.

Solving NNReach is interesting for practical purposes. An efficient algorithm
can be used to ensure that no input from some specified set of inputs is
misclassified or that some undesired class of outputs is never reached. In
applications like autonomous-driving, where classifiers based on neural
networks are used to make critical decisions, such safeguards are
indispensable.

However, all known algorithms for NNReach show the same drawback: a lack of
scalability to networks of large size which, unfortunately, are featured
typically in real-world applications [10]. This is not a big surprise as the
problem is NP-complete. This result was proposed by Katz et al. [8] for NN
with ReLU and identity activations, and later also by Ruan et al. [14]. While
there is no reason to doubt the NP-completeness claim, the proofs are not
stringent and contain flaws.

The argument for the upper bound in [8] misses the fact that real inputs are
not necessarily polynomially bounded in size. In fact, guessing values in
$\mathbb{R}$ is not even effective without a bound on the size of their
representation. Such a bound is closely linked to the question whether such
values can be approximated upto some precision. The proof by Katz et al. makes
no argument for any bound on the representation of such values, let alone a
polynomial one. 111While this paper was being processed, Katz et al. published
an extended version of their original paper [9]. Unfortunately, the flaws
concerning the upper bound are still present in this version.

The arguments for the lower bound by a reduction from 3sat in [8] and [15]
rely on a discretisation of real values to model Boolean values. This does not
work for the signum function $\sigma$ used by Ruan et al. as it is not
congruent for sums: e.g. $\sigma(-3)=\sigma(-1)$ but
$\sigma(2+(-3))\neq\sigma(2+(-1))$, showing that one cannot simply interpret
any negative number as the Boolean value _false_ etc. As a consequence,
completeness of the construction fails as there are (real) solutions to
NNReach which do not correspond to (discrete) satisfying 3sat assignments.
Katz et al. seem to be aware of this and use a slightly more elaborate
discretisation in their reduction, but unfortunately it still suffers from
similar problems. 222These problems are repaired in [9], but in a slightly
different way than we do.

We start our investigations into the complexity of NNReach by fixing these
issues in Sec. 3. We provide a different argument for membership in NP which
shows that the need for nondeterminism is not to be sought in the input values
but in the use of ReLU nodes. As a corollary we obtain polynomial decidability
for NN with a bounded number of such nodes. We also address the issue of
discretisation of real values in the lower bound proof, fixing the
construction given by Katz et al. We do not address the one by Ruan et al.
further, as this does not provide any further insights or new results.

We then observe that the reduction from 3sat constructs a very specific class
of NNReach instances which we call $\mathcal{C}(\textsc{3sat})$. NN from this
class have a fixed amount of layers but scaling input and output dimension as
well as layer size. This raises the question whether, in comparison to the
networks from $\mathcal{C}(\textsc{3sat})$, reducing the amount of layers or
fixing dimensionality leads to a class of networks for which NNReach is
efficiently solvable. In Sec. 4 we show that the answer to this is mostly
negative: NP-hardness of NNReach holds for NN with just one layer and an
output dimension of one. While this provides minimal requirements on the
structure of NN for NNReach to be NP-hard, we also give minimal criteria on
the weights and biases in NN for NP-hardness to hold. Thus, the computational
difficulty of NNReach in the sense of NP-completeness is quite robust. The
requirements on the structure or parameters of an NN that are needed for NP-
hardness to occur are easily met in practical applications. Due to space
restrictions, some technical proof details are deferred to the appendix.

We conclude in Sec. 5 with references to possible future work.

##  2 Preliminaries

###### Definition 1

A _neural network_ (NN) $N$ is a layered graph that represents a function of
type $\bbbr^{n}\rightarrow\bbbr^{m}$.

The first layer $l=0$ is called the input layer and consists of $n$ nodes. The
$i$-th node computes the output $y_{0i}=x_{i}$ where $x_{i}$ is the $i$-th
input to the overall network. Thus, the output of the input layer
$(y_{00},\dotsc,y_{0(n-1)})$ is identical to the input of $N$.

A layer $1\leq l\leq L-2$ is called _hidden_ and consists of $k$ nodes. Note
that $k$ must not be uniform across the hidden layers of $N$. Then, the $i$-th
node of layer $l$ computes the output
$y_{li}=\sigma_{li}(\sum_{j}c^{(l-1)}_{ji}y_{(l-1)j}+b_{li})$ where $j$
iterates over the output dimensions of the previous layer, $c^{(l-1)}_{ji}$
are real constants which are called _weights_ , $b_{li}$ is a real constant
which is called _bias_ and $\sigma_{li}$ is some (typically non-linear)
function called _activation_. The outputs of all nodes of layer $l$ combined
gives the output $(y_{l0},\dotsc,y_{l(k-1)})$ of the hidden layer.

The last layer $l=L-1$ is called the _output layer_ and consists of $m$ 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 of the output layer
$(y_{(L-1)0},\dotsc,y_{(L-1)(m-1)})$ is considered as the output of the
network $N$.

The output of a neural network $N$ under input $\boldsymbol{x}$ is denoted
$N(\boldsymbol{x})$. If a node in a layer $l>0$ has less inputs than there are
outputs in layer $l-1$ then we assume that the unconsidered outputs of $l-1$
are weighted with zero. We only consider networks where nodes in hidden layers
have the identity or the ReLU function, and nodes in the output layer have the
identity as activation. The _ReLU function_ is defined as $x\mapsto\max(0,x)$.
Nodes with ReLU or identity activation are called ReLU nodes or identity
nodes, respectively. Given some input to the NN, we say that a ReLU node is
_active_ , resp.  _inactive_ if the input for its activation function is
greater, resp. less than or equal to $0$. We visualize an NN as a directed
graph with weighted edges. An example is given in Fig. 1.

$-1$$0.3$$0.5$$3$$-0.4$$0.98$$1$$-0.745$$-4.1$$2.63$$1$$1.3$$-0.456$$1$$1$$-2.7$$0.24$$-3.21$$0.58$$0.32$$-1$$2.1$$0.52$$-2$$-0.12$
Figure 1: Schema of a neural network with five layers, input dimension of two
and output dimension of one. Filled nodes are ReLU nodes, empty nodes are
identity nodes. An edge between two nodes $u$ and $v$ with label $w$ denotes
that the output of $u$ is weighted with $w$ in the computation of $v$. No edge
between $u$ and $v$ implies $w=0$. The bias of a node is depicted by a value
above or below the node. If there is no such value then the bias is zero.

Our main interest lies in the validity of specifications over the output
values of NN given specifications over their input values. These
specifications are expressed as conjunctions of linear constraints on the
input and output variables of a network.

###### Definition 2

A _specification_ $\varphi$ for a given set of variables $X$ is defined by the
following grammar:

$\displaystyle\varphi$ $\displaystyle::=\varphi\land\varphi\mid t\leq b\qquad$
$\displaystyle t$ $\displaystyle::=c\cdot x\mid t+t$

where $b,c$ are rational constants and $x\in X$ is a variable.

We use $t\geq b$ and $t=b$ as syntactic sugar for $-t\leq-b$ and $t\leq
b\land-t\leq-b$. Furthermore, we use $\top$ for $x+(-x)=0$ and $\bot$ for
$x+(-x)=1$ where $x$ is some variable. We call a specification $\varphi$
simple if for all $t\leq b$ it holds that $t=c\cdot x$ for some rational
constant $c$ and variable $x$.

###### Definition 3

Specification $\varphi(x_{0},\dotsc,x_{n-1})$ is _true_ under
$\boldsymbol{x}=(r_{0},\dotsc,r_{n-1})\in\mathbb{R}^{n}$ if each inequality in
$\varphi$ is satisfied in real arithmetic with each $x_{i}$ set to $r_{i}$.

We write $\varphi(\boldsymbol{x})$ for the application of $\boldsymbol{x}$ to
the variables of $\varphi$. If there are less variables in $\varphi$ than
dimensions in $\boldsymbol{x}$ we ignore the additional values of
$\boldsymbol{x}$. If we consider a specification $\varphi$ in context of a
neural network $N$ we call it an _input or output specification_ and assume
that the set of variables occurring in $\varphi$ is a subset of the input
respectively output variables of $N$.

###### Definition 4

The decision problem NNReach is the following: given a neural network $N$,
input specification $\varphi_{\text{in}}(x_{0},\dotsc,x_{n-1})$ and output
specification $\varphi_{\text{out}}(y_{0},\dotsc,y_{m-1})$, is there
$\boldsymbol{x}\in\bbbr^{n}$ such that $\varphi_{\text{in}}(\boldsymbol{x})$
and $\varphi_{\text{out}}(N(\boldsymbol{x}))$ are true?

##  3 NNReach is NP-Complete

###  3.1 Membership in NP

The argument used by Katz et al. to show membership of NNReach in NP can be
summarized as follows: nondeterministically guess an input vector
$\boldsymbol{x}$ as a witness, compute the output $N(\boldsymbol{x})$ of the
network and check that
$\varphi_{\text{in}}(\boldsymbol{x})\land\varphi_{\text{out}}(N(\boldsymbol{x}))$
holds. It is indisputable that the computation and check of this procedure are
polynomial in the size of $N$, $\varphi_{\text{in}}$, $\varphi_{\text{out}}$
_and_ the size of $\boldsymbol{x}$. However, for inclusion in NP we also need
the size of $\boldsymbol{x}$ to be polynomially bounded in the size of the
instance given as $(N,\varphi_{\text{in}},\varphi_{\text{out}})$. There may be
an argument for this, for instance based on the correspondence between size of
$\boldsymbol{x}$ and required approximation precision for such values.
However, we are not aware of such an argument, let alone a striking one, and
there is also a simpler way of obtaining the upper bound.

###### Definition 5

A _ReLU-linear program_ over a set $X=\\{x_{0},\ldots,x_{n-1}\\}$ of variables
is a set $\Phi$ of (in-)equalities of the form

$b_{j}+\sum_{i=1}^{m}c_{ji}\cdot x_{ji}\leq
x_{j}\qquad\text{or}\qquad\mathop{\mathit{ReLU}}(b_{j}+\sum_{i=1}^{m}c_{ji}\cdot
x_{ji})=x_{j}$

where $x_{ji},x_{j}\in X$ and $c_{ji},b_{j}\in\mathbb{Q}$. Equations of the
second form are called _ReLU-equations_. A _solution_ to $\Phi$ is a vector
$\boldsymbol{x}\in\mathbb{R}^{n}$ which satisfies all (in-)equalities when
each variable $x_{i}\in X$ is replaced by $\boldsymbol{x}(i)$. A ReLU-equality
$\mathop{\mathit{ReLU}}(b_{j}+\sum_{i=1}^{m}c_{ji}\cdot x_{ji})=x_{j}$ is
satisfied by $\boldsymbol{x}$ if

  * •

$b_{j}+\sum_{i=1}^{m}c_{ji}\cdot x_{ji}\geq 0$ and
$x_{j}=b_{j}+\sum_{i=1}^{m}c_{ji}\cdot x_{ji}$, or

  * •

$b_{j}+\sum_{i=1}^{m}c_{ji}\cdot x_{ji}\leq 0$ and $x_{j}=0$.

The problem of _solving_ a ReLU-linear program is: given $\Phi$, decide
whether there is a solution to it.

Any ReLU-linear program without ReLU-equalities is a linear program in the
usual sense, and linear programs are known to be solvable in polynomial time
[7].

######  Lemma 1 ()

The problem of solving a ReLU-linear program is in NP.

###### Proof

Suppose a ReLU-linear program $\Phi$ with $l$ ReLU-equalities is given.
Existence of a solution can be decided as follows. Guess, for each ReLU-
equation $\chi_{k}$ of the form
$\mathop{\mathit{ReLU}}(b_{j}+\sum_{i=1}^{m}c_{ji}\cdot x_{ji})=x_{j}$, some
$a_{k}\in\\{0,1\\}$. Let $\boldsymbol{a}=(a_{0},\ldots,a_{l-1})$. Next, let
$\Phi_{\boldsymbol{a}}$ result from $\Phi$ by replacing each $\chi_{k}$ by the
following (in-)equalities.

$\displaystyle b_{j}+\sum_{i=1}^{m}c_{ji}\cdot x_{ji}\geq 0\enspace,\enspace
b_{j}+\sum_{i=1}^{m}c_{ji}\cdot x_{ji}=x_{j}$ $\displaystyle\text{if }a_{k}=1$
$\displaystyle b_{j}+\sum_{i=1}^{m}c_{ji}\cdot x_{ji}\leq 0\enspace,\enspace
x_{j}=0$ $\displaystyle\text{if }a_{k}=0$

The following is not hard to see: (i) Using standard transformations,
$\Phi_{\boldsymbol{a}}$ can be turned into a linear program of size linear in
$\Phi$. (ii) Any solution to $\Phi_{\boldsymbol{a}}$ is also a solution to
$\Phi$, (iii) If $\Phi$ has a solution, then there is
$\boldsymbol{a}\in\\{0,1\\}^{l}$ such that $\Phi_{\boldsymbol{a}}$ has a
solution. This can be created as follows. Let $\boldsymbol{x}$ be a solution
to $\Phi$. For each ReLU-equation $\chi_{k}$ as above, let $a_{k}=1$ if the
corresponding sum is non-negative, otherwise let $a_{k}=0$. Then
$\boldsymbol{x}$ is also a solution for $\Phi_{\boldsymbol{a}}$. Thus, ReLU-
linear programs can be solved in nondeterministic polynomial time by guessing
$\boldsymbol{a}$, and then constructing the linear program
$\Phi_{\boldsymbol{a}}$ and solving it. ∎

With this definition of a ReLU-linear program and the corresponding lemma at
hand, we are set to prove NP-membership of NNReach.

###### Theorem 3.1

NNReach is in NP.

###### Proof

Let $\mathcal{I}=(N,\varphi_{\text{in}},\varphi_{\text{out}})$. We construct a
ReLU-linear program $\Phi_{\mathcal{I}}$ of size linear in
$|N|+|\varphi_{\text{in}}|+|\varphi_{\text{out}}|$ which is solvable iff there
is a solution for $\mathcal{I}$. The ReLU-linear program $\Phi_{\mathcal{I}}$
contains the following (in-)equalities.

  * •

$\varphi_{\text{in}}$ and $\varphi_{\text{out}}$ (with each conjunct seen as
one (in-)equality),

  * •

for each non-ReLU node $v_{li}$ computing
$\sum_{j}c^{(l-1)}_{ji}y_{(l-1)j}+b_{li}$ add the equality
$\sum_{j}c^{(l-1)}_{ji}y_{(l-1)j}+b_{li}=y_{li}$ (in the form of two
inequalities of appropriate form),

  * •

for each ReLU node $v_{li}$ computing
$\mathop{\mathit{ReLU}}(\sum_{j}c^{(l-1)}_{ji}y_{(l-1)j}+b_{li})$ add the
ReLU-equality
$\mathop{\mathit{ReLU}}(\sum_{j}c^{(l-1)}_{ji}y_{(l-1)j}+b_{li})=y_{li}$.

The claim on the size of $\Phi_{\mathcal{I}}$ should be clear. Moreover, note
that a solution $\boldsymbol{x}$ to $\mathcal{I}$ can be extended to an
assignment $\boldsymbol{x}^{\prime}$ of real values at every node of $N$,
including values $\boldsymbol{y}$ for the output nodes of $N$ s.t., in
particular $N(\boldsymbol{x})=\boldsymbol{y}$. Then $\boldsymbol{x}^{\prime}$
is a solution to $\Phi_{\mathcal{I}}$. Likewise, a solution to
$\Phi_{\mathcal{I}}$ can be turned into a solution to $\mathcal{I}$ by
projection to the input variables.

Hence, NNReach polynomially reduces to the problem of solving ReLU-linear
programs which, by Lem. 1 is in NP. ∎

It is interesting to point out the role of witnesses for positive instances of
the NNReach problem: it is tempting to regard values to the input nodes of the
NN as potential witnesses as done by Katz et al. but, as mentioned before, for
as long as there is no argument for their polynomial boundedness these are
_not_ suitable witnesses in an NP procedure. Instead, Thm. 3.1 above shows
that an assignment to the ReLU nodes as being in-/active can serve as such a
witness. This immediately yields a polynomial fragment of NNReach.

###### Corollary 1

The reachability problem for NN with a bounded number of ReLU nodes is
decidable in polynomial time.

###  3.2 NP-Hardness

$-1$$1$NOT$-1$$-1$$-1$$1$$-1$OR$1$$\varepsilon$$\varepsilon-1$$-1$$1$$1$$1$BOOL$1$$0.5$$-0.5$$-1$$1$$1$$1$$\displaystyle\text{BOOL}^{*}$$1$$-0.5$$\dotsc$AND$1$$1$
Figure 2: Gadgets used in the reduction from 3sat to NNReach. A non-weighted
outgoing edge of a gadget is connected to a weighted incoming edge of another
gadget in the actual construction or is considered an output of the overall
neural network.

Katz et al. try to build a polynomial-time reduction from 3sat to NNReach. The
underlying idea is to encode the structure of a 3sat formula in a neural
network and the existence of a satisfying assignment for this formula in the
corresponding input- and output-specifications. Consider the 3sat instance

$\psi=(X_{0}\lor X_{1}\lor X_{1})\land(\neg X_{0}\lor X_{1}\lor\neg
X_{2})\land(\neg X_{1}\lor X_{2}\lor X_{3})$

with four propositional variables and three clauses, and let
$(N,\varphi_{\text{in}},\varphi_{\text{out}})$ be the NNReach instance
resulting from the mapping of $\psi$ according to the reduction. To understand
the structure of $N$ we make use of so-called gadgets, specified in Fig. 2.
Each gadget is a compact NN and is used to describe a functional subcomponent
of $N$. Using these gadgets, the network $N$ is depicted in Fig. 3.

Ignoring the bool-gadgets for the moment, assume that input values are taken
from $\\{0,1\\}$ instead of $\mathbb{R}$. The function computed by $N$ is
described as follows. Each of the three or-gadgets together with their
connected not-gadgets represent one of the clauses in $\psi$. From Fig. 2 we
can infer that the not-gadgets negate their inputs and that the or-gadgets
output $1$ if at least one input is $1$ and $0$ otherwise. Hence, if an or-
gadget outputs $1$ then the current input, viewed as an assignment to the
propositional variables in $\psi$, satisfies the corresponding clause. The
and-gadget simply sums up all of its inputs and, thus, we get that $y$ is
equal to $3$ iff each or-gadget outputs one. Therefore, with the output
specification $\varphi_{\text{out}}:=y=3$, we get a reduction from 3sat to
NNReach, provided that input values are externally restricted to $\\{0,1\\}$.

But NN are defined for all real-valued inputs, so we need further adjustments
to make the reduction complete. First, note that it is impossible to write an
input specification $\varphi_{\text{in}}(\boldsymbol{x})$ which is satisfied
by $\boldsymbol{x}$ iff $\boldsymbol{x}\in\\{0,1\\}^{n}$ because
$\\{0,1\\}^{n}$ is not a hyperrectangle in $\mathbb{R}^{n}$ but conjunctions
of inequalities only specify hyperrectangles. This is where we make use of
bool-gadgets. Let $\varepsilon$ be a very small constant. A bool-gadget with
input $x$ and output $z$ computes
$z=\mathrm{max}(0,\varepsilon-x)+\mathrm{max}(0,x-1+\varepsilon)$. Now, Katz
et al. claim the following: if $x\in[0;1]$ then we have $z\in[0;\varepsilon]$
iff $x\in[0;\varepsilon]$ or $x\in[1-\varepsilon;1]$. Thus, by connecting a
bool-gadget to each input $x_{i}$ in $N$ and using the simple specifications

$\displaystyle\varphi_{\text{in}}$
$\displaystyle:=\bigwedge_{i=0}^{3}x_{i}\geq 0\land x_{i}\leq 1\enspace$
$\displaystyle\varphi_{\text{out}}$
$\displaystyle:=\bigwedge_{i=0}^{3}z_{i}\geq 0\land z_{i}\leq\varepsilon\land
y\geq 3(1-\varepsilon)\land y\leq 3$

we would get a correct translation of $\psi$. Note that the constraint on $y$
is no longer $y=3$ as the valid inputs to $N$, determined by the bool-gadgets
and their output constraints, are not exactly $0$ or exactly $1$.

ORNOT$x_{0}$$z_{0}$$x_{1}$NOT$x_{2}$$x_{3}$BOOLBOOLBOOLBOOLORORNOTAND$z_{1}$$z_{2}$$z_{3}$$y$
Figure 3: Schema of a neural network resulting from the reduction of the 3sat-
formula $(X_{0}\lor X_{1}\lor X_{1})\land(\neg X_{0}\lor X_{1}\lor\neg
X_{2})\land(\neg X_{1}\lor X_{2}\lor X_{3})$. Note that no weights are
depicted as these are specified inside the gadgets.

However, the claim about bool-gadgets is wrong. Consider a bool-gadget with
very small $\varepsilon$ such that it is safe to assume
$\varepsilon<2\varepsilon<1-\varepsilon$. Then, for $x=2\varepsilon$ we have
$z=0$, which contradicts the claim. In fact, it can be shown that for each
$\varepsilon\leq\frac{1}{2}$ and each input $x\in[0;1]$ the output $z$ is an
element of $[0;\varepsilon]$. Clearly, this is not the intended property of
these gadgets. But with some adjustments to the bool-gadgets we can make the
reduction work.

A $\textsc{bool}^{*}$-gadget is a neural network with functional form
$\bbbr\to\bbbr$ shown in Fig. 2. It computes the function

$\displaystyle
z=\mathrm{max}\left(0,\frac{1}{2}-x\right)+\mathrm{max}\left(0,x-\frac{1}{2}\right)-\frac{1}{2},$

where $x$ is the input variable and $z$ is the output variable. For this
$\textsc{bool}^{*}$-gadget we can show a similar statement as it was intended
for the bool-gadgets in the original proof.

###### Lemma 2

In a $\textsc{bool}^{*}$-gadget with input $x$ and output $z$ we have $z=0$ if
and only if $x=0$ or $x=1$.

###### Proof

Note that
$z=\mathrm{max}\left(0,\frac{1}{2}-x\right)+\mathrm{max}\left(0,x-\frac{1}{2}\right)-\frac{1}{2}$
is equivalent to

$\displaystyle z=\begin{cases}-x&\text{if }x<\frac{1}{2},\\\
x-1&\text{otherwise.}\end{cases}$

From this we immediately get that $z=0$ if $x=0$ or $x=1$, and $z\neq 0$ for
all other values of $x$. ∎

Now, replacing all bool-gadgets with $\textsc{bool}^{*}$-gadgets in the
construction and using the simple specifications $\varphi_{\text{in}}=\top$
and $\varphi_{\text{out}}=\bigwedge_{i=0}^{n-1}z_{i}=0\land y=m$ for a 3sat-
instance with $n$ propositional variables and $m$ clauses, we get a correct
reduction from 3sat to NNReach.

###### Theorem 3.2

NNReach is NP-hard.

One could argue that the networks resulting from the reduction of 3sat are not
typical feed-forward neural networks as they do not follow a layerwise
structure. A reason for this is that some inputs are connected to not-gadgets
where some are not and that the outputs $z_{i}$ are not in the same layer as
the output $y$. This can of course be fixed by introducing additional dummy
nodes.

##  4 NP-Hardness Holds in Very Restricted Cases Already

Let $\mathcal{C}(\textsc{3sat})$ be the class of NNReach instances which are
obtained as images under the reduction presented in the previous section. Note
that the NN of $\mathcal{C}(\textsc{3sat})$ are already quite restricted; they
possess only a fixed number of layers. In this section we strengthen the NP-
hardness result by constructing even simpler classes of NN for which NNReach
is NP-hard already. Sect. 4.1 studies the possibility to make these NN
structurally as simple as possible; Sect. 4.2 shows that requirements on
weights and biases can be relaxed whilst retaining NP-hardness.

###  4.1 Neural Networks of a Simple Structure

We consider NN with just one hidden layer of ReLU nodes and an output
dimension of one. As before, we can establish a reduction from 3sat.

###### Theorem 4.1

NNReach is NP-hard for NN with output dimension one, a single hidden layer and
simple specifications.

###### Proof

Let $\psi$ be a 3sat formula with $n$ propositional variables $X_{i}$ and $m$
clauses $l_{j}$. We slightly modify the construction of a network $N$ in the
proof of Thm. 3.2. First, we remove the last identity node of all
$\textsc{bool}^{*}$-gadgets in $N$ and directly connect the two outputs of
their ReLU nodes to the and-gadget, weighted with $1$. Additionally, we merge
not-gadgets and or-gadgets in $N$. Consider the or-gadget corresponding to
some clause $l_{j}$. The merged gadget has three inputs
$x_{j_{0}},x_{j_{1}},x_{j_{2}}$ and computes
$\max\bigl{(}0,1-\sum_{k=0}^{2}f_{j}(x_{j_{k}})\bigr{)}$ where
$f_{j}(x_{j_{k}})=x_{j_{k}}$ if $X_{j_{k}}$ occurs positively in $l_{j}$ and
$f_{j}(x_{j_{k}})=1-x_{ij}$ if it occurs negatively. It is straightforward to
see that the output of such a gadget is $0$ if at least one positively (resp.
negatively) weighted input is $0$, resp. $1$, and that the output is $1$ if
all positively weighted inputs are $1$ and all negatively weighted inputs are
$0$. These merged gadgets are connected with weight $-1$ to the and-gadget.
Once done for all $\textsc{bool}^{*}$-, not\- and or-gadgets, the overall
output $y$ of $N$ is given by

$\displaystyle\sum_{i=0}^{n-1}\max\bigl{(}0,\frac{1}{2}-x_{i}\bigr{)}+\max\bigl{(}0,x_{i}-\frac{1}{2}\bigr{)}-\sum_{i=0}^{m-1}\max\bigl{(}0,1-\sum_{j=0}^{2}f_{i}(x_{ij})\bigr{)}.$

Note that $N$ has input dimension $n$, a single hidden layer of $2n+m$ ReLU
nodes and output dimension $1$.

Now take the simple specifications
$\varphi_{\text{in}}=\bigwedge_{i=0}^{n-1}x_{i}\geq 0\land x_{i}\leq 1$ and
$\varphi_{\text{out}}=y=\frac{n}{2}$. We argue that the following holds for a
solution to $(N,\varphi_{\text{in}},\varphi_{\text{out}})$: (i) all $x_{i}$
are either $0$ or $1$, and (ii) the output of each merged or-gadget is $0$. To
show (i), we assume the opposite, i.e. there is a solution with
$x_{k}\in(0;1)$ for some $k$. This implies that
$\sum_{i=0}^{n-1}\max\bigl{(}0,\frac{1}{2}-x_{i}\bigr{)}+\max\bigl{(}0,x_{i}-\frac{1}{2}\bigr{)}<\frac{n}{2}$
as for all $x_{i}\in[0;1]$ we have
$\max\bigl{(}0,\frac{1}{2}-x_{i}\bigr{)}+\max\bigl{(}0,x_{i}-\frac{1}{2}\bigr{)}\leq\frac{1}{2}$,
and for $x_{k}$ we have
$\max\bigl{(}0,\frac{1}{2}-x_{k}\bigr{)}+\max\bigl{(}0,x_{k}-\frac{1}{2}\bigr{)}<\frac{1}{2}$.
Furthermore, we must have
$-\sum_{i=0}^{m-1}\max\bigl{(}0,1-\sum_{j=0}^{2}f(x_{ij})\bigr{)}\leq 0$.
Therefore, this cannot be a solution for
$(N,\varphi_{\text{in}},\varphi_{\text{out}})$ as it does not satisfy
$y=\frac{n}{2}$.

To show (ii), assume there is a solution such that one merged or-gadget
outputs a value different from $0$. Then,
$-\sum_{i=0}^{m-1}\max\bigl{(}0,1-\sum_{j=0}^{2}f(x_{ij})\bigr{)}<0$ which in
combination with (i) yields $y<\frac{n}{2}$. Again, this is a contradiction.

Putting (i) and (ii) together, a solution for
$(N,\varphi_{\text{in}},\varphi_{\text{out}})$ implies the existence of a
model for $\psi$. For the opposite direction assume that $\psi$ has a model
$I$. Then, a solution for $(N,\varphi_{\text{in}},\varphi_{\text{out}})$ is
given by $x_{i}=1$ if $I(X_{i})$ is true and $x_{i}=0$ otherwise. ∎

In the previous section, especially in the arguments of Cor. 1, we pointed out
that the occurrence of ReLU nodes is crucial for the NP-hardness of NNReach.
Thus, it is tempting to assume that any major restriction to these nodes leads
to efficiently solvable classes.

######  Theorem 4.2 ()

NNReach is NP-hard for NN where all ReLU nodes have at most one non-zero
weighted input and simple specifications.

###### Proof

We prove NP-hardness via a reduction from 3sat. The reduction works in the
same way as in the proof of Thm. 3.2, but with the following adjustments. We
replace the or-gadgets with simple identity-nodes, we do not include the and-
gadget, and we set the output specification to
$\varphi_{\text{out}}=\bigwedge_{i=0}^{n-1}z_{i}=0\land\bigwedge_{i=0}^{m}y_{i}\geq
1$, where $y_{i}$ is the output of the $i$-th identity-node replacing the
former $i$-th or-gadget, $z_{i}$ is the output of the $i$-th BOOL-gadget, $n$
is the number of propositional variables and $m$ the number of clauses in the
considered 3sat-instance. Note that this is a simple specification and that
the only ReLU nodes in this network are inside the
$\textsc{bool}^{*}$-gadgets, which have only one non-zero input. Now, if each
$z_{i}=0$ then the value of an output $y_{i}$ is equivalent to the number of
inputs equal to $1$. The correctness of this reduction is argued int the exaxt
same way as in in the original one. ∎

###  4.2 Neural Networks with Simple Parameters

$\dotsc$AND$-c$$d$$-c$$-c$DISC$d$$-c$$-c$$\displaystyle\text{EQ}^{0}$$-c$NORM$-c$$d$$-c$$-c$$\displaystyle\overline{\text{NORM}}$$-c$$-c$$d$$d$$-c$$\displaystyle\text{OR}_{A}$$-c$$-c$$-c$$-c$$-c$$-c$$d$$-c$$-c$$-c$$-c$$d$$-c$$-c$$-c$$\displaystyle\text{OR}_{B}$$-c$$-c$$-c$$-c$$-c$$-c$$-c$$-c$$-c$$-c$$d$$-c$$-c$$-c$$-c$$d$
Figure 4: Gadgets used to show that NNReach is NP-hard if restricted to
$\mathcal{C}\left(\\{-c,0,d\\}\right)$ . A non-weighted outgoing edge of a
gadget is connected to a weighted incoming one of another gadget in the actual
construction or are considered as outputs of the overall neural networks.

One could argue that the NP-hardness results in Thm. 3.2 and 4.1 are only
partially applicable to real world problems as the constructed NN use very
specific combinations of weights and biases, namely $-1,0,\frac{1}{2}$ and
$1$, which may be unlikely to occur in this exact combination in real-world
applications. We show that NNReach is already NP-hard in cases where only very
weak assumptions are made on the set of occurring weights and biases.

For $P\subseteq\bbbq$ let $\mathcal{C}(P)$ be the class of NNReach instances
whose NN only use weights and biases from $P$ and simple specifications. We
will show that NP-hardness already occurs when $P$ contains three values: $0$,
some positive and some negative value. We make use of the same techniques as
in Sec. 3 and assume that the general idea of gadgets and the reduction from
3sat to NNReach are known.

###### Definition 6

Let $c,d\in\bbbq^{>0}$ and $\psi$ be a 3sat-formula with $n$ propositional
variables $X_{i}$ and $m$ clauses $l_{j}$. The network $N_{-c,d,\psi}$ is a
network with $2n$ inputs, two for each $X_{i}$, called $x_{i}$ and
$\overline{x_{i}}$. We describe the structure of $N_{-c,d,\psi}$ using the
gadgets from Fig. 4:

  * •

Each input $x_{i}$ is connected to both inputs of a disc-gadget and this
gadget is connected with weight $-c$ to a chain of five identity nodes
interconnected with weight $-c$. We call the output of the last node of this
chain $z_{i}$.

  * •

Each pair $x_{i}$ and $\overline{x_{i}}$ is connected to an
$\textsc{eq}^{0}$-gadget and this gadget is connected with weight $-c$ to a
chain of six identity nodes interconnected with weight $-c$. We call the
output of the last node of this chain $e_{i}$.

  * •

Each input $x_{i}$ is connected to a norm-gadget. Analogously, each
$\overline{x_{i}}$ is connected to a $\overline{\textsc{norm}}$-gadget.

  * •

If $c\geq 1$ (resp. $c<1$) then there are $m$ $\textsc{or}_{A}$-gadgets (resp.
$\textsc{or}_{B}$-gadgets), one for each $l_{j}$ s.t. if $X_{i}$ occurs
positively in $l_{j}$ then the output of the norm-gadget connected to $x_{i}$
is connected and if $X_{i}$ occurs negatively the output of the
$\overline{\textsc{norm}}$-gadget conntected to $\overline{x_{i}}$ is
connected.

  * •

The outputs of all $\textsc{or}_{A}$-gadgets respectively
$\textsc{or}_{B}$-gadgets are connected to a single and-gadget. We denote the
output of this and-gadget with $y$.

Note that each $N_{-c,d,\psi}$ has eight layers and output dimension $2n+1$.
Moreover, $N_{-c,d,\psi}\in\mathcal{C}{\left(\\{-c,0,d\\}\right)}$. Next, we
need to clarify some properties of the used gadgets.

######  Lemma 3 ()

Let $x_{0},x_{1},x_{2}$ denote inputs for some gadget. The following
statements hold:

  1. 1.

If $x_{0}=x_{1}$ then the output of a disc-gadget is $0$ if and only if
$x_{0}=x_{1}=-\frac{d}{c^{2}}$ or $x_{0}=x_{1}=\frac{1}{c}.$

  2. 2.

If $x_{0}=-\frac{d}{c^{2}}$ then the output of a norm-gadget is $0$ and if
$x_{0}=\frac{1}{c}$ then the output is $-dc$.

  3. 3.

If $x_{0}=\frac{d}{c^{2}}$ then the output of
$\overline{\textsc{norm}}$-gadget is $-dc$ and if $x_{0}=-\frac{1}{c}$ then
the output is $0$.

  4. 4.

If $x_{0}=x_{1}=x_{2}=0$ then the output of an $\textsc{or}_{A}$-gadget is
$dc^{4}-dc^{3}$. If at least one input is $-dc$ while the others are $0$ then
the output is $dc^{4}$. The same holds for an $\textsc{or}_{B}$-gadget with
the difference that if $x_{0}=x_{1}=x_{2}=0$ then the output is
$dc^{4}-dc^{5}$.

###### Proof

We start with property 3.1 and assume that the inputs $x_{0},x_{1}$ are equal.
We can infer from the depiction in Fig. 4 that the output of a disc-gadget is
given by $d-c\max(0,dx_{0})-c\max(0,-cx_{1})$. At this point we make a case
distinction. If $x_{0}=x_{1}<0$ then the output is given by $d+c^{2}x_{1}$ and
equal to zero if and only if $x_{1}=-\frac{d}{c^{2}}$. If $x_{0}=x_{1}>0$ then
the output is given by $d-cdx_{0}$ and equal to zero if and only if
$x_{0}=\frac{1}{c}$. The last case, namely $x_{0}=x_{1}=0$, leads to an output
of $d$.

The properties 3.2, 3.3 and 3.4 are easily argued. We can infer from Fig. 4
that the output of a norm-gadget is given by $-c(d-c\max(0,-cx_{0}))$, the
output of a $\overline{\textsc{norm}}$-gadget given by $-c\max(0,c^{2}x_{0})$,
the output of an or-A-gadget given by
$dc^{4}-c\max(0,dc^{2}+c^{2}\sum_{i=0}^{2}x_{i})$ and the output of an OR-B-
gadget given by $dc^{4}-c\max(0,dc^{4}+c^{2}\sum_{i=0}^{2}x_{i})$. Then the
statements about these gadgets follow by inserting the mentioned values and
solving the equations. ∎

With these properties at hand, we are suited to prove our main statement of
this section.

###### Theorem 4.3

Let $c,d\in\bbbq^{>0}$. NNReach restricted to
$\mathcal{C}\left(\\{-c,0,d\\}\right)$ is NP-hard.

###### Proof

Let $c,d\in\mathbb{Q}^{>0}$. Take a 3sat-formula $\psi$ and consider
$(N_{-c,d,\psi},\varphi_{\text{in}},\varphi_{\text{out}})$ with
$N_{-c,d,\psi}$ defined above, $\varphi_{\text{in}}=\top$ and
$\varphi_{\text{out}}=\bigwedge_{i=0}^{n-1}z_{i}=0\land e_{i}=0\land y=m\cdot
d^{2}c^{4}$. Obviously, these specifications are simple.

Clearly, $(N_{-c,d,\psi},\varphi_{\text{in}},\varphi_{\text{out}})$ can be
constructed in time polynomial in the size of $\psi$. For the correctness of
the construction assume that $\psi$ has a model $I$. We claim that
$(N_{-c,d,\psi},\varphi_{\text{in}},\varphi_{\text{out}})$ is solved with
$x_{i}=\frac{1}{c}$ if $I(X_{i})$ is true, $x_{i}=-\frac{d}{c^{2}}$ otherwise,
and $\overline{x_{i}}=-x_{i}$. Note that $\varphi_{\text{in}}$ is trivially
satisfied.

So apply these inputs to $N_{-c,d,\psi}$. According to Lem. 3.1, all outputs
$z_{i}$ are $0$. It is easily verified that all outputs $e_{i}$ are $0$ as
well. Thus, it is left to argue that $y=m\cdot d^{2}c^{4}$. Consider one of
the $\textsc{or}_{\textsc{A}\mid\textsc{B}}$-gadgets occurring in
$N_{-c,d,\psi}$, corresponding to a clause $l_{j}$. Its inputs are given by
the norm\- and $\overline{\textsc{norm}}$-gadgets connected to the inputs
$x_{i}$, resp. $\overline{x_{i}}$ corresponding to the $X_{i}$ occurring in
$l_{j}$. According to Lem. 3.2 and 3 these inputs are either $0$ or $-dc$. If
$l_{j}$ is satisfied by $I$ then there is at least one input to the
$\textsc{or}_{\textsc{A}\mid\textsc{B}}$-gadget that is equal to $-dc$. From
the fact that $\psi$ is satisfied by $I$ and Lem. 3.4 it follows that each
$\textsc{or}_{\textsc{A}\mid\textsc{B}}$-gadget outputs $dc^{4}$. Therefore,
the output $y$ of $N_{-c,d,\psi}$ is $m\cdot d^{2}c^{4}$. This means that
$\varphi_{\text{out}}$ is valid as well.

Consider now the converse direction. A solution for
$(N_{-c,d,\psi},\varphi_{\text{in}},\varphi_{\text{out}})$ must yield that all
$x_{i}$ are $\frac{1}{c}$ or $-\frac{d}{c^{2}}$ and $x_{i}=\overline{x_{i}}$
as all $z_{i}$ and $e_{i}$ have to equal $0$. Therefore, all $m$
$\textsc{or}_{\textsc{A}\mid\textsc{B}}$-gadgets have to output $dc^{4}$ as
$y$ must equal $m\cdot d^{2}c^{4}$. This implies that each
$\textsc{or}_{\textsc{A}\mid\textsc{B}}$-gadget has at least one input that is
$-dc$ which in turn means that there is at least one indirectly connected
$x_{i}$ or $\overline{x_{i}}$ that is $\frac{1}{c}$ resp. $\frac{d}{c^{2}}$.
Thus, $\psi$ is satisfied by setting $X_{i}$ true if $x_{i}=\frac{1}{c}$ and
false if $x_{i}=-\frac{d}{c^{2}}$. ∎

If $d=c$ and we allow for arbitrary specifications we can show that $0$ as a
value for weights or biases is unnecessary to keep the lower bound.

###### Theorem 4.4

Let $c\in\mathbb{Q}^{>0}$. NNReach is NP-hard for NN in
$\mathcal{C}\left(\\{-c,c\\}\right)$ and arbitrary specifications.

###### Proof

This is done in the same way as the proof of Thm. 4.3 with some slight
modifications. We only sketch this reduction by describing the differences
compared to the instances
$(N_{-c,c,\psi},\varphi_{\text{in}},\varphi_{\text{out}})$ resulting from the
reduction used in Thm. 4.3.

We do not use $\textsc{eq}^{0}$-gadgets in the network but add for each input
$x_{i}$ the conjunct $x_{i}=-\overline{x_{i}}$ to the input specification
$\varphi_{\text{in}}$. This also means that we do not include
$\bigwedge_{i=0}^{n-1}e_{i}=0$ in the output specification
$\varphi_{\text{out}}$. Consider the weights between the input and the first
hidden layer. If the inputs $x_{i}$ and $\overline{x_{i}}$ were originally
weighted with zero we set the weights corresponding to $x_{i}$ and
$\overline{x_{i}}$ to be $c$. In combination with the input constraint
$x_{i}=-\overline{x_{i}}$ this is equal to weighting $x_{i}$ and
$\overline{x_{i}}$ with zero. If $x_{i}$ ($\overline{x_{i}}$) was originally
weighted with $c$ we have to set the weight of $\overline{x_{i}}$ ($x_{i}$) to
be $-c$. If it was weighted with $-c$ we have to set the weight of its
counterpart to be $c$. This leads to the case that all non-zero inputs of a
node in the first hidden layer are doubled compared to the same inputs in a
network $N_{-c,c,\psi}$. Consider now the weights between two layers $l$ and
$l+1$ with $l>0$. For each node in $l$ we add a node in the same layer with
the same input weights. If the output of a node in layer $l$ was originally
weighted with zero then we weight it with $c$ and the corresponding output of
its copy with $-c$. If the output was originally weighted with weight $c$
($-c$) then we weight the output of the copy node with $c$ ($-c$), too. As
before, this doubles the input values at the nodes in layer $l+1$, which means
that compared to a network $N_{-c,c,\psi}$ the output value of our modified
network is multiplied by $2^{7}$. Thus, we have to change the output
constraint of $y$ to be $y=2^{7}(m\cdot c^{6})$. Note that these modifications
give a network using only the weights $-c$ and $c$.

To get rid of zero bias, we add the inputs
$x_{\text{bias},1},\overline{x_{\text{bias},1}},\dotsc,x_{\text{bias},7},\overline{x_{\text{bias},7}}$
to the network and add the input constraints
$x_{\text{bias},i}=-\sum_{j=0}^{i-1}\frac{1}{2^{j+1}c^{j}}$ and
$x_{\text{bias},i}=-\overline{x_{\text{bias},i}}$ to $\varphi_{\text{in}}$.
Then, we set the bias of all nodes which originally had a zero bias to be $c$.
For $x_{\text{bias,i}}$ with $i>1$ we add a chain of $i-1$ identity nodes each
with bias $c$ and interconnected with weight $c$ and connect this chain with
weight $c$ to $x_{\text{bias},i}$ and $-c$ to $\overline{x_{\text{bias},i}}$.
All other weights are assumed to be zero which is realized using the same
techniques as described in the previous paragraph. If a node in the first
hidden layer originally had a zero bias we weight the input
$x_{\text{bias},1}$ with $c$ and $\overline{x_{\text{bias},i}}$ with $-c$. If
the input specification holds then the bias plus these inputs sums up to zero.
If a node in some layer $l\in\\{2,\dotsc,7\\}$ originally had a zero bias we
weight the output of the last node of the chain corresponding to
$x_{\text{bias},l}$ and its copy with $c$. Again, if the input specification
holds, the bias value of this node is nullified. This modification ensures
that the network is from $\mathcal{C}(\\{-c,c\\})$. ∎

##  5 Conclusion

We investigated the computational complexity of the reachability problem for
NN with ReLU and identity activations. We revised the original proof of its
NP-completeness, fixing flaws in both the upper and lower bound, and showed
that the parameter driving NP-hardness is the number of ReLU nodes.
Furthermore, we showed that NNReach is difficult for very restricted classes
of small NN already, respectively that three parameters of different signum
occurring as weights and biases suffice for NP-hardness. This indicates that
finding non-trivial classes of NN with practical relevance and polynomial
NNReach is unlikely.

It remains to be seen whether NP-hardness can be strengthened, for instance
for classes of NN with a single hidden layer and a maximum of two non-zero
inputs to ReLU nodes, or only one arbitrary positive and only one arbitrary
negative weight and bias value. However, possible results here are only of
theoretical interest.

From a practical perspective, it would be interesting to see if pure ReLU
networks, where every node in a hidden layer has a ReLU activation, lead to
similar results as these are more common in practice. Also, investigating the
fixed-parameter tractability of the problem more broadly could be promising.
It remains to be seen whether there are parameters other than the number of
ReLU nodes, like structural properties or dimensionality, whose fixing leads
to polynomial decidability. This could yield efficiently solvable classes of
NN that are also of practical interest.

## References

  * [1] Bunel, R., Turkaslan, I., Torr, P.H.S., Kohli, P., Mudigonda, P.K.: A unified view of piecewise linear neural network verification. In: Bengio, S., Wallach, H.M., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada. pp. 4795–4804 (2018), https://proceedings.neurips.cc/paper/2018/hash/be53d253d6bc3258a8160556dda3e9b2-Abstract.html
  * [2] Dixon, M., Klabjan, D., Bang, J.H.: Classification-based financial markets prediction using deep neural networks. Algorithmic Finance 6(3-4), 67–77 (2017). https://doi.org/10.3233/AF-170176
  * [3] Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: D’Souza, D., Kumar, K.N. (eds.) Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10482, pp. 269–286. Springer (2017). https://doi.org/10.1007/978-3-319-68167-2_19
  * [4] Grigorescu, S.M., Trasnea, B., Cocias, T.T., Macesanu, G.: A survey of deep learning techniques for autonomous driving. J. Field Robotics 37(3), 362–386 (2020). https://doi.org/10.1002/rob.21918
  * [5] Hinton, G., Deng, L., Yu, D., Dahl, G.E., Mohamed, A.r., Jaitly, N., Senior, A., Vanhoucke, V., Nguyen, P., Sainath, T.N., et al.: Deep neural networks for acoustic modeling in speech recognition: The shared views of four research groups. IEEE Signal Process. Mag. 29(6), 82–97 (2012). https://doi.org/10.1109/MSP.2012.2205597
  * [6] Huang, X., Kroening, D., Ruan, W., Sharp, J., Sun, Y., Thamo, E., Wu, M., Yi, X.: A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretability. Comput. Sci. Rev. 37, 100270 (2020). https://doi.org/10.1016/j.cosrev.2020.100270
  * [7] Karmarkar, N.: A new polynomial-time algorithm for linear programming. Comb. 4(4), 373–396 (1984). https://doi.org/10.1007/BF02579150
  * [8] Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kuncak, V. (eds.) Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10426, pp. 97–117. Springer (2017). https://doi.org/10.1007/978-3-319-63387-9_5
  * [9] Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: a calculus for reasoning about deep neural networks. Form Methods Syst Des (2021). https://doi.org/10.1007/s10703-021-00363-7
  * [10] Khan, A., Sohail, A., Zahoora, U., Qureshi, A.S.: A survey of the recent architectures of deep convolutional neural networks. Artif. Intell. Rev. 53(8), 5455–5516 (2020). https://doi.org/10.1007/s10462-020-09825-6
  * [11] Krizhevsky, A., Sutskever, I., Hinton, G.E.: Imagenet classification with deep convolutional neural networks. Commun. ACM 60(6), 84–90 (2017). https://doi.org/10.1145/3065386
  * [12] Litjens, G., Kooi, T., Bejnordi, B.E., Setio, A.A.A., Ciompi, F., Ghafoorian, M., van der Laak, J.A.W.M., van Ginneken, B., Sánchez, C.I.: A survey on deep learning in medical image analysis. Medical Image Anal. 42, 60–88 (2017). https://doi.org/10.1016/j.media.2017.07.005
  * [13] Narodytska, N., Kasiviswanathan, S.P., Ryzhyk, L., Sagiv, M., Walsh, T.: Verifying properties of binarized deep neural networks. In: McIlraith, S.A., Weinberger, K.Q. (eds.) Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018. pp. 6615–6624. AAAI Press (2018), https://www.aaai.org/ocs/index.php/AAAI/AAAI18/paper/view/16898
  * [14] Ruan, W., Huang, X., Kwiatkowska, M.: Reachability analysis of deep neural networks with provable guarantees. In: Lang, J. (ed.) Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden. pp. 2651–2659. ijcai.org (2018). https://doi.org/10.24963/ijcai.2018/368
  * [15] Ruan, W., Huang, X., Kwiatkowska, M.: Reachability analysis of deep neural networks with provable guarantees. CoRR abs/1805.02242 (2018), http://arxiv.org/abs/1805.02242