# Guaranteeing Safety for Neural Network-Based Aircraft Collision Avoidance Systems

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

## Key facts

- Cited by 26 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 15 Dec 2019.

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

- [Certified Patch Robustness via Smoothed Vision Transformers](https://mlsanity.com/paper/2110.07719/) (2021)
- [How to Certify Machine Learning Based Safety-critical Systems? A Systematic Literature Review](https://mlsanity.com/paper/2107.12045/) (2021)
- [A Survey on Knowledge Editing of Neural Networks](https://mlsanity.com/paper/2310.19704/) (2023)
- [Verification of Image-based Neural Network Controllers Using Generative Models](https://mlsanity.com/paper/2105.07091/) (2021)
- [Neural Network Repair with Reachability Analysis](https://mlsanity.com/paper/2108.04214/) (2021)
- [Sound and Complete Neural Network Repair with Minimality and Locality Guarantees](https://mlsanity.com/paper/2110.07682/) (2021)
- [Neural Network Compression of ACAS Xu Early Prototype is Unsafe: Closed-Loop Verification through Quantized State Backreachability](https://mlsanity.com/paper/2201.06626/) (2022)
- [Scalable Surrogate Verification of Image-based Neural Network Control Systems using Composition and Unrolling](https://mlsanity.com/paper/2405.18554/) (2024)
- [Verifying Low-dimensional Input Neural Networks via Input Quantization](https://mlsanity.com/paper/2108.07961/) (2021)
- [Adversarial Robustness Certification for Bayesian Neural Networks](https://mlsanity.com/paper/2306.13614/) (2023)
- [Provably Safe Neural Network Controllers via Differential Dynamic Logic](https://mlsanity.com/paper/2402.10998/) (2024)
- [Discovering Closed-Loop Failures of Vision-Based Controllers via Reachability Analysis](https://mlsanity.com/paper/2211.02736/) (2022)
- [Generating Probabilistic Safety Guarantees for Neural Network Controllers](https://mlsanity.com/paper/2103.01203/) (2021)
- [AVOIDDS: Aircraft Vision-based Intruder Detection Dataset and Simulator](https://mlsanity.com/paper/2306.11203/) (2023)
- [Solving Probabilistic Verification Problems of Neural Networks using Branch and Bound](https://mlsanity.com/paper/2405.17556/) (2024)
- [A Robust Optimisation Perspective on Counterexample-Guided Repair of Neural Networks](https://mlsanity.com/paper/2301.11342/) (2023)
- [Scaling up Memory-Efficient Formal Verification Tools for Tree Ensembles](https://mlsanity.com/paper/2105.02595/) (2021)
- [Abstract Interpretation of Fixpoint Iterators with Applications to Neural Networks](https://mlsanity.com/paper/2110.08260/) (2021)
- [Defining Operational Conditions for Safety-Critical AI-Based Systems from Data](https://mlsanity.com/paper/2601.22118/) (2026)
- [From High-Dimensional Spaces to Verifiable ODD Coverage for Safety-Critical AI-based Systems](https://mlsanity.com/paper/2604.02198/) (2026)
- [Evolution of Natural Language Processing Technology: Not Just Language Processing Towards General Purpose AI](https://mlsanity.com/paper/2310.06228/) (2023)
- [Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision](https://mlsanity.com/paper/2507.22760/) (2025)
- [Aircraft Collision Avoidance Systems: Technological Challenges and Solutions on the Path to Regulatory Acceptance](https://mlsanity.com/paper/2510.20916/) (2025)
- [On the Applicability of Safety Nets: A Safety-By-Design Solution for Certifying Neural Networks](https://mlsanity.com/paper/2608.20053/) (2026)
- [Coverage-Driven Verification for Safety-by-Design in AI-Based Collision Avoidance Systems](https://mlsanity.com/paper/2608.20864/) (2026)
- [Stochastic World Models for Verifying Vision-Based Neural Feedback Systems](https://mlsanity.com/paper/2609.38120/) (2026)

## Abstract (arXiv)

The decision logic for the ACAS X family of aircraft collision avoidance systems is represented as a large numeric table. Due to storage constraints of certified avionics hardware, neural networks have been suggested as a way to significantly compress the data while still preserving performance in terms of safety. However, neural networks are complex continuous functions with outputs that are difficult to predict. Because simulations evaluate only a finite number of encounters, simulations are not sufficient to guarantee that the neural network will perform correctly in all possible situations. We propose a method to provide safety guarantees when using a neural network collision avoidance system. The neural network outputs are bounded using neural network verification tools like Reluplex and Reluval, and a reachability method determines all possible ways aircraft encounters will resolve using neural network advisories and assuming bounded aircraft dynamics. Experiments with systems inspired by ACAS X show that neural networks giving either horizontal or vertical maneuvers can be proven safe. We explore how relaxing the bounds on aircraft dynamics can lead to potentially unsafe encounters and demonstrate how neural network controllers can be modified to guarantee safety through online costs or lowering alerting cost. The reachability method is flexible and can incorporate uncertainties such as pilot delay and sensor error. These results suggest a method for certifying neural network collision avoidance systems for use in real aircraft.