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.

翻译：本文研究神经网络计算的形式化验证问题。核心关注各类鲁棒性与极小化问题，例如：给定线性规划实例形式下的输入输出符号规范，是否存在有效输入使得网络计算出有效输出？该性质是否对所有有效输入成立？两个给定网络是否计算相同函数？是否存在更小的网络实现相同函数计算？这些问题近期已有实际视角的研究，并采用启发式算法进行近似求解。我们通过构建一个理论框架来补充现有成果，该框架使我们能够互换神经网络中的安全性与效率问题，并分析其计算复杂性。研究表明，在半线性设定下这些问题具有可解性，即当使用分段线性激活函数且采用求和或最大值度量时，多数问题最多属于P类或NP类。