# QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks

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

## Key facts

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

## Builds on (most cited first, 30 of 50)

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [EfficientNet: Rethinking Model Scaling for Convolutional Neural Networks](https://mlsanity.com/paper/1905.11946/) (2019)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Fashion-MNIST: a Novel Image Dataset for Benchmarking Machine Learning Algorithms](https://mlsanity.com/paper/1708.07747/) (2017)
- [Towards Evaluating the Robustness of Neural Networks](https://mlsanity.com/paper/1608.04644/) (2016)
- [Deep Compression: Compressing Deep Neural Networks with Pruning, Trained Quantization and Huffman Coding](https://mlsanity.com/paper/1510.00149/) (2015)
- [Adversarial examples in the physical world](https://mlsanity.com/paper/1607.02533/) (2016)
- [Quantization and Training of Neural Networks for Efficient Integer-Arithmetic-Only Inference](https://mlsanity.com/paper/1712.05877/) (2017)
- [The Limitations of Deep Learning in Adversarial Settings](https://mlsanity.com/paper/1511.07528/) (2015)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [A White Paper on Neural Network Quantization](https://mlsanity.com/paper/2106.08295/) (2021)
- [DeepXplore: Automated Whitebox Testing of Deep Learning Systems](https://mlsanity.com/paper/1705.06640/) (2017)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [DeepTest: Automated Testing of Deep-Neural-Network-driven Autonomous Cars](https://mlsanity.com/paper/1708.08559/) (2017)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Machine Learning Testing: Survey, Landscapes and Horizons](https://mlsanity.com/paper/1906.10742/) (2019)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [DeepGauge: Multi-Granularity Testing Criteria for Deep Learning Systems](https://mlsanity.com/paper/1803.07519/) (2018)
- [Maximum Resilience of Artificial Neural Networks](https://mlsanity.com/paper/1705.01040/) (2017)
- [Verifying Properties of Binarized Deep Neural Networks](https://mlsanity.com/paper/1709.06662/) (2017)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [TensorFuzz: Debugging Neural Networks with Coverage-Guided Fuzzing](https://mlsanity.com/paper/1807.10875/) (2018)
- [An Abstraction-Based Framework for Neural Network Verification](https://mlsanity.com/paper/1910.14574/) (2019)
- [Who is Real Bob? Adversarial Attacks on Speaker Recognition Systems](https://mlsanity.com/paper/1911.01840/) (2019)
- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [A Statistical Approach to Assessing Neural Network Robustness](https://mlsanity.com/paper/1811.07209/) (2018)
- [Concolic Testing for Deep Neural Networks](https://mlsanity.com/paper/1805.00089/) (2018)
- [An SMT-Based Approach for Verifying Binarized Neural Networks](https://mlsanity.com/paper/2011.02948/) (2020)
- [Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness](https://mlsanity.com/paper/1904.09959/) (2019)
- [Efficient Exact Verification of Binarized Neural Networks](https://mlsanity.com/paper/2005.03597/) (2020)

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

- [Logic for Explainable AI](https://mlsanity.com/paper/2305.05172/) (2023)
- [A Survey of Neural Network Robustness Assessment in Image Recognition](https://mlsanity.com/paper/2404.08285/) (2024)
- [Verifying Quantized Graph Neural Networks is PSPACE-complete](https://mlsanity.com/paper/2502.16244/) (2025)
- [Verification of Bit-Flip Attacks against Quantized Neural Networks](https://mlsanity.com/paper/2502.16286/) (2025)
- [Training Verification-Friendly Neural Networks via Neuron Behavior Consistency](https://mlsanity.com/paper/2412.13229/) (2024)
- [Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exits](https://mlsanity.com/paper/2512.20755/) (2025)
- [QNNRepair: Quantized Neural Network Repair](https://mlsanity.com/paper/2306.13793/) (2023)
- [An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks](https://mlsanity.com/paper/2307.15907/) (2023)
- [Efficient DNN-Powered Software with Fair Sparse Models](https://mlsanity.com/paper/2407.02805/) (2024)
- [Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision](https://mlsanity.com/paper/2507.22760/) (2025)
- [Exact and Asymptotically Complete Robust Verifications of Neural Networks via Ising Solvers](https://mlsanity.com/paper/2603.00408/) (2026)
- [SoK: Formal Methods for Fact-Checking and Information Integrity](https://mlsanity.com/paper/2609.23239/) (2026)

## Abstract (arXiv)

Deep learning has become a promising programming paradigm in software development, owing to its surprising performance in solving many challenging tasks. Deep neural networks (DNNs) are increasingly being deployed in practice, but are limited on resource-constrained devices owing to their demand for computational power. Quantization has emerged as a promising technique to reduce the size of DNNs with comparable accuracy as their floating-point numbered counterparts. The resulting quantized neural networks (QNNs) can be implemented energy-efficiently. Similar to their floating-point numbered counterparts, quality assurance techniques for QNNs, such as testing and formal verification, are essential but are currently less explored. In this work, we propose a novel and efficient formal verification approach for QNNs. In particular, we are the first to propose an encoding that reduces the verification problem of QNNs into the solving of integer linear constraints, which can be solved using off-the-shelf solvers. Our encoding is both sound and complete. We demonstrate the application of our approach on local robustness verification and maximum robustness radius computation. We implement our approach in a prototype tool QVIP and conduct a thorough evaluation. Experimental results on QNNs with different quantization bits confirm the effectiveness and efficiency of our approach, e.g., two orders of magnitude faster and able to solve more verification tasks in the same time limit than the state-of-the-art methods.