On Integer Programming for the Binarized Neural Network Verification Problem

Binarized neural networks (BNNs) are feedforward neural networks with binary weights and activation functions. When using a BNN for classification, the verification problem asks whether a small perturbation of a given input can cause the network to misclassify that input. The robustness of a BNN can then be assessed by solving the verification problem on multiple inputs. The BNN verification problem can be formulated as an integer programming (IP) problem. However, the natural IP formulation is often difficult to solve because big-M constraints induce a large integrality gap. We present two techniques to strengthen this IP formulation. First, we introduce a new method for obtaining a linear objective in the multiclass setting. Second, we introduce a new technique for generating valid inequalities that exploits the recursive structure of BNNs. Our computational results show that these techniques enable BNN verification under larger input perturbations than existing IP approaches within a limited time.

Funding: This research was supported by the Office of Naval Research [Grant N000142612067] and by the National Science Foundation [Grant 2000986].

Supplemental Material: The online appendix is available at https://doi.org/10.1287/ijoo.2025.0099.