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

TL;DR

QNNVerifier is an open-source SMT-based tool that verifies neural network implementations considering quantization effects, enabling safety property checks with advanced strategies and invariant inference to improve efficiency.

Contribution

It introduces the first support for quantization in neural network verification using SMT techniques, combining invariant inference and discretization for faster analysis.

Findings

Supports fixed- and floating-point quantization effects

Enables verification of safety properties with multiple strategies

Achieves significant speed-ups through invariant inference

Abstract

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