The FABRIC Strategy for Verifying Neural Feedback Systems
This work addresses the verification problem for neural feedback systems, which is crucial for safety-critical applications, by providing a more scalable and integrated approach, though it is incremental in combining existing forward techniques with novel backward methods.
The paper tackles the limited scalability of backward reachability analysis for neural feedback systems by introducing new algorithms for computing over- and underapproximations of backward reachable sets and integrating them with forward analysis into the FaBRIC algorithm. The result is a significant performance improvement over prior state-of-the-art methods on benchmark evaluations.
Forward reachability analysis is a dominant approach for verifying reach-avoid specifications in neural feedback systems, i.e., dynamical systems controlled by neural networks, and a number of directions have been proposed and studied. In contrast, far less attention has been given to backward reachability analysis for these systems, in part because of the limited scalability of known techniques. In this work, we begin to address this gap by introducing new algorithms for computing both over- and underapproximations of backward reachable sets for nonlinear neural feedback systems. We also describe and implement an integration of these backward reachability techniques with existing ones for forward analysis. We call the resulting algorithm Forward and Backward Reachability Integration for Certification (FaBRIC). We evaluate our algorithms on a representative set of benchmarks and show that they significantly outperform the prior state of the art.