# A Mixed Integer Programming Approach for Verifying Properties of Binarized Neural Networks

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 19 references that are in the map.
- First posted on arXiv 11 Mar 2022.

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

- [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)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [Verifying Properties of Binarized Deep Neural Networks](https://mlsanity.com/paper/1709.06662/) (2017)
- [Exploiting Verified Neural Networks via Floating Point Numerical Error](https://mlsanity.com/paper/2003.03021/) (2020)
- [Efficient Exact Verification of Binarized Neural Networks](https://mlsanity.com/paper/2005.03597/) (2020)

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

- [Quantization-aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks](https://mlsanity.com/paper/2211.16187/) (2022)
- [Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization](https://mlsanity.com/paper/2405.17049/) (2024)
- [Verification of Neural Networks Local Differential Classification Privacy](https://mlsanity.com/paper/2310.20299/) (2023)

## Abstract (arXiv)

Many approaches for verifying input-output properties of neural networks have been proposed recently. However, existing algorithms do not scale well to large networks. Recent work in the field of model compression studied binarized neural networks (BNNs), whose parameters and activations are binary. BNNs tend to exhibit a slight decrease in performance compared to their full-precision counterparts, but they can be easier to verify. This paper proposes a simple mixed integer programming formulation for BNN verification that leverages network structure. We demonstrate our approach by verifying properties of BNNs trained on the MNIST dataset and an aircraft collision avoidance controller. We compare the runtime of our approach against state-of-the-art verification algorithms for full-precision neural networks. The results suggest that the difficulty of training BNNs might be worth the reduction in runtime achieved by our verification algorithm.