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

AI summary

Overview

Research area: Formal verification of neural feedback systems (dynamical systems controlled by neural networks), specifically reachability analysis for reach-avoid specifications.

Technical level: Advanced. The paper is written for readers comfortable with set-valued dynamical systems, over/under-approximation theory, optimization formulations (including MILP), and neural network verification.

Scope: The paper proposes new backward reachability algorithms, including over- and under-approximations of backward reachable sets, and combines them with an existing forward analysis method into a unified verification strategy called FaBRe.

What This Paper Is About

Verifying that a neural-network-controlled dynamical system always reaches a goal while never entering unsafe states is normally done by propagating the system forward in time, because propagating backward through a neural network is hard. This limits existing verification methods. The paper's goal is to build tractable algorithms for backward reachability analysis and to combine them with forward analysis so that the two approaches jointly verify safety properties.

Key Contributions

1. New backward reachability algorithms. The paper introduces three methods for computing an under-approximation of the backward reachable set (BRS) from a guaranteed over-approximation: Golden Section Search (GSS), Iterative Convex Hull (ICH), and Largest Empty Box (LEB).

2. A bounding formulation for backward sets. The paper formulates a minimization problem whose solution gives a lower bound on the preimage (Equation 2), and shows that replacing the minimization with a maximization yields an upper bound; together these define a hyperrectangle that is a guaranteed over-approximation of the true BRS.

3. The FaBRe verification strategy. A unified framework that partitions the time horizon into T = F + B steps, using F steps of forward analysis and B steps of backward analysis. Containment of the forward over-approximation within the backward under-approximation certifies the reach property; disjointness of forward and backward over-approximations certifies the avoid property.

4. A combined verification criterion for reach-avoid safety. The paper defines safety of a system as satisfaction of either the forward or backward reach-avoid properties and shows how the two property sets (Equations 3 and 4) can be used jointly, rather than exclusively, to establish safety soundly.

Main Findings

• Forward analysis dominates because backward analysis does not scale. The paper states that most existing reachability methods for neural feedback systems rely on forward analysis, and attributes this to the difficulty of computing a backward pass through a neural network and the limited scalability of existing backward reachability methods.

• Backward preimages can be soundly bounded by optimization. Solving the minimization problem in Equation 5 gives a lower bound on the preimage from Equation 2, and replacing the minimization with a maximization gives an upper bound; the two together define a hyperrectangle that is a guaranteed over-approximation of the true backward reachable set.

• Under-approximations can be extracted from over-approximations. The paper formulates the under-approximation problem as finding the largest subset of the over-approximation whose over-approximated forward image remains within the target set, and offers three methods for solving it.

• GSS trades query cost for simplicity. The Golden Section Search method parameterizes the under-approximate hyperrectangle as c ± ρr with ρ in (0, 1), where c is the center and r the radii of the over-approximate hyperrectangle, and searches for the maximal ρ; the paper notes this may require many forward queries.

• ICH is a sampling-based alternative. Iterative Convex Hull densely samples the over-approximate hyperrectangle, labels points as positive or negative based on containment in the target set, forms a candidate under-approximation from the positive samples, and validates it with an over-approximated query, repeating with the candidate as the new over-approximation if validation fails.

• LEB targets nonconvex reachable sets. For highly nonconvex reachable sets, the paper solves a small MILP to find the largest candidate under-approximate hyperrectangle excluding all negative samples from ICH.

• No empirical results are reported. The paper's Section 3.4 describes ongoing work: comparisons of the over-approximation method with the work cited as [6], the under-approximation method with [7], and FaBRe with the state-of-the-art forward reachability method of [1]. The paper reports that results are not yet available, and states the goal of demonstrating measurable improvements in scalability over current approaches. No datasets, benchmarks, runtimes, or numerical results appear in the provided content.

Methodology in Plain English

The authors start from the standard way of describing a neural feedback system: a state evolves over T discrete steps, each of duration δ, with a state update driven by a state update function f, a neural network controller u (a fully-connected feed-forward network with n inputs, n outputs, and ReLU activations), and a perturbation term drawn from a set E. Because the perturbation is a set rather than a single value, each state maps to a set of possible next states.

Forward reachability propagates the initial set I through this update for T steps, producing an over-approximation of all reachable states. The paper's forward component reuses the method of [1]. Backward reachability asks the reverse question: given a target set (such as the goal set G or the avoid set A), which states are guaranteed to map into it? This preimage operation (Equation 2) has no scalable direct solver, so instead of computing it exactly, the authors compute bounds. For each component of the state, they solve an optimization problem that finds the minimal value reachable in one step from the target set; that minimum gives a lower bound. Maximizing instead of minimizing gives an upper bound. These per-component bounds assemble into a hyperrectangle that provably contains the true backward reachable set.

Once they have that guaranteed over-approximation, they try to carve an under-approximation out of it: the largest axis-aligned box for which the forward image, computed with an over-approximating method, still lies inside the target set. Three strategies do this. GSS shrinks a scaled copy of the box toward its center and binary-searches the scale factor. ICH instead samples many points in the box, checks which ones land in the target, builds a candidate box from the successes, and validates it; failures feed back as new constraints. LEB handles the nonconvex case by solving a small mixed-integer linear program that finds a large box containing no known-bad samples.

The FaBRe strategy then splits the time budget: F steps forward, B steps backward, with T = F + B. For a reach property, if the forward over-approximation after F steps sits inside the backward under-approximation after B steps, the system provably reaches the goal. For an avoid property, the forward over-approximation from the initial set and the backward over-approximation from the avoid set are computed, and if they are disjoint at every time step in [1, T], the system provably avoids all unsafe states.

Why This Matters

Impact on research. The paper attacks a structural limitation in neural feedback system verification: the field's near-exclusive reliance on forward reachability. By supplying tractable backward over- and under-approximation algorithms and a principled way to combine them, it opens a direction for hybrid verification that could trade precision and scalability more flexibly than either direction alone. Because the backward preimage is characterized through optimization bounds rather than exact computation, the approach is compatible with existing forward analysis tools and does not require a new verification pipeline.

Real-world applications.

• Robotics, where a learned controller must drive a system to a target region while provably avoiding collisions or unsafe configurations.
• Autonomous driving, cited in the paper as an application area, where a neural controller must reach a destination while never entering unsafe states.
• Aerospace autonomy, also cited in the paper, where flight control policies must satisfy goal-reaching and avoidance specifications under disturbances.
• Any deployed neural controller subject to bounded disturbances and formal safety requirements, where certification of reach-avoid behavior is needed rather than empirical testing alone.

Industry relevance. Sampling-based falsification is common in industrial practice because it scales, but it cannot provide formal guarantees, and certificate-based invariance methods are often hard to construct. A verification method that is both sound and scalable would give engineers a path to certify neural controllers without relying on sampling. The paper also frames its contribution as aiming to demonstrate measurable improvements in scalability over current state-of-the-art forward reachability methods, which is the practical bottleneck in industrial verification.

Future Directions

• Empirical evaluation of the three backward methods. The paper states it is comparing its over-approximation method with the work of [6] and its under-approximation method with [7]. The relative accuracy and cost of GSS, ICH, and LEB remain to be established.

• Benchmarking FaBRe against forward-only analysis. The paper is comparing FaBRe with the state-of-the-art forward reachability method of [1]. Whether a mixed forward/backward split improves scalability in practice, and how the split F/B should be chosen, is left open.

• Choosing the split parameter. The paper treats the subdivision T = F + B as a configurable parameter of the solver, but how to select F and B automatically to maximize verification success or minimize computation is not addressed.

• Scaling to higher dimensions and nonconvex sets. The paper notes that precise reachability methods scale poorly due to the curse of dimensionality, and it introduces LEB specifically for highly nonconvex reachable sets, leaving the question of how these methods behave as dimension grows.

Target Audience

This paper is aimed at researchers and graduate students working on formal verification, neural network verification, and safety-critical control. It will be most useful to readers already familiar with reachability analysis, set-valued dynamical systems, and neural network verification tooling. Practitioners building certified controllers for robotics, autonomous driving, or aerospace autonomy will find the problem framing relevant, though the aggressive use of mathematical notation and the absence of experimental results mean it functions as a methods proposal rather than an evaluation paper. Readers looking for benchmarks or performance numbers will not find them here.

Authors’ 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.