# QEBVerif: Quantization Error Bound Verification of Neural Networks

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

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- Builds on 46 of its 83 references that are in the map.
- First posted on arXiv 6 Dec 2022.

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

- [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)
- [Quantization and Training of Neural Networks for Efficient Integer-Arithmetic-Only Inference](https://mlsanity.com/paper/1712.05877/) (2017)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Up or Down? Adaptive Rounding for Post-Training Quantization](https://mlsanity.com/paper/2004.10568/) (2020)
- [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)
- [LQ-Nets: Learned Quantization for Highly Accurate and Compact Deep Neural Networks](https://mlsanity.com/paper/1807.10029/) (2018)
- [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)
- [Differentiable Soft Quantization: Bridging Full-Precision and Low-Bit Neural Networks](https://mlsanity.com/paper/1908.05033/) (2019)
- [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)
- [Learning to Quantize Deep Networks by Optimizing Quantization Intervals with Task Loss](https://mlsanity.com/paper/1808.05779/) (2018)
- [Fixed Point Quantization of Deep Convolutional Networks](https://mlsanity.com/paper/1511.06393/) (2015)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [Defensive Quantization: When Efficiency Meets Robustness](https://mlsanity.com/paper/1904.08444/) (2019)
- [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)
- [Deep Neural Network Compression for Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1810.04240/) (2018)
- [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)
- [Scalable Quantitative Verification For Deep Neural Networks](https://mlsanity.com/paper/2002.06864/) (2020)

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

- [Logic for Explainable AI](https://mlsanity.com/paper/2305.05172/) (2023)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [QGen: On the Ability to Generalize in Quantization Aware Training](https://mlsanity.com/paper/2404.11769/) (2024)
- [Revisiting Differential Verification: Equivalence Verification with Confidence](https://mlsanity.com/paper/2410.20207/) (2024)
- [Quantization Robustness of Monotone Operator Equilibrium Networks](https://mlsanity.com/paper/2603.10562/) (2026)
- [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)
- [SimCert: Probabilistic Certification for Behavioral Similarity in Deep Neural Network Compression](https://mlsanity.com/paper/2603.14818/) (2026)
- [An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks](https://mlsanity.com/paper/2307.15907/) (2023)

## Abstract (arXiv)

To alleviate the practical constraints for deploying deep neural networks (DNNs) on edge devices, quantization is widely regarded as one promising technique. It reduces the resource requirements for computational power and storage space by quantizing the weights and/or activation tensors of a DNN into lower bit-width fixed-point numbers, resulting in quantized neural networks (QNNs). While it has been empirically shown to introduce minor accuracy loss, critical verified properties of a DNN might become invalid once quantized. Existing verification methods focus on either individual neural networks (DNNs or QNNs) or quantization error bound for partial quantization. In this work, we propose a quantization error bound verification method, named QEBVerif, where both weights and activation tensors are quantized. QEBVerif consists of two parts, i.e., a differential reachability analysis (DRA) and a mixed-integer linear programming (MILP) based verification method. DRA performs difference analysis between the DNN and its quantized counterpart layer-by-layer to compute a tight quantization error interval efficiently. If DRA fails to prove the error bound, then we encode the verification problem into an equivalent MILP problem which can be solved by off-the-shelf solvers. Thus, QEBVerif is sound, complete, and reasonably efficient. We implement QEBVerif and conduct extensive experiments, showing its effectiveness and efficiency.