# Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI

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

## Key facts

- Cited by 21 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 May 2020.

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

- [Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems](https://mlsanity.com/paper/2405.06624/) (2024)
- [How to Certify Machine Learning Based Safety-critical Systems? A Systematic Literature Review](https://mlsanity.com/paper/2107.12045/) (2021)
- [Towards quantum enhanced adversarial robustness in machine learning](https://mlsanity.com/paper/2306.12688/) (2023)
- [Neural Network Verification with Proof Production](https://mlsanity.com/paper/2206.00512/) (2022)
- [NNLander-VeriF: A Neural Network Formal Verification Framework for Vision-Based Autonomous Aircraft Landing](https://mlsanity.com/paper/2203.15841/) (2022)
- [Joint Differentiable Optimization and Verification for Certified Reinforcement Learning](https://mlsanity.com/paper/2201.12243/) (2022)
- [Parallel and Multi-Objective Falsification with Scenic and VerifAI](https://mlsanity.com/paper/2107.04164/) (2021)
- [A Scenario-Based Platform for Testing Autonomous Vehicle Behavior Prediction Models in Simulation](https://mlsanity.com/paper/2110.14870/) (2021)
- [Toward Certification of Machine-Learning Systems for Low Criticality Airborne Applications](https://mlsanity.com/paper/2209.13975/) (2022)
- [Addressing the IEEE AV Test Challenge with Scenic and VerifAI](https://mlsanity.com/paper/2108.13796/) (2021)
- [BERN-NN: Tight Bound Propagation For Neural Networks Using Bernstein Polynomial Interval Arithmetic](https://mlsanity.com/paper/2211.14438/) (2022)
- [Synthesizing Pareto-Optimal Interpretations for Black-Box Models](https://mlsanity.com/paper/2108.07307/) (2021)
- [Scenario-based Compositional Verification of Autonomous Systems with Neural Perception](https://mlsanity.com/paper/2504.20942/) (2025)
- [Conformal Safety Shielding for Imperfect-Perception Agents](https://mlsanity.com/paper/2506.17275/) (2025)
- [AssistTaxi: A Comprehensive Dataset for Taxiway Analysis and Autonomous Operations](https://mlsanity.com/paper/2409.06856/) (2024)
- [Learning Contextual Runtime Monitors for Safe AI-Based Autonomy](https://mlsanity.com/paper/2601.20666/) (2026)
- [Creating a Formally Verified Neural Network for Autonomous Navigation: An Experience Report](https://mlsanity.com/paper/2411.14163/) (2024)
- [Incorporating System-level Safety Requirements in Perception Models via Reinforcement Learning](https://mlsanity.com/paper/2412.02951/) (2024)
- [Locally Pareto-Optimal Interpretations for Black-Box Machine Learning Models](https://mlsanity.com/paper/2508.15220/) (2025)
- [Interval POMDP Shielding for Imperfect-Perception Agents](https://mlsanity.com/paper/2604.20728/) (2026)
- [Diffusion-Guided Search via Exponential Tilting (DiffTilt): An Application to Falsification of Safety-Critical Systems](https://mlsanity.com/paper/2607.23134/) (2026)

## Abstract (arXiv)

We demonstrate a unified approach to rigorous design of safety-critical autonomous systems using the VerifAI toolkit for formal analysis of AI-based systems. VerifAI provides an integrated toolchain for tasks spanning the design process, including modeling, falsification, debugging, and ML component retraining. We evaluate all of these applications in an industrial case study on an experimental autonomous aircraft taxiing system developed by Boeing, which uses a neural network to track the centerline of a runway. We define runway scenarios using the Scenic probabilistic programming language, and use them to drive tests in the X-Plane flight simulator. We first perform falsification, automatically finding environment conditions causing the system to violate its specification by deviating significantly from the centerline (or even leaving the runway entirely). Next, we use counterexample analysis to identify distinct failure cases, and confirm their root causes with specialized testing. Finally, we use the results of falsification and debugging to retrain the network, eliminating several failure cases and improving the overall performance of the closed-loop system.