# Verifying Properties of Binarized Deep Neural Networks

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

## Key facts

- Cited by 79 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 19 Sep 2017.

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

- [Robust Machine Learning Systems: Challenges, Current Trends, Perspectives, and the Road Ahead](https://mlsanity.com/paper/2101.02559/) (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)
- [A Review of Formal Methods applied to Machine Learning](https://mlsanity.com/paper/2104.02466/) (2021)
- [Reachability Is NP-Complete Even for the Simplest Neural Networks](https://mlsanity.com/paper/2108.13179/) (2021)
- [ASTERYX : A model-Agnostic SaT-basEd appRoach for sYmbolic and score-based eXplanations](https://mlsanity.com/paper/2206.11900/) (2022)
- [Taxonomy of Machine Learning Safety: A Survey and Primer](https://mlsanity.com/paper/2106.04823/) (2021)
- [On the Computation of Necessary and Sufficient Explanations](https://mlsanity.com/paper/2203.10451/) (2022)
- [Computing Abductive Explanations for Boosted Trees](https://mlsanity.com/paper/2209.07740/) (2022)
- [Logic for Explainable AI](https://mlsanity.com/paper/2305.05172/) (2023)
- [Scaling Up Exact Neural Network Compression by ReLU Stability](https://mlsanity.com/paper/2102.07804/) (2021)
- [Verification-Aided Deep Ensemble Selection](https://mlsanity.com/paper/2202.03898/) (2022)
- [BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks](https://mlsanity.com/paper/2103.07224/) (2021)
- [RvLLM: LLM Runtime Verification with Domain Knowledge](https://mlsanity.com/paper/2505.18585/) (2025)
- [Neural Termination Analysis](https://mlsanity.com/paper/2102.03824/) (2021)
- [On Quantifying Literals in Boolean Logic and Its Applications to Explainable AI](https://mlsanity.com/paper/2108.09876/) (2021)
- [Minimal Multi-Layer Modifications of Deep Neural Networks](https://mlsanity.com/paper/2110.09929/) (2021)
- [Systems Security Foundations for Agentic Computing](https://mlsanity.com/paper/2512.01295/) (2025)
- [Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning](https://mlsanity.com/paper/2101.10102/) (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)
- [Network Inversion of Binarised Neural Nets](https://mlsanity.com/paper/2402.11995/) (2024)
- [On Neural Network Equivalence Checking using SMT Solvers](https://mlsanity.com/paper/2203.11629/) (2022)
- [A Survey on Verification and Validation, Testing and Evaluations of Neurosymbolic Artificial Intelligence](https://mlsanity.com/paper/2401.03188/) (2024)
- [QEBVerif: Quantization Error Bound Verification of Neural Networks](https://mlsanity.com/paper/2212.02781/) (2022)
- [Tighter Abstract Queries in Neural Network Verification](https://mlsanity.com/paper/2210.12871/) (2022)
- [A New Class of Explanations for Classifiers with Non-Binary Features](https://mlsanity.com/paper/2304.14760/) (2023)
- [Drop Clause: Enhancing Performance, Interpretability and Robustness of the Tsetlin Machine](https://mlsanity.com/paper/2105.14506/) (2021)
- [Customizable Reference Runtime Monitoring of Neural Networks using Resolution Boxes](https://mlsanity.com/paper/2104.14435/) (2021)
- [Provable Guarantees on the Robustness of Decision Rules to Causal Interventions](https://mlsanity.com/paper/2105.09108/) (2021)

## Abstract (arXiv)

Understanding properties of deep neural networks is an important challenge in deep learning. In this paper, we take a step in this direction by proposing a rigorous way of verifying properties of a popular class of neural networks, Binarized Neural Networks, using the well-developed means of Boolean satisfiability. Our main contribution is a construction that creates a representation of a binarized neural network as a Boolean formula. Our encoding is the first exact Boolean representation of a deep neural network. Using this encoding, we leverage the power of modern SAT solvers along with a proposed counterexample-guided search procedure to verify various properties of these networks. A particular focus will be on the critical property of robustness to adversarial perturbations. For this property, our experimental results demonstrate that our approach scales to medium-size deep neural networks used in image classification tasks. To the best of our knowledge, this is the first work on verifying properties of deep neural networks using an exact Boolean encoding of the network.