# On Integer Programming for the Binarized Neural Network Verification Problem

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 10 of its 23 references that are in the map.
- First posted on arXiv 1 Oct 2025.

## Builds on (most cited first, 10 of 10)

- [Counterfactual Explanations without Opening the Black Box: Automated Decisions and the GDPR](https://mlsanity.com/paper/1711.00399/) (2017)
- [Explaining Machine Learning Classifiers through Diverse Counterfactual Explanations](https://mlsanity.com/paper/1905.07697/) (2019)
- [Training Binary Neural Networks with Real-to-Binary Convolutions](https://mlsanity.com/paper/2003.11535/) (2020)
- [Verifying Properties of Binarized Deep Neural Networks](https://mlsanity.com/paper/1709.06662/) (2017)
- [An SMT-Based Approach for Verifying Binarized Neural Networks](https://mlsanity.com/paper/2011.02948/) (2020)
- [Efficient Exact Verification of Binarized Neural Networks](https://mlsanity.com/paper/2005.03597/) (2020)
- [Efficient Super Resolution Using Binarized Neural Network](https://mlsanity.com/paper/1812.06378/) (2018)
- [End to End Binarized Neural Networks for Text Classification](https://mlsanity.com/paper/2010.05223/) (2020)
- [Combinatorial Attacks on Binarized Neural Networks](https://mlsanity.com/paper/1810.03538/) (2018)
- [Embedded Binarized Neural Networks](https://mlsanity.com/paper/1709.02260/) (2017)

## Abstract (arXiv)

Binarized neural networks (BNNs) are feedforward neural networks with binary weights and activation functions. In the context of using a BNN for classification, the verification problem seeks to determine whether a small perturbation of a given input can lead it to be misclassified by the BNN, and the robustness of the BNN can be measured by solving the verification problem over multiple inputs. The BNN verification problem can be formulated as an integer programming (IP) problem. However, the natural IP formulation is often challenging to solve due to a large integrality gap induced by big-M constraints. We present two techniques to improve the IP formulation. First, we introduce a new method for obtaining a linear objective for the multi-class setting. Second, we introduce a new technique for generating valid inequalities for the IP formulation that exploits the recursive structure of BNNs. We find that our techniques enable verifying BNNs against a higher range of input perturbation than existing IP approaches within a limited time.