In this paper we investigate formal verification problems for Neural Network computations. Various reachability problems will be in the focus, such as: Given symbolic specifications of allowed inputs and outputs in form of Linear Programming instances, one question is whether valid inputs exist such that the given network computes a valid output? Does this property hold for all valid inputs? The former question's complexity has been investigated recently by S\"alzer and Lange for nets using the Rectified Linear Unit and the identity function as their activation functions. We complement their achievements by showing that the problem is NP-complete for piecewise linear functions with rational coefficients that are not linear, NP-hard for almost all suitable activation functions including non-linear ones that are continuous on an interval, complete for the Existential Theory of the Reals $\exists \mathbb R$ for every non-linear polynomial and $\exists \mathbb R$-hard for the exponential function and various sigmoidal functions. For the completeness results, linking the verification tasks with the theory of Constraint Satisfaction Problems turns out helpful.

翻译：本文研究了神经网络计算的形式化验证问题。重点关注各类可达性问题，例如：给定以线性规划形式表示的允许输入和输出的符号规范，问题包括：是否存在有效输入使得给定网络计算出有效输出？该性质是否对所有有效输入成立？Salzer与Lange最近使用修正线性单元和恒等函数作为激活函数的网络研究了前一类问题的复杂度。我们通过展示以下结果补充了他们的工作：对于具有有理系数的分段线性函数（非线性的情况），该问题为NP完全；对于几乎所有合适的激活函数（包括在区间上连续的非线性函数），该问题为NP困难；对于任意非线性多项式函数，该问题为实数存在理论（$\exists \mathbb R$）完全；对于指数函数和各种S型函数，该问题为$\exists \mathbb R$困难。在完备性结果中，将验证任务与约束满足问题理论相关联被证明是有帮助的。