\textsf{BDD4BNN}: a BDD-based quantitative analysis framework for binarized neural networks
From MaRDI portal
Publication:832164
Abstract: Verifying and explaining the behavior of neural networks is becoming increasingly important, especially when they are deployed in safety-critical applications. In this paper, we study verification problems for Binarized Neural Networks (BNNs), the 1-bit quantization of general real-numbered neural networks. Our approach is to encode BNNs into Binary Decision Diagrams (BDDs), which is done by exploiting the internal structure of the BNNs. In particular, we translate the input-output relation of blocks in BNNs to cardinality constraints which are then encoded by BDDs. Based on the encoding, we develop a quantitative verification framework for BNNs where precise and comprehensive analysis of BNNs can be performed. We demonstrate the application of our framework by providing quantitative robustness analysis and interpretability for BNNs. We implement a prototype tool BDD4BNN and carry out extensive experiments which confirm the effectiveness and efficiency of our approach.
Recommendations
- Verifying binarized neural networks by Angluin-style learning
- An SMT-based approach for verifying binarized neural networks
- How many bits does it take to quantize your neural network?
- Branch and bound for piecewise linear neural network verification
- Inference and contradictory analysis for binary neural networks
Cites work
- A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability
- An abstraction-based framework for neural network verification
- An efficient query learning algorithm for ordered binary decision diagrams
- An SMT theory of fixed-point arithmetic
- An SMT-based approach for verifying binarized neural networks
- Assessing heuristic machine learning explanations with model counting
- Branch and bound for piecewise linear neural network verification
- Constrained image generation using binarized neural networks with decision procedures
- Formal verification of piece-wise linear feed-forward neural networks
- Graph-Based Algorithms for Boolean Function Manipulation
- How many bits does it take to quantize your neural network?
- scientific article; zbMATH DE number 1956595 (Why is no real title available?)
- Improving neural network verification through spurious region guided refinement
- Reluplex: an efficient SMT solver for verifying deep neural networks
- Safety verification of deep neural networks
- Verification of deep convolutional neural networks using ImageStars
- Verifying binarized neural networks by Angluin-style learning
Cited in
(9)- Inference and contradictory analysis for binary neural networks
- Verifying binarized neural networks by Angluin-style learning
- An SMT-based approach for verifying binarized neural networks
- How many bits does it take to quantize your neural network?
- Formal verification for quantized neural networks
- \textsf{CLEVEREST}: accelerating CEGAR-based neural network verification via adversarial attacks
- Quantitative Verification for Neural Networks using ProbStars
- \textsf{QEBVerif}: quantization error bound verification of neural networks
- Quantitative verification of learning-enabled systems using ProbStar reachability
Describes a project that uses
Uses Software
This page was built for publication: \textsf{BDD4BNN}: a BDD-based quantitative analysis framework for binarized neural networks
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832164)
