mlsanityData to 14 Oct 2026

Verifying Properties of Binarized Deep Neural Networks

arXiv 1709.06662 ↗First posted 19 Sep 2017stat.ML cs.AI cs.CRcited by 79

Not on the map. Why?

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.

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

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2021: 19; 2022: 21; 2023: 18; 2024: 8; 2025: 10; 2026: 3.

79 papers.

Sort:

By area:

  1. 2021Robust Machine Learning Systems: Challenges, Current Trends, Perspectives, and the Road Aheadcited by 41
  2. 2021On the Computational Intelligibility of Boolean Classifierscited by 40
  3. 2023When Deep Learning Meets Polyhedral Theory: A Surveycited by 39
  4. 2021A Review of Formal Methods applied to Machine Learningcited by 33
  5. 2021Reachability Is NP-Complete Even for the Simplest Neural Networkscited by 27
  6. 2022ASTERYX : A model-Agnostic SaT-basEd appRoach for sYmbolic and score-based eXplanationscited by 26
  7. 2021Taxonomy of Machine Learning Safety: A Survey and Primercited by 25
  8. 2022On the Computation of Necessary and Sufficient Explanationscited by 23
  9. 2022Computing Abductive Explanations for Boosted Treescited by 23
  10. 2023Logic for Explainable AIcited by 23
  11. 2021Scaling Up Exact Neural Network Compression by ReLU Stabilitycited by 19
  12. 2022Verification-Aided Deep Ensemble Selectioncited by 18
38 more
  1. 2021BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networkscited by 17
  2. 2025RvLLM: LLM Runtime Verification with Domain Knowledgecited by 17
  3. 2021Neural Termination Analysiscited by 16
  4. 2021On Quantifying Literals in Boolean Logic and Its Applications to Explainable AIcited by 16
  5. 2021Minimal Multi-Layer Modifications of Deep Neural Networkscited by 14
  6. 2025Systems Security Foundations for Agentic Computingcited by 13
  7. 2021Towards Practical Robustness Analysis for DNNs based on PAC-Model Learningcited by 12
  8. 2022QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networkscited by 12
  9. 2025Neural Network Verification is a Programming Language Challengecited by 12
  10. 2024Network Inversion of Binarised Neural Netscited by 11
  11. 2022On Neural Network Equivalence Checking using SMT Solverscited by 10
  12. 2024A Survey on Verification and Validation, Testing and Evaluations of Neurosymbolic Artificial Intelligencecited by 10
  13. 2022QEBVerif: Quantization Error Bound Verification of Neural Networkscited by 9
  14. 2022Tighter Abstract Queries in Neural Network Verificationcited by 8
  15. 2023A New Class of Explanations for Classifiers with Non-Binary Featurescited by 8
  16. 2021Drop Clause: Enhancing Performance, Interpretability and Robustness of the Tsetlin Machinecited by 7
  17. 2021Customizable Reference Runtime Monitoring of Neural Networks using Resolution Boxescited by 6
  18. 2021Provable Guarantees on the Robustness of Decision Rules to Causal Interventionscited by 6
  19. 2021Verifying Quantized Neural Networks using SMT-Based Model Checkingcited by 6
  20. 2021Geometric Path Enumeration for Equivalence Verification of Neural Networkscited by 6
  21. 2023What, Indeed, is an Achievable Provable Guarantee for Learning-Enabled Safety Critical Systemscited by 6
  22. 2023Locally-Minimal Probabilistic Explanationscited by 6
  23. 2024Formal Explanations for Neuro-Symbolic AIcited by 6
  24. 2022Reachability In Simple Neural Networkscited by 5
  25. 2023On the Complexity of Enumerating Prime Implicants from Decision-DNNF Circuitscited by 5
  26. 2021QNNVerifier: A Tool for Verifying Neural Networks using SMT-Based Model Checkingcited by 4
  27. 2022A Scalable, Interpretable, Verifiable & Differentiable Logic Gate Convolutional Neural Network Architecture From Truth Tablescited by 4
  28. 2024Revisiting Differential Verification: Equivalence Verification with Confidencecited by 4
  29. 2021BCNN: Binary Complex Neural Networkcited by 3
  30. 2022A Mixed Integer Programming Approach for Verifying Properties of Binarized Neural Networkscited by 3
  31. 2022Quantization-aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networkscited by 3
  32. 2023Efficient Computation of Shap Explanation Scores for Neural Network Classifiers via Knowledge Compilationcited by 3
  33. 2024A Survey of Neural Network Robustness Assessment in Image Recognitioncited by 3
  34. 2021Toward Neural-Network-Guided Program Synthesis and Verificationcited by 2
  35. 2022Systems Challenges for Trustworthy Embodied Systemscited by 2
  36. 2022Deep Binary Reinforcement Learning for Scalable Verificationcited by 2
  37. 2022CEG4N: Counter-Example Guided Neural Network Quantization Refinementcited by 2
  38. 2023Incremental Satisfiability Modulo Theory for Verification of Deep Neural Networkscited by 2

50 most cited of 79 All 79 (JSON)