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

TL;DR

This paper reports on a case study of designing and training a neural network for autonomous navigation, emphasizing the use of differentiable logics and neural network verifiers to ensure safety properties by design.

Contribution

It demonstrates the application of differentiable logics and verification techniques to create neural networks with safety guarantees for autonomous vehicles.

Findings

Neural networks can be trained with safety properties in mind.

Neural network verifiers are useful for self-driving system safety.

Design choices impact the verifiability of neural networks.

Abstract

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.