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

Autor:	Song, Xidan, Manino, Edoardo, Sena, Luiz, Alves, Erickson, Filho, Eddie de Lima, Bessa, Iury, Lujan, Mikel, Cordeiro, Lucas
Rok vydání:	2021
Předmět:	Computer Science - Artificial Intelligence Computer Science - Machine Learning Computer Science - Logic in Computer Science
Druh dokumentu:	Working Paper
Popis:	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 Comment: Submitted to the Demo track of the ICSE 2022 conference
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2111.13110 Zobrazit plný text záznamu View this record from Arxiv