The FABRIC Strategy for Verifying Neural Feedback Systems

TL;DR

This paper introduces FaBRIC, a novel algorithm that combines forward and backward reachability analysis to improve verification of neural feedback systems, addressing scalability issues and enhancing certification capabilities.

Contribution

The paper presents new algorithms for backward reachability analysis and integrates them with existing forward methods, significantly advancing neural system verification.

Findings

FaBRIC outperforms previous methods on benchmarks

Backward analysis improves verification accuracy

Integrated approach enhances scalability and robustness

Abstract

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.