Robustness Verifcation in Neural Networks

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.

;Comment: 16 pages, 1 figure