Polyhedral Enclosures: An Efficient Combinatorial Abstraction for Nonlinear Neural Feedback Systems
This work addresses the need for scalable verification methods for nonlinear neural feedback systems, which are critical for ensuring safety in control applications.
The paper proposes a novel algorithm for forward reachability analysis of nonlinear neural feedback systems, using polyhedral enclosures and mixed-integer linear programming to compute sound over-approximations of reachable sets. The method demonstrates significant improvements over the current state of the art on representative benchmarks.
As dynamical systems equipped with neural network controllers (neural feedback systems) become increasingly prevalent, it is critical to develop methods to ensure their safe operation. Verifying safety requires extending control theoretic analysis methods to these systems. Although existing techniques can efficiently handle linear neural feedback systems, relatively few scalable methods address the nonlinear case. We propose a novel algorithm for forward reachability analysis of nonlinear neural feedback systems. The approach leverages the structure of the nonlinear transition functions of the systems to compute tight polyhedral enclosures (i.e., abstractions). These enclosures, combined with the neural controller, are then encoded as a mixed-integer linear program (MILP). Optimizing this MILP yields a sound over-approximation of the forward-reachable set. Beyond the conference version of this work, we perform more extensive ablations, and introduce further optimizations to the algorithm. We evaluate our algorithm on representative benchmarks, and demonstrate significant improvements over the current state of the art.