# Constraint-Aware Refinement for Safety Verification of Neural Feedback Loops

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 18 references that are in the map.
- First posted on arXiv 30 Sep 2024.

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

- [Concrete Problems in AI Safety](https://mlsanity.com/paper/1606.06565/) (2016)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Adversarial Examples: Attacks and Defenses for Deep Learning](https://mlsanity.com/paper/1712.07107/) (2017)
- [DeepDriving: Learning Affordance for Direct Perception in Autonomous Driving](https://mlsanity.com/paper/1505.00256/) (2015)
- [Neural Lander: Stable Drone Landing Control using Learned Dynamics](https://mlsanity.com/paper/1811.08027/) (2018)
- [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)
- [Backward Reachability Analysis of Neural Feedback Loops: Techniques for Linear and Nonlinear Systems](https://mlsanity.com/paper/2209.14076/) (2022)
- [One-Shot Reachability Analysis of Neural Network Dynamical Systems](https://mlsanity.com/paper/2209.11827/) (2022)
- [A Hybrid Partitioning Strategy for Backward Reachability of Neural Feedback Loops](https://mlsanity.com/paper/2210.07918/) (2022)
- [Specification-Guided Safety Verification for Feedforward Neural Networks](https://mlsanity.com/paper/1812.06161/) (2018)
- [TTT: A Temporal Refinement Heuristic for Tenuously Tractable Discrete Time Reachability Problems](https://mlsanity.com/paper/2407.14394/) (2024)

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

- [Formal Safety Verification and Refinement for Generative Motion Planners via Certified Local Stabilization](https://mlsanity.com/paper/2509.19688/) (2025)
- [Learning Verifiable Control Policies Using Relaxed Verification](https://mlsanity.com/paper/2504.16879/) (2025)
- [Scalable Data-Driven Reachability Analysis and Control via Koopman Operators with Conformal Coverage Guarantees](https://mlsanity.com/paper/2601.01076/) (2026)
- [Stochastic World Models for Verifying Vision-Based Neural Feedback Systems](https://mlsanity.com/paper/2609.38120/) (2026)

## Abstract (arXiv)

Neural networks (NNs) are becoming increasingly popular in the design of control pipelines for autonomous systems. However, since the performance of NNs can degrade in the presence of out-of-distribution data or adversarial attacks, systems that have NNs in their control pipelines, i.e., neural feedback loops (NFLs), need safety assurances before they can be applied in safety-critical situations. Reachability analysis offers a solution to this problem by calculating reachable sets that bound the possible future states of an NFL and can be checked against dangerous regions of the state space to verify that the system does not violate safety constraints. Since exact reachable sets are generally intractable to calculate, reachable set over approximations (RSOAs) are typically used. The problem with RSOAs is that they can be overly conservative, making it difficult to verify the satisfaction of safety constraints, especially over long time horizons or for highly nonlinear NN control policies. Refinement strategies such as partitioning or symbolic propagation are typically used to limit the conservativeness of RSOAs, but these approaches come with a high computational cost and often can only be used to verify safety for simple reachability problems. This paper presents Constraint-Aware Refinement for Verification (CARV): an efficient refinement strategy that reduces the conservativeness of RSOAs by explicitly using the safety constraints on the NFL to refine RSOAs only where necessary. We demonstrate that CARV can verify the safety of an NFL where other approaches either fail or take up to 60x longer and 40x the memory.