# Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs

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

## Key facts

- Cited by 14 papers in the map (data through 14 Oct 2026).
- Builds on 27 of its 80 references that are in the map.
- First posted on arXiv 12 Jan 2024.

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

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Florence: A New Foundation Model for Computer Vision](https://mlsanity.com/paper/2111.11432/) (2021)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Self-Driving Cars: A Survey](https://mlsanity.com/paper/1901.04407/) (2019)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Analyzing Differentiable Fuzzy Logic Operators](https://mlsanity.com/paper/2002.06100/) (2020)
- [Neural Lander: Stable Drone Landing Control using Learned Dynamics](https://mlsanity.com/paper/1811.08027/) (2018)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [Scenic: A Language for Scenario Specification and Scene Generation](https://mlsanity.com/paper/1809.09310/) (2018)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [Incorporating Domain Knowledge into Deep Neural Networks](https://mlsanity.com/paper/2103.00180/) (2021)
- [Deep Learning with Logical Constraints](https://mlsanity.com/paper/2205.00523/) (2022)
- [POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems](https://mlsanity.com/paper/2106.13867/) (2021)
- [Certified Reinforcement Learning with Logic Guidance](https://mlsanity.com/paper/1902.00778/) (2019)
- [Exploiting Verified Neural Networks via Floating Point Numerical Error](https://mlsanity.com/paper/2003.03021/) (2020)
- [Neural Network Robustness as a Verification Property: A Principled Case Study](https://mlsanity.com/paper/2104.01396/) (2021)
- [JuliaReach: a Toolbox for Set-Based Reachability](https://mlsanity.com/paper/1901.10736/) (2019)
- [Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes](https://mlsanity.com/paper/2207.02715/) (2022)
- [DNNV: A Framework for Deep Neural Network Verification](https://mlsanity.com/paper/2105.12841/) (2021)
- [Verifying Controllers with Convolutional Neural Network-based Perception: A Case for Intelligible, Safe, and Precise Abstractions](https://mlsanity.com/paper/2111.05534/) (2021)
- [Closed-loop Analysis of Vision-based Autonomous Systems: A Case Study](https://mlsanity.com/paper/2302.04634/) (2023)
- [Logic of Differentiable Logics: Towards a Uniform Semantics of DL](https://mlsanity.com/paper/2303.10650/) (2023)
- [CAISAR: A platform for Characterizing Artificial Intelligence Safety and Robustness](https://mlsanity.com/paper/2206.03044/) (2022)
- [CheckINN: Wide Range Neural Network Verification in Imandra (Extended)](https://mlsanity.com/paper/2207.10562/) (2022)
- [Measure Construction by Extension in Dependent Type Theory with Application to Integration](https://mlsanity.com/paper/2209.02345/) (2022)
- [Comparing Differentiable Logics for Learning Systems: A Research Preview](https://mlsanity.com/paper/2311.09809/) (2023)

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

- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Neuro-Symbolic AI: Explainability, Challenges, and Future Trends](https://mlsanity.com/paper/2411.04383/) (2024)
- [A Certified Proof Checker for Deep Neural Network Verification in Imandra](https://mlsanity.com/paper/2405.10611/) (2024)
- [Compiling High-Level Neural Network Specifications into VNN-LIB Queries](https://mlsanity.com/paper/2402.01353/) (2024)
- [RepV: Safety-Separable Latent Spaces for Scalable Neurosymbolic Plan Verification](https://mlsanity.com/paper/2510.26935/) (2025)
- [A Scalable Approach to Probabilistic Neuro-Symbolic Robustness Verification](https://mlsanity.com/paper/2502.03274/) (2025)
- [Proof-Carrying Neuro-Symbolic Code](https://mlsanity.com/paper/2504.12031/) (2025)
- [A General Framework for Property-Driven Machine Learning](https://mlsanity.com/paper/2505.00466/) (2025)
- [VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification](https://mlsanity.com/paper/2605.07451/) (2026)
- [A Neurosymbolic Framework for Bias Correction in Convolutional Neural Networks](https://mlsanity.com/paper/2405.15886/) (2024)
- [Bridging the Gap: Representation Spaces in Neuro-Symbolic AI](https://mlsanity.com/paper/2411.04393/) (2024)
- [The CAISAR Platform: Extending the Reach of Machine Learning Specification and Verification](https://mlsanity.com/paper/2506.12084/) (2025)
- [Quantitative Linear Logic for Neuro-Symbolic Learning and Verification](https://mlsanity.com/paper/2605.13845/) (2026)

## Abstract (arXiv)

Neuro-symbolic programs, i.e. programs containing both machine learning components and traditional symbolic code, are becoming increasingly widespread. Finding a general methodology for verifying such programs is challenging due to both the number of different tools involved and the intricate interface between the ``neural'' and ``symbolic'' program components. In this paper we present a general decomposition of the neuro-symbolic verification problem into parts, and examine the problem of the embedding gap that occurs when one tries to combine proofs about the neural and symbolic components. To address this problem we then introduce Vehicle -- standing as an abbreviation for a ``verification condition language'' -- an intermediate programming language interface between machine learning frameworks, automated theorem provers, and dependently-typed formalisations of neuro-symbolic programs. Vehicle allows users to specify the properties of the neural components of neuro-symbolic programs once, and then safely compile the specification to each interface using a tailored typing and compilation procedure. We give a high-level overview of Vehicle's overall design, its interfaces and compilation & type-checking procedures, and then demonstrate its utility by formally verifying the safety of a simple autonomous car controlled by a neural network, operating in a stochastic environment with imperfect information.