Verifying Nonlinear Neural Feedback Systems using Polyhedral Enclosures

As dynamical systems controlled by neural networks become increasingly prevalent, it is critical to ensure their safe operation. Although efficient techniques exist to handle neural systems with linear transition functions, few scalable methods address the nonlinear case. We propose a novel algorithm for verifying nonlinear neural feedback systems using forward reachability analysis. Our algorithm leverages the structure of the nonlinear transition functions to compute tight linear abstractions which we call polyhedral enclosures. These are then encoded as mixed-integer linear programs (MILPs) and solved to yield a sound over-approximation of the forward-reachable set. We evaluate our algorithm on representative benchmarks and demonstrate an order of magnitude improvement over the previous state of the art