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

arXiv: https://arxiv.org/abs/2601.08065 · HTML: https://mlsanity.com/paper/2601.08065/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 6 of its 7 references that are in the map.
- First posted on arXiv 12 Jan 2026.

## Builds on (most cited first, 6 of 6)

- [Large Scale Interactive Motion Forecasting for Autonomous Driving : The Waymo Open Motion Dataset](https://mlsanity.com/paper/2104.10133/) (2021)
- [Backward Reachability Analysis of Neural Feedback Loops: Techniques for Linear and Nonlinear Systems](https://mlsanity.com/paper/2209.14076/) (2022)
- [Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates](https://mlsanity.com/paper/2405.14058/) (2024)
- [Diffusion-Based Failure Sampling for Evaluating Safety-Critical Autonomous Systems](https://mlsanity.com/paper/2406.14761/) (2024)
- [Polyhedral Enclosures: An Efficient Combinatorial Abstraction for Nonlinear Neural Feedback Systems](https://mlsanity.com/paper/2503.22660/) (2025)
- [BURNS: Backward Underapproximate Reachability for Neural-Feedback-Loop Systems](https://mlsanity.com/paper/2505.03643/) (2025)

## Abstract (arXiv)

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.