# Efficient Exact Verification of Binarized Neural Networks

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

## Key facts

- Cited by 33 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 7 May 2020.

## Built on by (most cited first, 30 of 33)

- [A Survey of Quantization Methods for Efficient Neural Network Inference](https://mlsanity.com/paper/2103.13630/) (2021)
- [On the Computational Intelligibility of Boolean Classifiers](https://mlsanity.com/paper/2104.06172/) (2021)
- [When Deep Learning Meets Polyhedral Theory: A Survey](https://mlsanity.com/paper/2305.00241/) (2023)
- [Physics-Informed Machine Learning for Modeling and Control of Dynamical Systems](https://mlsanity.com/paper/2306.13867/) (2023)
- [Anchor-based Plain Net for Mobile Image Super-Resolution](https://mlsanity.com/paper/2105.09750/) (2021)
- [Logic for Explainable AI](https://mlsanity.com/paper/2305.05172/) (2023)
- [BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks](https://mlsanity.com/paper/2103.07224/) (2021)
- [QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks](https://mlsanity.com/paper/2212.11138/) (2022)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Towards Efficient Verification of Quantized Neural Networks](https://mlsanity.com/paper/2312.12679/) (2023)
- [SHAP Meets Tensor Networks: Provably Tractable Explanations with Parallelism](https://mlsanity.com/paper/2510.21599/) (2025)
- [Drop Clause: Enhancing Performance, Interpretability and Robustness of the Tsetlin Machine](https://mlsanity.com/paper/2105.14506/) (2021)
- [Verifying Low-dimensional Input Neural Networks via Input Quantization](https://mlsanity.com/paper/2108.07961/) (2021)
- [Locally-Minimal Probabilistic Explanations](https://mlsanity.com/paper/2312.11831/) (2023)
- [Self-Healing Robust Neural Networks via Closed-Loop Control](https://mlsanity.com/paper/2206.12963/) (2022)
- [Efficient and Robust Mixed-Integer Optimization Methods for Training Binarized Deep Neural Networks](https://mlsanity.com/paper/2110.11382/) (2021)
- [A Scalable, Interpretable, Verifiable & Differentiable Logic Gate Convolutional Neural Network Architecture From Truth Tables](https://mlsanity.com/paper/2208.08609/) (2022)
- [Logic Gate Neural Networks are Good for Verification](https://mlsanity.com/paper/2505.19932/) (2025)
- [A Mixed Integer Programming Approach for Verifying Properties of Binarized Neural Networks](https://mlsanity.com/paper/2203.07078/) (2022)
- [Quantization-aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks](https://mlsanity.com/paper/2211.16187/) (2022)
- [Verifiable Learning for Robust Tree Ensembles](https://mlsanity.com/paper/2305.03626/) (2023)
- [Deep Binary Reinforcement Learning for Scalable Verification](https://mlsanity.com/paper/2203.05704/) (2022)
- [Effective Neural Network L0 Regularization With BinMask](https://mlsanity.com/paper/2304.11237/) (2023)
- [Current and Future Challenges in Knowledge Representation and Reasoning](https://mlsanity.com/paper/2308.04161/) (2023)
- [Decomposing Hard SAT Instances with Metaheuristic Optimization](https://mlsanity.com/paper/2312.10436/) (2023)
- [Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization](https://mlsanity.com/paper/2405.17049/) (2024)
- [Verifying Properties of Tsetlin Machines](https://mlsanity.com/paper/2303.14464/) (2023)
- [Evaluating robustness of support vector machines with the Lagrangian dual approach](https://mlsanity.com/paper/2306.02639/) (2023)
- [Verifiable Boosted Tree Ensembles](https://mlsanity.com/paper/2402.14988/) (2024)
- [Golden Ratio Search: A Low-Power Adversarial Attack for Deep Learning based Modulation Classification](https://mlsanity.com/paper/2409.11454/) (2024)

## Abstract (arXiv)

Concerned with the reliability of neural networks, researchers have developed verification techniques to prove their robustness. Most verifiers work with real-valued networks. Unfortunately, the exact (complete and sound) verifiers face scalability challenges and provide no correctness guarantees due to floating point errors. We argue that Binarized Neural Networks (BNNs) provide comparable robustness and allow exact and significantly more efficient verification. We present a new system, EEV, for efficient and exact verification of BNNs. EEV consists of two parts: (i) a novel SAT solver that speeds up BNN verification by natively handling the reified cardinality constraints arising in BNN encodings; and (ii) strategies to train solver-friendly robust BNNs by inducing balanced layer-wise sparsity and low cardinality bounds, and adaptively cancelling the gradients. We demonstrate the effectiveness of EEV by presenting the first exact verification results for L-inf-bounded adversarial robustness of nontrivial convolutional BNNs on the MNIST and CIFAR10 datasets. Compared to exact verification of real-valued networks of the same architectures on the same tasks, EEV verifies BNNs hundreds to thousands of times faster, while delivering comparable verifiable accuracy in most cases.