Abstracts.2021.ML.Verification
by Matthew Daggit
Verification of neural networks is currently a hot topic in automated theorem proving. Progress has been rapid and there are now a wide range of tools available that can verify properties of networks with hundreds of thousands of nodes. In theory this opens the door to the verification of larger control systems that make use of neural network components. However, there is currently no general methodology for bridging the gap between verifiers and interactive theorem provers that could be used to construct these larger proofs.
In this talk I will present Vehicle, a dependently typed domain-specific language for formalising properties of black-box neural network components. The Vehicle compiler translates specifications down to problems for the neural network verifier Marabou, before automatically generating a file containing an Agda version of the spec. Proofs about the larger system may then be built on top of this Agda interface. I will demonstrate the methodology by proving that a simple neural-network enhanced car controller will always stay on the road.
Zoom recording was lost, but a similar talk was given a few weeks later at the Herriot-Watt University LAIV Seminar, visible here.
- Matthew L. Daggitt, Wen Kokke, Robert Atkey, Luca Arnaboldi, Ekaterina Komendantskya. 2022. Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers.