Reference. Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers

Matthew Daggitt, Wen Kokke, Robert Atkey, Luca Arnaboldi, Ekaterina Komendantskya · arXiv · 2022 · machine-learning-verification · arXiv
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, although work has managed to incorporate the results of these verifiers to prove larger properties of individual systems, there is currently no general methodology for bridging the gap between verifiers and interactive theorem provers (ITPs). In this paper we present Vehicle, our solution to this problem. Vehicle is equipped with an expressive domain specific language for stating neural network specifications which can be compiled to both verifiers and ITPs. It overcomes previous issues with maintainability and scalability in similar ITP formalisations by using a standard ONNX file as the single canonical representation of the network. We demonstrate its utility by using it to connect the neural network verifier Marabou to Agda and then formally verifying that a car steered by a neural network never leaves the road, even in the face of an unpredictable cross wind and imperfect sensors. The network has over 20,000 nodes, and therefore this proof represents an improvement of 3 orders of magnitude over prior proofs about neural network enhanced systems in ITPs.

Cite
Cite as @daggitt-2022-vehicle (helia, typst) · \cite{daggitt-2022-vehicle} (LaTeX)
BibTeX
bibtex · 8 lines
@misc{daggitt-2022-vehicle,
  author = {Matthew Daggitt and Wen Kokke and Robert Atkey and Luca Arnaboldi and Ekaterina Komendantskya},
  title = {Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers},
  year = {2022},
  month = {2},
  eprint = {2202.05207},
  archiveprefix = {arXiv}
}
hayagriva YAML (typst)
yaml · 12 lines
daggitt-2022-vehicle:
  type: misc
  title: 'Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers'
  author:
  - Daggitt, Matthew
  - Kokke, Wen
  - Atkey, Robert
  - Arnaboldi, Luca
  - Komendantskya, Ekaterina
  date: 2022-02
  serial-number:
    arxiv: '2202.05207'
Download: daggitt-2022-vehicle.bib · daggitt-2022-vehicle.yml
Cites 28 works (1 here)
With notes (1)

Everybody’s Got To Be Somewhere mcbrideEverybodysGotToBeSomewhere2018MSFP · 2018
The key to any nameless representation of syntax is how it indicates the variables we choose to use and thus, implicitly, those we discard. Standard de Bruijn representations delay discarding maximally till the leaves of terms where one is chosen from the variables in scope at the expense of the rest. Consequently, introducing new but unused variables requires term traversal. This paper introduces a nameless ‘co-de-Bruijn’ representation which makes the opposite canonical choice, delaying discarding minimally, as near as possible to the root. It is literate Agda: dependent types make it a practical joy to express and be driven by strong intrinsic invariants which ensure that scope is aggressively whittled down to just the support of each subterm, in which every remaining variable occurs somewhere. The construction is generic, delivering a universe of syntaxes with higher-order metavariables, for which the appropriate notion of substitution is hereditary. The implementation of simultaneous substitution exploits tight scope control to avoid busywork and shift terms without traversal. Surprisingly, it is also intrinsically terminating, by structural recursion alone.
DOI
External (27)
daggitt-2022-vehicle reference entries/refs/daggitt-2022-vehicle/daggitt-2022-vehicle.hel