An SMT-based approach for verifying binarized neural networks

DOI10.1007/978-3-030-72013-1_11zbMATH Open1474.68188arXiv2011.02948OpenAlexW3140205966MaRDI QIDQ2233508FDOQ2233508

Authors: Guy Amir, Haoze Wu, Clark Barrett, Guy Katz 

Publication date: 18 October 2021

Abstract: Deep learning has emerged as an effective approach for creating modern software systems, with neural networks often surpassing hand-crafted systems. Unfortunately, neural networks are known to suffer from various safety and security issues. Formal verification is a promising avenue for tackling this difficulty, by formally certifying that networks are correct. We propose an SMT-based technique for verifying Binarized Neural Networks - a popular kind of neural network, where some weights have been binarized in order to render the neural network more memory and energy efficient, and quicker to evaluate. One novelty of our technique is that it allows the verification of neural networks that include both binarized and non-binarized components. Neural network verification is computationally very difficult, and so we propose here various optimizations, integrated into our SMT procedure as deduction steps, as well as an approach for parallelizing verification queries. We implement our technique as an extension to the Marabou framework, and use it to evaluate the approach on popular binarized neural network architectures.

Full work available at URL: https://arxiv.org/abs/2011.02948

Recommendations

• Verifying binarized neural networks by Angluin-style learning
• \textsf{BDD4BNN}: a BDD-based quantitative analysis framework for binarized neural networks
• Reluplex: an efficient SMT solver for verifying deep neural networks
• Reluplex: a calculus for reasoning about deep neural networks
• Formal verification of piece-wise linear feed-forward neural networks

Mathematics Subject Classification ID

Artificial neural networks and deep learning (68T07) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Title not available (Why is that?)
• Deep learning
• Satisfiability modulo theories
• Safety verification of deep neural networks
• Reluplex: an efficient SMT solver for verifying deep neural networks
• Verification of deep convolutional neural networks using ImageStars
• An abstraction-based framework for neural network verification
• Formal verification of piece-wise linear feed-forward neural networks
• How many bits does it take to quantize your neural network?
• DeepSafe: a data-driven approach for assessing robustness of neural networks
• Title not available (Why is that?)

Cited In (12)

• \textsf{BDD4BNN}: a BDD-based quantitative analysis framework for binarized neural networks
• On neural network equivalence checking using SMT solvers
• \textsc{OccRob}: efficient SMT-based occlusion robustness verification of deep neural networks
• Towards formal XAI: formally approximate minimal explanations of neural networks
• Reluplex: an efficient SMT solver for verifying deep neural networks
• Verifying binarized neural networks by Angluin-style learning
• Verifying the generalization of deep learning to out-of-distribution domains
• Verifying Neural Networks Against Backdoor Attacks
• Challenging SMT solvers to verify neural networks
• \textsf{QEBVerif}: quantization error bound verification of neural networks
• Verifying generalization in deep learning
• Task-aware verifiable RNN-based policies for partially observable Markov decision processes

Uses Software

• Marabou
• Fashion-MNIST
• XNOR-Net

This page was built for publication: An SMT-based approach for verifying binarized neural networks

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233508)