# BURNS: Backward Underapproximate Reachability for Neural-Feedback-Loop Systems

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 22 references that are in the map.
- First posted on arXiv 6 May 2025.

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

- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances](https://mlsanity.com/paper/1709.07523/) (2017)
- [A Dual Approach to Scalable Verification of Deep Networks](https://mlsanity.com/paper/1803.06567/) (2018)
- [Reaching the Limit in Autonomous Racing: Optimal Control versus Reinforcement Learning](https://mlsanity.com/paper/2310.10943/) (2023)
- [Learning Robust Autonomous Navigation and Locomotion for Wheeled-Legged Robots](https://mlsanity.com/paper/2405.01792/) (2024)
- [Reachability Analysis of Neural Feedback Loops](https://mlsanity.com/paper/2108.04140/) (2021)
- [OVERT: An Algorithm for Safety Verification of Neural Network Control Policies for Nonlinear Systems](https://mlsanity.com/paper/2108.01220/) (2021)
- [Reachable Polyhedral Marching (RPM): A Safety Verification Algorithm for Robotic Systems with Deep Neural Network Components](https://mlsanity.com/paper/2011.11609/) (2020)
- [Backward Reachability Analysis of Neural Feedback Loops: Techniques for Linear and Nonlinear Systems](https://mlsanity.com/paper/2209.14076/) (2022)
- [PREMAP: A Unifying PREiMage APproximation Framework for Neural Networks](https://mlsanity.com/paper/2408.09262/) (2024)
- [MPCC++: Model Predictive Contouring Control for Time-Optimal Flight with Safety Constraints](https://mlsanity.com/paper/2403.17551/) (2024)
- [TTT: A Temporal Refinement Heuristic for Tenuously Tractable Discrete Time Reachability Problems](https://mlsanity.com/paper/2407.14394/) (2024)
- [Verifying Inverse Model Neural Networks](https://mlsanity.com/paper/2202.02429/) (2022)
- [Backward Reachability Analysis of Perturbed Continuous-Time Linear Systems Using Set Propagation](https://mlsanity.com/paper/2310.19083/) (2023)

## Built on by (most cited first, 2 of 2)

- [The FABRIC Strategy for Verifying Neural Feedback Systems](https://mlsanity.com/paper/2603.08964/) (2026)
- [A New Strategy for Verifying Reach-Avoid Specifications in Neural Feedback Systems](https://mlsanity.com/paper/2601.08065/) (2026)

## Abstract (arXiv)

Learning-enabled planning and control algorithms are increasingly popular, but they often lack rigorous guarantees of performance or safety. We introduce an algorithm for computing underapproximate backward reachable sets of nonlinear discrete time neural feedback loops. We then use the backward reachable sets to check goal-reaching properties. Our algorithm is based on overapproximating the system dynamics function to enable computation of underapproximate backward reachable sets through solutions of mixed-integer linear programs. We rigorously analyze the soundness of our algorithm and demonstrate it on a numerical example. Our work expands the class of properties that can be verified for learning-enabled systems.