# Compiling High-Level Neural Network Specifications into VNN-LIB Queries

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 10 of its 28 references that are in the map.
- First posted on arXiv 24 Jan 2024.

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

- [An Introduction to Variational Autoencoders](https://mlsanity.com/paper/1906.02691/) (2019)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [Learning Student-Friendly Teacher Networks for Knowledge Distillation](https://mlsanity.com/paper/2102.07650/) (2021)
- [Certified Monotonic Neural Networks](https://mlsanity.com/paper/2011.10219/) (2020)
- [DNNV: A Framework for Deep Neural Network Verification](https://mlsanity.com/paper/2105.12841/) (2021)
- [Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs](https://mlsanity.com/paper/2401.06379/) (2024)
- [CAISAR: A platform for Characterizing Artificial Intelligence Safety and Robustness](https://mlsanity.com/paper/2206.03044/) (2022)
- [Towards a Certified Proof Checker for Deep Neural Network Verification](https://mlsanity.com/paper/2307.06299/) (2023)

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

- [Scaling LLM Test-Time Compute with Mobile NPU on Smartphones](https://mlsanity.com/paper/2509.23324/) (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)

## Abstract (arXiv)

The formal verification of traditional software has been revolutionised by verification-orientated languages such as Dafny and F* which enable developers to write high-level specifications that are automatically compiled down to low-level SMT-LIB queries. In contrast, neural network verification currently lacks such infrastructure, often requiring users to express requirements in formats close to the low-level VNN-LIB query format. This gap persists because targeting VNN-LIB presents unique algorithmic challenges when compared to targeting SMT-LIB: VNN-LIB is restricted to a fixed finite set of variables representing the input and outputs of the network, and even toy neural network specifications have an extremely large number of variables. In this paper, we present the first algorithm for compiling high-level neural network specifications into optimised VNN-LIB queries. Our algorithm is numerically sound and supports a far rich logical fragment than existing tools, including transformations of variables, first-class quantifiers, and specifications involving multiple networks or multiple applications of the same network. We implement this algorithm within the Vehicle framework and demonstrate that its performance is asymptotically optimal for benchmark specifications.