Machine learning components, such as neural networks, gradually make their way into software; and, when the software is critically safe, the machine learning components must be verifiably safe. This gives rise to the problem of neural network verification. The community has been making rapid progress in methods for incorporating logical specifications into neural networks, both in training and verification. However, to truly unlock the ability to verify real-world neural network-enhanced systems we believe the following is necessary.

• The specification of neural network properties should be written once and should automatically work with training and verification tools.
• The specification should be written in a manner independent of any particular neural network training/inference platform.
• The specification should be able to be written as a high-level property over the problem space, rather than a property over the embedding space.
• After verification the specification should be exportable to general interactive theorem provers so that its proof can be incorporated into proofs about the larger system around the neural network.

In this tutorial we will present Vehicle, a functional (Haskell-based) DSL that allows users to do all of this. We will provide an introduction to the Vehicle specification language and type system, and then walk attendees through using it to express a variety of famous and not-so-famous specifications. Subsequently we demonstrate how a specification can be compiled down to i) Tensorflow graphs to be used as loss functions during training, ii) queries for network verifiers, and iii) cross-compiled to Agda. Finally we will discuss some of the technical challenges in the implementation as well as some of the outstanding problems.

The tutorial will come with an exercise session. Attendees are encouraged to check the pre-requisites for Vehicle here: https://vehicle-lang.github.io/tutorial/#prerequisites