# Verifying Quantized Neural Networks using SMT-Based Model Checking

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 31 of its 101 references that are in the map.
- First posted on arXiv 10 Jun 2021.

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

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [A Unified Approach to Interpreting Model Predictions](https://mlsanity.com/paper/1705.07874/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Gaussian Error Linear Units (GELUs)](https://mlsanity.com/paper/1606.08415/) (2016)
- [A Comprehensive Survey on Graph Neural Networks](https://mlsanity.com/paper/1901.00596/) (2019)
- [Implicit Neural Representations with Periodic Activation Functions](https://mlsanity.com/paper/2006.09661/) (2020)
- [XNOR-Net: ImageNet Classification Using Binary Convolutional Neural Networks](https://mlsanity.com/paper/1603.05279/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Quantized Neural Networks: Training Neural Networks with Low Precision Weights and Activations](https://mlsanity.com/paper/1609.07061/) (2016)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Certified Robustness to Adversarial Word Substitutions](https://mlsanity.com/paper/1909.00986/) (2019)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [Compression of Deep Convolutional Neural Networks for Fast and Low Power Mobile Applications](https://mlsanity.com/paper/1511.06530/) (2015)
- [Fixed Point Quantization of Deep Convolutional Networks](https://mlsanity.com/paper/1511.06393/) (2015)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [A Dual Approach to Scalable Verification of Deep Networks](https://mlsanity.com/paper/1803.06567/) (2018)
- [LaVAN: Localized and Visible Adversarial Noise](https://mlsanity.com/paper/1801.02608/) (2018)
- [Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming](https://mlsanity.com/paper/1903.01287/) (2019)
- [Measuring Neural Net Robustness with Constraints](https://mlsanity.com/paper/1605.07262/) (2016)
- [Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks](https://mlsanity.com/paper/1708.03322/) (2017)
- [Verifying Properties of Binarized Deep Neural Networks](https://mlsanity.com/paper/1709.06662/) (2017)
- [A Survey on Methods and Theories of Quantized Neural Networks](https://mlsanity.com/paper/1808.04752/) (2018)
- [An SMT-Based Approach for Verifying Binarized Neural Networks](https://mlsanity.com/paper/2011.02948/) (2020)
- [Exploiting Verified Neural Networks via Floating Point Numerical Error](https://mlsanity.com/paper/2003.03021/) (2020)
- [Scalable Verification of Quantized Neural Networks (Technical Report)](https://mlsanity.com/paper/2012.08185/) (2020)
- [Verification of Neural Network Behaviour: Formal Guarantees for Power System Applications](https://mlsanity.com/paper/1910.01624/) (2019)
- [Probabilistic Inference Modulo Theories](https://mlsanity.com/paper/1605.08367/) (2016)
- [Incremental Bounded Model Checking of Artificial Neural Networks in CUDA](https://mlsanity.com/paper/1907.12933/) (2019)

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

- [QNNVerifier: A Tool for Verifying Neural Networks using SMT-Based Model Checking](https://mlsanity.com/paper/2111.13110/) (2021)
- [Chordal Sparsity for SDP-based Neural Network Verification](https://mlsanity.com/paper/2206.03482/) (2022)
- [Quantization-aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks](https://mlsanity.com/paper/2211.16187/) (2022)
- [NeuroCodeBench: a plain C neural network benchmark for software verification](https://mlsanity.com/paper/2309.03617/) (2023)
- [QNNRepair: Quantized Neural Network Repair](https://mlsanity.com/paper/2306.13793/) (2023)
- [Influence-Guided Concolic Testing of Transformer Robustness](https://mlsanity.com/paper/2509.23806/) (2025)

## Abstract (arXiv)

Artificial Neural Networks (ANNs) are being deployed for an increasing number of safety-critical applications, including autonomous cars and medical diagnosis. However, concerns about their reliability have been raised due to their black-box nature and apparent fragility to adversarial attacks. These concerns are amplified when ANNs are deployed on restricted system, which limit the precision of mathematical operations and thus introduce additional quantization errors. Here, we develop and evaluate a novel symbolic verification framework using software model checking (SMC) and satisfiability modulo theories (SMT) to check for vulnerabilities in ANNs. More specifically, we propose several ANN-related optimizations for SMC, including invariant inference via interval analysis, slicing, expression simplifications, and discretization of non-linear activation functions. With this verification framework, we can provide formal guarantees on the safe behavior of ANNs implemented both in floating- and fixed-point arithmetic. In this regard, our verification approach was able to verify and produce adversarial examples for 52 test cases spanning image classification and general machine learning applications. Furthermore, for small- to medium-sized ANN, our approach completes most of its verification runs in minutes. Moreover, in contrast to most state-of-the-art methods, our approach is not restricted to specific choices regarding activation functions and non-quantized representations. Our experiments show that our approach can analyze larger ANN implementations and substantially reduce the verification time compared to state-of-the-art techniques that use SMT solving.