Prof. Sam Coogan (GA Tech): Contraction-guided safety and reachability analysis of neural network controlled systems

In this talk, we study safety properties of a dynamical system in feedback with a neural network controller from a reachability perspective. We first embed the closed-loop dynamics into a larger system using the theory of mixed monotone dynamical systems with favorable control theoretic properties. In particular, we show that hyper-rectangular over-approximations of the reachable sets are efficiently computed using a single trajectory of the embedding system. Numerically computing this trajectory requires bounds on the input-output behavior of the neural network controller, which we obtain via carefully selected and infrequent queries to an oracle. We assume the oracle provides these input-output bounds as intervals or as affine bounding functions, which is common for many state-of-the-art methods. Moreover, we show that, if this embedding system is constructed in a certain way, the contraction rate of the embedding system is the same as the original closed-loop system. Thus, this embedding provides a scalable approach for reachability analysis of the neural network control loop while preserving the nonlinear structure of the 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.