Robustness Verifcation in Neural Networks
Adrian Wurm
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.