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

TL;DR

This paper presents an experience report, describing a case study which was undertook to explore the design and training of a neural network on a custom dataset for vision-based autonomous navigation, and motivates the choice of a suitable neural network verifier.

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.

Figures (6)

• Figure 1: Differentiable logics allow for the use of logical constraints during training by translating them into additional loss terms. Note that in this paper, we do not use continuous verification, that is, we do not re-train the network after the verification; instead, we only try to evaluate what influence training with logical constraints has on the verification afterwards.
• Figure 2: Samples from the LEGO road dataset showing various lighting conditions and track configurations. The red dots located at label coordinates show the centre of the path to be followed in the frame.
• Figure 3: The proposed neural network architecture for extracting the path centre in an input image of size $112\times 112$ pixels.
• Figure 4: Comparison of predictions of models trained without (vanilla) and with logical constraints (constrained-training) on an adversarial example in epoch 45 of 100.
• Figure 5: The prediction loss (i.e., mean squared error; lower is better) and constraint accuracy (higher is better) for a model trained only on data (vanilla) and a model trained on both data and logical constraints with differentiable logics (constrained-training).