Bounding the Complexity of Formally Verifying Neural Networks: A Geometric Approach
Bounding the Complexity of Formally Verifying Neural Networks: A Geometric Approach
复制标题
DOI：
10.1109/cdc45484.2021.9683375
复制
发表时间：
2020-12
期刊：
影响因子：
--
通讯作者：
James Ferlez;Yasser Shoukry
中科院分区：
文献类型：
--
作者：
James Ferlez;Yasser Shoukry
在本文中，我们考虑了正式验证整流线性单元（ReLU）神经网络（NN）行为的计算复杂性，其中验证需要确定NN是否满足凸多边形规范。具体来说，我们表明，对于两种不同的神经网络架构——浅神经网络和两级晶格（TLL）神经网络——当验证问题的所有其他方面保持固定时，具有（凸）多面体约束的验证问题是待验证神经网络中神经元数量的多项式。我们通过为每种类型的体系结构展示显式的（但相似的）验证算法来实现这些复杂性结果。两种算法都通过超平面有效地将神经网络参数转化为神经网络输入空间的分区；这将原始的验证问题分解为多项式的许多子验证问题，这些子验证问题来源于神经元的几何形状。我们表明，这些子问题可以被选择，使得神经网络在每个子问题中都是纯仿射的，因此每个子问题都可以在多项式时间内通过线性规划（LP）解决。因此，可以使用已知的算法来枚举超平面排列中的区域，从而获得原始验证问题的多项式时间算法。最后，我们将我们提出的算法用于动态系统的验证，特别是当这些神经网络架构用作LTI系统的状态反馈控制器时。我们进一步用数值方法评估了这种方法的可行性。
In this paper, we consider the computational complexity of formally verifying the behavior of Rectified Linear Unit (ReLU) Neural Networks (NNs), where verification entails determining whether the NN satisfies convex polytopic specifications. Specifically, we show that for two different NN architectures – shallow NNs and Two-Level Lattice (TLL) NNs – the verification problem with (convex) polytopic constraints is polynomial in the number of neurons in the NN to be verified, when all other aspects of the verification problem held fixed. We achieve these complexity results by exhibiting explicit (but similar) verification algorithms for each type of architecture. Both algorithms efficiently translate the NN parameters into a partitioning of the NN’s input space by means of hyperplanes; this has the effect of partitioning the original verification problem into polynomially many sub-verification problems derived from the geometry of the neurons. We show that these sub-problems may be chosen so that the NN is purely affine within each, and hence each sub-problem is solvable in polynomial time by means of a Linear Program (LP). Thus, a polynomial-time algorithm for the original verification problem can be obtained using known algorithms for enumerating the regions in a hyperplane arrangement. Finally, we adapt our proposed algorithms to the verification of dynamical systems, specifically when these NN architectures are used as state-feedback controllers for LTI systems. We further evaluate the viability of this approach numerically.