< Retour au sommaire

Dynamic System with Neural Components Verification using Forward Analysis

Samuel Akinwande le

Lieu: 1092

Suivre en visio

As dynamical systems controlled by neural networks (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 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 polyhedral enclosures (i.e., abstractions). These enclosures, combined with the neural controller, are then encoded as mixed-integer linear programs (MILPs). Solving these MILPs yields 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 current state of the art.