A New Strategy for Verifying Reach-Avoid Specifications in Neural Feedback Systems

TL;DR

The paper tackles verification of reach-avoid specifications for neural feedback systems, where forward reachability is common but backward analysis remains challenging and scalable solutions are scarce. It proposes a unified FaBRe strategy that partitions the horizon into $F$ forward and $B$ backward steps, combining forward over-approximations with backward hyperrectangle approximations to certify safety or reach-avoid properties. Three backward-approximation algorithms are introduced—Golden Section Search, Iterative Convex Hull, and Largest Empty Box—together with MILP-based under-approximation to yield sound bounds. Preliminary comparisons against state-of-the-art methods suggest potential scalability improvements for verifying neural feedback systems with complex dynamics and disturbances.

Abstract

Forward reachability analysis is the predominant approach for verifying reach-avoid properties in neural feedback systems (dynamical systems controlled by neural networks). This dominance stems from the limited scalability of existing backward reachability methods. In this work, we introduce new algorithms that compute both over- and under-approximations of backward reachable sets for such systems. We further integrate these backward algorithms with established forward analysis techniques to yield a unified verification framework for neural feedback systems.