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.

翻译：本文提出了一种基于区间分析的计算高效框架，用于严格验证带有神经网络控制器的非线性连续时间动力系统。给定一个神经网络，我们利用现有验证算法为其输入-输出行为构建包含函数。受混合单调理论启发，我们通过神经网络的包含函数与开环系统的分解函数将闭环动力学嵌入到更大的系统中。这种嵌入方法在保持系统非线性结构的同时，为神经控制回路的 safety 分析提供了可扩展方法。我们证明了可以通过嵌入系统的单条轨迹高效计算可达集的超矩形超近似。通过设计分区策略的算法，我们利用这一计算优势，在平衡运行时间与可调参数的同时改进了可达集估计。通过两个案例研究展示了该算法的性能：首先展示了该方法在复杂非线性环境中的优势，随后证明我们的方法在线性离散化系统中达到了与最先进验证算法相当的性能。