  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.
