Backward Reachability Analysis for Neural Feedback Loops

TL;DR

This paper introduces a backward reachability method for verifying the safety of neural feedback loops, overcoming challenges posed by neural network nonlinearities and non-invertibility, and demonstrating improved safety certification in control systems.

Contribution

It develops a novel backward reachability analysis technique for neural feedback loops using affine bounds and linear programming, addressing neural network nonlinearities and non-invertibility.

Findings

Reduces conservativeness of backprojection set estimates by up to 88%.

Successfully verifies safety in a collision avoidance scenario where forward methods fail.

Demonstrates low computational cost of the proposed approach.

Abstract

The increasing prevalence of neural networks (NNs) in safety-critical applications calls for methods to certify their behavior and guarantee safety. This paper presents a backward reachability approach for safety verification of neural feedback loops (NFLs), i.e., closed-loop systems with NN control policies. While recent works have focused on forward reachability as a strategy for safety certification of NFLs, backward reachability offers advantages over the forward strategy, particularly in obstacle avoidance scenarios. Prior works have developed techniques for backward reachability analysis for systems without NNs, but the presence of NNs in the feedback loop presents a unique set of problems due to the nonlinearities in their activation functions and because NN models are generally not invertible. To overcome these challenges, we use existing forward NN analysis tools to find affine bounds on the control inputs and solve a series of linear programs (LPs) to efficiently find an approximation of the backprojection (BP) set, i.e., the set of states for which the NN control policy will drive the system to a given target set. We present an algorithm to iteratively find BP set estimates over a given time horizon and demonstrate the ability to reduce conservativeness in the BP set estimates by up to 88% with low additional computational cost. We use numerical results from a double integrator model to verify the efficacy of these algorithms and demonstrate the ability to certify safety for a linearized ground robot model in a collision avoidance scenario where forward reachability fails.