限定神经网络形式化验证复杂度的几何方法
机器学习
2021-03-26 v2
摘要
在本文中，我们考虑形式化验证修正线性单元（ReLU）神经网络（NNs）行为计算复杂度的问题，其中验证是指确定该 NN 是否满足凸多面体规范。具体而言，我们证明对于两种不同的 NN 架构——浅层 NN 和两级格（TLL）NN——当验证问题的其他所有方面保持固定时，带有（凸）多面体约束的验证问题在待验证 NN 的神经元数量上是多项式级的。我们通过为每种架构给出显式（但相似）的验证算法来得到这些复杂度结果。两种算法都通过超平面将 NN 参数高效地转化为对 NN 输入空间的划分；这起到了将原始验证问题依据神经元的几何结构划分为多项式多个子验证问题的作用。我们证明可以选择这些子问题，使得 NN 在每一个子问题内是纯仿射的，因此每个子问题可通过线性规划（LP）在多项式时间内求解。于是，利用已知的枚举超平面排列中区域数的算法，可获得原始验证问题的多项式时间算法。最后，我们将所提算法适配于动力系统的验证，特别是当这些 NN 架构被用作 LTI 系统的状态反馈控制器时。我们进一步从数值上评估了该方法的可行性。
引用
@article{arxiv.2012.11761,
title = {Bounding the Complexity of Formally Verifying Neural Networks: A Geometric Approach},
author = {James Ferlez and Yasser Shoukry},
journal= {arXiv preprint arXiv:2012.11761},
year = {2021}
}