# Scalable Verification of Quantized Neural Networks (Technical Report)

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

## Key facts

- Cited by 28 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 15 Dec 2020.

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

- [Logic for Explainable AI](https://mlsanity.com/paper/2305.05172/) (2023)
- [BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks](https://mlsanity.com/paper/2103.07224/) (2021)
- [Neural Termination Analysis](https://mlsanity.com/paper/2102.03824/) (2021)
- [Infinite Time Horizon Safety of Bayesian Neural Networks](https://mlsanity.com/paper/2111.03165/) (2021)
- [GoTube: Scalable Stochastic Verification of Continuous-Depth Models](https://mlsanity.com/paper/2107.08467/) (2021)
- [QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks](https://mlsanity.com/paper/2212.11138/) (2022)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Towards Efficient Verification of Quantized Neural Networks](https://mlsanity.com/paper/2312.12679/) (2023)
- [QEBVerif: Quantization Error Bound Verification of Neural Networks](https://mlsanity.com/paper/2212.02781/) (2022)
- [Revisiting the Adversarial Robustness-Accuracy Tradeoff in Robot Learning](https://mlsanity.com/paper/2204.07373/) (2022)
- [Verifying Quantized Neural Networks using SMT-Based Model Checking](https://mlsanity.com/paper/2106.05997/) (2021)
- [QNNVerifier: A Tool for Verifying Neural Networks using SMT-Based Model Checking](https://mlsanity.com/paper/2111.13110/) (2021)
- [Logic Gate Neural Networks are Good for Verification](https://mlsanity.com/paper/2505.19932/) (2025)
- [Quantization-aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks](https://mlsanity.com/paper/2211.16187/) (2022)
- [VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees](https://mlsanity.com/paper/2312.09748/) (2023)
- [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)
- [Floating-Point Neural Network Verification at the Software Level](https://mlsanity.com/paper/2510.23389/) (2025)
- [Confidence Preservation Property in Knowledge Distillation Abstractions](https://mlsanity.com/paper/2401.11365/) (2024)
- [VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification](https://mlsanity.com/paper/2605.07451/) (2026)
- [Evaluating robustness of support vector machines with the Lagrangian dual approach](https://mlsanity.com/paper/2306.02639/) (2023)
- [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)
- [Robustness Analysis of Continuous-Depth Models with Lagrangian Techniques](https://mlsanity.com/paper/2308.12192/) (2023)
- [Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision](https://mlsanity.com/paper/2507.22760/) (2025)
- [1 bit is all we need: binary normalized neural networks](https://mlsanity.com/paper/2509.07025/) (2025)
- [Influence-Guided Concolic Testing of Transformer Robustness](https://mlsanity.com/paper/2509.23806/) (2025)
- [NNV3: Expanding Neural Network Verification to New Architectures and Domains](https://mlsanity.com/paper/2609.30050/) (2026)

## Abstract (arXiv)

Formal verification of neural networks is an active topic of research, and recent advances have significantly increased the size of the networks that verification tools can handle. However, most methods are designed for verification of an idealized model of the actual network which works over real arithmetic and ignores rounding imprecisions. This idealization is in stark contrast to network quantization, which is a technique that trades numerical precision for computational efficiency and is, therefore, often applied in practice. Neglecting rounding errors of such low-bit quantized neural networks has been shown to lead to wrong conclusions about the network's correctness. Thus, the desired approach for verifying quantized neural networks would be one that takes these rounding errors into account. In this paper, we show that verifying the bit-exact implementation of quantized neural networks with bit-vector specifications is PSPACE-hard, even though verifying idealized real-valued networks and satisfiability of bit-vector specifications alone are each in NP. Furthermore, we explore several practical heuristics toward closing the complexity gap between idealized and bit-exact verification. In particular, we propose three techniques for making SMT-based verification of quantized neural networks more scalable. Our experiments demonstrate that our proposed methods allow a speedup of up to three orders of magnitude over existing approaches.