In this paper, we consider the computational complexity of bounding the reachable set of a Linear Time-Invariant (LTI) system controlled by a Rectified Linear Unit (ReLU) Two-Level Lattice (TLL) Neural Network (NN) controller. In particular, we show that for such a system and controller, it is possible to compute the exact one-step reachable set in polynomial time in the size of the TLL NN controller (number of neurons). Additionally, we show that a tight bounding box of the reachable set is computable via two polynomial-time methods: one with polynomial complexity in the size of the TLL and the other with polynomial complexity in the Lipschitz constant of the controller and other problem parameters. Finally, we propose a pragmatic algorithm that adaptively combines the benefits of (semi-)exact reachability and approximate reachability, which we call L-TLLBox. We evaluate L-TLLBox with an empirical comparison to a state-of-the-art NN controller reachability tool. In our experiments, L-TLLBox completed reachability analysis as much as 5000x faster than this tool on the same network/system, while producing reach boxes that were from 0.08 to 1.42 times the area.
翻译:在本文中,我们考虑了由校正线性线性单位(RELU) 控制神经网络控制器(NN) 控制的线性时间变量系统(LTI) 的可达性约束组的计算复杂性。 特别是, 我们显示, 对于这样的系统和控制器, 可以用TLL NN 控制器( 神经元数量) 的大小来计算多元时间中精确的一步可达性设定。 此外, 我们显示, 一个紧紧的可达性框可以通过两种多元时间方法进行比较: 一种是TLLL规模的多元复杂度,另一种是控制器和其他问题参数的利普施茨常数的多元复杂度。 最后, 我们提出一种务实的算法, 将( 半) 异性可达性和近似可达性( L- LLLLLBox) 控制器的优点和近似可达性( 我们称之为L- TLLLBox ) 。 我们用实验用一个实验性比较方式将LL-T 与一个状态的可达性1- NLLVLV) 的可达性分析器作为5000- 工具, 完成的LLLT 的可达性工具。