# Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers

arXiv: https://arxiv.org/abs/2202.05207 · HTML: https://mlsanity.com/paper/2202.05207/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 28 references that are in the map.
- First posted on arXiv 10 Feb 2022.

## Builds on (most cited first, 12 of 12)

- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Knowledge Distillation: A Survey](https://mlsanity.com/paper/2006.05525/) (2020)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Unconstrained Monotonic Neural Networks](https://mlsanity.com/paper/1908.05164/) (2019)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks](https://mlsanity.com/paper/1708.03322/) (2017)
- [Exploiting Verified Neural Networks via Floating Point Numerical Error](https://mlsanity.com/paper/2003.03021/) (2020)
- [DNNV: A Framework for Deep Neural Network Verification](https://mlsanity.com/paper/2105.12841/) (2021)
- [Case Study: Verifying the Safety of an Autonomous Racing Car with a Neural Network Controller](https://mlsanity.com/paper/1910.11309/) (2019)
- [Everybody's Got To Be Somewhere](https://mlsanity.com/paper/1807.04085/) (2018)

## Built on by (most cited first, 5 of 5)

- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Provably Safe Neural Network Controllers via Differential Dynamic Logic](https://mlsanity.com/paper/2402.10998/) (2024)
- [Towards a Certified Proof Checker for Deep Neural Network Verification](https://mlsanity.com/paper/2307.06299/) (2023)
- [A General Framework for Property-Driven Machine Learning](https://mlsanity.com/paper/2505.00466/) (2025)
- [The CAISAR Platform: Extending the Reach of Machine Learning Specification and Verification](https://mlsanity.com/paper/2506.12084/) (2025)

## Abstract (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.