This paper proposes a computationally efficient framework, based on interval analysis, for rigorous verification of nonlinear continuous-time dynamical systems with neural network controllers. Given a neural network, we use an existing verification algorithm to construct inclusion functions for its input-output behavior. Inspired by mixed monotone theory, we embed the closed-loop dynamics into a larger system using an inclusion function of the neural network and a decomposition function of the open-loop system. This embedding provides a scalable approach for safety analysis of the neural control loop while preserving the nonlinear structure of the system. We show that one can efficiently compute hyper-rectangular over-approximations of the reachable sets using a single trajectory of the embedding system. We design an algorithm to leverage this computational advantage through partitioning strategies, improving our reachable set estimates while balancing its runtime with tunable parameters. We demonstrate the performance of this algorithm through two case studies. First, we demonstrate this method's strength in complex nonlinear environments. Then, we show that our approach matches the performance of the state-of-the art verification algorithm for linear discretized systems.
翻译:本文提出一个基于间距分析的计算高效框架, 用于严格核查神经网络控制器的非线性连续时动态系统。 在神经网络中, 我们使用现有的核查算法来构建输入输出行为的包容功能。 在混合单体理论的启发下, 我们将闭环动态嵌入一个更大的系统, 使用神经网络的包容功能和开放环系统分解功能。 这个嵌入提供了一种可扩缩的方法, 用于对神经控制环进行安全分析, 同时保护系统的非线性结构。 我们显示, 可以利用嵌入系统单一轨迹, 高效地计算超长角超匹配的可达域元功能。 我们设计一种算法, 通过分隔战略, 改进我们的可达集估计值, 同时平衡其运行时间与可捕量参数。 我们通过两个案例研究来展示这一算法的性能。 首先, 我们展示了这个方法在复杂的非线性环境中的强度。 然后, 我们展示了我们的方法与直线化系统艺术核查的性能相匹配。