# Neural Network Compression of ACAS Xu Early Prototype is Unsafe: Closed-Loop Verification through Quantized State Backreachability

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 34 references that are in the map.
- First posted on arXiv 17 Jan 2022.

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

- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [Deep Neural Network Compression for Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1810.04240/) (2018)
- [Guaranteeing Safety for Neural Network-Based Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1912.07084/) (2019)
- [Safety Verification of Neural Network Controlled Systems](https://mlsanity.com/paper/2011.05174/) (2020)
- [Verifying Low-dimensional Input Neural Networks via Input Quantization](https://mlsanity.com/paper/2108.07961/) (2021)
- [Linear Encodings for Polytope Containment Problems](https://mlsanity.com/paper/1903.05214/) (2019)
- [Numerical Verification of Affine Systems with up to a Billion Dimensions](https://mlsanity.com/paper/1804.01583/) (2018)

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

- [Backward Reachability Analysis of Neural Feedback Loops: Techniques for Linear and Nonlinear Systems](https://mlsanity.com/paper/2209.14076/) (2022)
- [Provably Safe Neural Network Controllers via Differential Dynamic Logic](https://mlsanity.com/paper/2402.10998/) (2024)
- [DRIP: Domain Refinement Iteration with Polytopes for Backward Reachability Analysis of Neural Feedback Loops](https://mlsanity.com/paper/2212.04646/) (2022)
- [Predictive Uncertainty for Runtime Assurance of a Real-Time Computer Vision-Based Landing System](https://mlsanity.com/paper/2508.09732/) (2025)
- [AutoSpec: Automated Generation of Neural Network Specifications](https://mlsanity.com/paper/2409.10897/) (2024)
- [Learning Verifiable Control Policies Using Relaxed Verification](https://mlsanity.com/paper/2504.16879/) (2025)
- [The inverse problem for neural networks](https://mlsanity.com/paper/2308.14093/) (2023)
- [Verification of Visual Controllers via Compositional Geometric Transformations](https://mlsanity.com/paper/2507.04523/) (2025)

## Abstract (arXiv)

ACAS Xu is an air-to-air collision avoidance system designed for unmanned aircraft that issues horizontal turn advisories to avoid an intruder aircraft. Due the use of a large lookup table in the design, a neural network compression of the policy was proposed. Analysis of this system has spurred a significant body of research in the formal methods community on neural network verification. While many powerful methods have been developed, most work focuses on open-loop properties of the networks, rather than the main point of the system -- collision avoidance -- which requires closed-loop analysis. In this work, we develop a technique to verify a closed-loop approximation of the system using state quantization and backreachability. We use favorable assumptions for the analysis -- perfect sensor information, instant following of advisories, ideal aircraft maneuvers and an intruder that only flies straight. When the method fails to prove the system is safe, we refine the quantization parameters until generating counterexamples where the original (non-quantized) system also has collisions.