Efficient Interaction-Aware Interval Analysis of Neural Network Feedback Loops
This work addresses the challenge of verifying safety in control systems with neural network components, which is crucial for applications like autonomous vehicles, but it is incremental as it builds on existing verification methods.
The paper tackles the problem of efficiently analyzing neural network feedback loops by proposing a framework for interval reachability that uses embedding systems to over-approximate behavior under uncertainty, achieving scalability up to 200 state dimensions.
In this paper, we propose a computationally efficient framework for interval reachability of systems with neural network controllers. Our approach leverages inclusion functions for the open-loop system and the neural network controller to embed the closed-loop system into a larger-dimensional embedding system, where a single trajectory over-approximates the original system's behavior under uncertainty. We propose two methods for constructing closed-loop embedding systems, which account for the interactions between the system and the controller in different ways. The interconnection-based approach considers the worst-case evolution of each coordinate separately by substituting the neural network inclusion function into the open-loop inclusion function. The interaction-based approach uses novel Jacobian-based inclusion functions to capture the first-order interactions between the open-loop system and the controller by leveraging state-of-the-art neural network verifiers. Finally, we implement our approach in a Python framework called ReachMM to demonstrate its efficiency and scalability on benchmarks and examples ranging to $200$ state dimensions.