# BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks

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

## Key facts

- Cited by 17 papers in the map (data through 14 Oct 2026).
- Builds on 45 of its 80 references that are in the map.
- First posted on arXiv 12 Mar 2021.

## Builds on (most cited first, 30 of 45)

- [EfficientNet: Rethinking Model Scaling for Convolutional Neural Networks](https://mlsanity.com/paper/1905.11946/) (2019)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Adversarial examples in the physical world](https://mlsanity.com/paper/1607.02533/) (2016)
- [Practical Black-Box Attacks against Machine Learning](https://mlsanity.com/paper/1602.02697/) (2016)
- [XNOR-Net: ImageNet Classification Using Binary Convolutional Neural Networks](https://mlsanity.com/paper/1603.05279/) (2016)
- [The Limitations of Deep Learning in Adversarial Settings](https://mlsanity.com/paper/1511.07528/) (2015)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Deep Learning for Medical Image Analysis](https://mlsanity.com/paper/1708.08987/) (2017)
- [Deep Learning with Limited Numerical Precision](https://mlsanity.com/paper/1502.02551/) (2015)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Distilling a Neural Network Into a Soft Decision Tree](https://mlsanity.com/paper/1711.09784/) (2017)
- [Formal Guarantees on the Robustness of a Classifier against Adversarial Manipulation](https://mlsanity.com/paper/1705.08475/) (2017)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [A Dual Approach to Scalable Verification of Deep Networks](https://mlsanity.com/paper/1803.06567/) (2018)
- [Interpretable Machine Learning -- A Brief History, State-of-the-Art and Challenges](https://mlsanity.com/paper/2010.09337/) (2020)
- [Maximum Resilience of Artificial Neural Networks](https://mlsanity.com/paper/1705.01040/) (2017)
- [Interpreting CNNs via Decision Trees](https://mlsanity.com/paper/1802.00121/) (2018)
- [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)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [An Abstraction-Based Framework for Neural Network Verification](https://mlsanity.com/paper/1910.14574/) (2019)
- [Who is Real Bob? Adversarial Attacks on Speaker Recognition Systems](https://mlsanity.com/paper/1911.01840/) (2019)
- [Extracting Automata from Recurrent Neural Networks Using Queries and Counterexamples](https://mlsanity.com/paper/1711.09576/) (2017)
- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [A Statistical Approach to Assessing Neural Network Robustness](https://mlsanity.com/paper/1811.07209/) (2018)

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

- [Logic for Explainable AI](https://mlsanity.com/paper/2305.05172/) (2023)
- [The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks](https://mlsanity.com/paper/2301.07068/) (2023)
- [RvLLM: LLM Runtime Verification with Domain Knowledge](https://mlsanity.com/paper/2505.18585/) (2025)
- [Attack as Defense: Characterizing Adversarial Examples using Robustness](https://mlsanity.com/paper/2103.07633/) (2021)
- [QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks](https://mlsanity.com/paper/2212.11138/) (2022)
- [Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks](https://mlsanity.com/paper/2207.00759/) (2022)
- [AS2T: Arbitrary Source-To-Target Adversarial Attack on Speaker Recognition Systems](https://mlsanity.com/paper/2206.03351/) (2022)
- [QEBVerif: Quantization Error Bound Verification of Neural Networks](https://mlsanity.com/paper/2212.02781/) (2022)
- [A Scalable, Interpretable, Verifiable & Differentiable Logic Gate Convolutional Neural Network Architecture From Truth Tables](https://mlsanity.com/paper/2208.08609/) (2022)
- [Adversarial Attacks on ML Defense Models Competition](https://mlsanity.com/paper/2110.08042/) (2021)
- [Verification of Bit-Flip Attacks against Quantized Neural Networks](https://mlsanity.com/paper/2502.16286/) (2025)
- [gRoMA: a Tool for Measuring the Global Robustness of Deep Neural Networks](https://mlsanity.com/paper/2301.02288/) (2023)
- [Scaling #DNN-Verification Tools with Efficient Bound Propagation and Parallel Computing](https://mlsanity.com/paper/2312.05890/) (2023)
- [Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization](https://mlsanity.com/paper/2405.17049/) (2024)
- [Training Verification-Friendly Neural Networks via Neuron Behavior Consistency](https://mlsanity.com/paper/2412.13229/) (2024)
- [An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks](https://mlsanity.com/paper/2307.15907/) (2023)
- [Eventizing Traditionally Opaque Binary Neural Networks as 1-safe Petri net Models](https://mlsanity.com/paper/2602.13128/) (2026)

## Abstract (arXiv)

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.