# Creating a Formally Verified Neural Network for Autonomous Navigation: An Experience Report

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 23 of its 47 references that are in the map.
- First posted on arXiv 21 Nov 2024.

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

- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [GradNorm: Gradient Normalization for Adaptive Loss Balancing in Deep Multitask Networks](https://mlsanity.com/paper/1711.02257/) (2017)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Analyzing Differentiable Fuzzy Logic Operators](https://mlsanity.com/paper/2002.06100/) (2020)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [Neural Network Verification with Branch-and-Bound for General Nonlinearities](https://mlsanity.com/paper/2405.21063/) (2024)
- [Deep Learning with Logical Constraints](https://mlsanity.com/paper/2205.00523/) (2022)
- [Formal Verification of Neural Network Controlled Autonomous Systems](https://mlsanity.com/paper/1810.13072/) (2018)
- [The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Results](https://mlsanity.com/paper/2212.10376/) (2022)
- [The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results](https://mlsanity.com/paper/2312.16760/) (2023)
- [Neural Network Robustness as a Verification Property: A Principled Case Study](https://mlsanity.com/paper/2104.01396/) (2021)
- [Provably Bounding Neural Network Preimages](https://mlsanity.com/paper/2302.01404/) (2023)
- [DNNV: A Framework for Deep Neural Network Verification](https://mlsanity.com/paper/2105.12841/) (2021)
- [Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI](https://mlsanity.com/paper/2005.07173/) (2020)
- [Case Study: Verifying the Safety of an Autonomous Racing Car with a Neural Network Controller](https://mlsanity.com/paper/1910.11309/) (2019)
- [Logic of Differentiable Logics: Towards a Uniform Semantics of DL](https://mlsanity.com/paper/2303.10650/) (2023)
- [Comparing differentiable logics for learning with logical constraints](https://mlsanity.com/paper/2407.03847/) (2024)
- [Risk Verification of Stochastic Systems with Neural Network Controllers](https://mlsanity.com/paper/2209.09881/) (2022)

## Abstract (arXiv)

The increased reliance of self-driving vehicles on neural networks opens up the challenge of their verification. In this paper we present an experience report, describing a case study which we undertook to explore the design and training of a neural network on a custom dataset for vision-based autonomous navigation. We are particularly interested in the use of machine learning with differentiable logics to obtain networks satisfying basic safety properties by design, guaranteeing the behaviour of the neural network after training. We motivate the choice of a suitable neural network verifier for our purposes and report our observations on the use of neural network verifiers for self-driving systems.