Skip to content

Abstracts.2021.ML.Verification

Jump to bottom
Fabian edited this page Feb 15, 2022 · 7 revisions

Interfacing neural network verifiers with interactive theorem provers

by Matthew Daggit

Abstract

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.

Bibliography

Clone this wiki locally