# QNNVerifier: A Tool for Verifying Neural Networks using SMT-Based Model Checking

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 13 of its 24 references that are in the map.
- First posted on arXiv 25 Nov 2021.

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

- [A Unified Approach to Interpreting Model Predictions](https://mlsanity.com/paper/1705.07874/) (2017)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [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)
- [Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming](https://mlsanity.com/paper/1903.01287/) (2019)
- [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)
- [Scalable Verification of Quantized Neural Networks (Technical Report)](https://mlsanity.com/paper/2012.08185/) (2020)
- [Verifying Quantized Neural Networks using SMT-Based Model Checking](https://mlsanity.com/paper/2106.05997/) (2021)

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

- [Chordal Sparsity for SDP-based Neural Network Verification](https://mlsanity.com/paper/2206.03482/) (2022)
- [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)
- [Lipschitz-Based Robustness Certification Under Floating-Point Execution](https://mlsanity.com/paper/2603.13334/) (2026)

## Abstract (arXiv)

QNNVerifier is the first open-source tool for verifying implementations of neural networks that takes into account the finite word-length (i.e. quantization) of their operands. The novel support for quantization is achieved by employing state-of-the-art software model checking (SMC) techniques. It translates the implementation of neural networks to a decidable fragment of first-order logic based on satisfiability modulo theories (SMT). The effects of fixed- and floating-point operations are represented through direct implementations given a hardware-determined precision. Furthermore, QNNVerifier allows to specify bespoke safety properties and verify the resulting model with different verification strategies (incremental and k-induction) and SMT solvers. Finally, QNNVerifier is the first tool that combines invariant inference via interval analysis and discretization of non-linear activation functions to speed up the verification of neural networks by orders of magnitude. A video presentation of QNNVerifier is available at https://youtu.be/7jMgOL41zTY