Polynomial-Time Reachability for LTI Systems With Two-Level Lattice Neural Network Controllers

In this letter, 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 $5000\times$ 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）双层格（TLL）神经网络（NN）控制器控制的线性时不变（LTI）系统的可达集界定的计算复杂性。特别地，我们表明对于这样一个系统和控制器，有可能在TLL神经网络控制器（神经元数量）规模的多项式时间内计算出精确的单步可达集。此外，我们表明可达集的紧密边界框可通过两种多项式时间方法计算：一种在TLL规模上具有多项式复杂性，另一种在控制器的利普希茨常数和其他问题参数上具有多项式复杂性。最后，我们提出一种实用算法，它自适应地结合了（半）精确可达性和近似可达性的优点，我们称之为L - TLLBox。我们通过与一种最先进的神经网络控制器可达性工具进行实证比较来评估L - TLLBox。在我们的实验中，L - TLLBox在相同的网络/系统上完成可达性分析的速度比该工具快多达5000倍，同时生成的可达框面积是其0.08到1.42倍。