Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On Integer Programming for the Binarized Neural Network Verification Problem

Woojin Kim, James R. Luedtke

TL;DR

This work addresses verifying binarized neural networks (BNNs) under input perturbations by formulating the problem as an integer program and tackling two core challenges: a large integrality gap from big-$M$ formulations and limited scalability when considering many target misclassifications. It introduces a linear objective formulation that collapses all alternative classes into a single optimization, and layerwise derived valid inequalities that exploit the recursive BNN structure to tighten relaxations via outer/inner approximations and targeted subproblems. Theoretical developments include layer-propagation linearizations, convex-hull descriptions for neurons, and sufficient conditions for variable-fixings and two-variable cuts, complemented by a comprehensive computational study on MNIST-based networks showing faster verification and larger perturbation ranges with the proposed methods. The results demonstrate practical improvements in BNN verification performance and offer a path toward more scalable, exact verification and potential utility for counterfactual explanations in interpretable ML systems.

Abstract

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.

On Integer Programming for the Binarized Neural Network Verification Problem

TL;DR

This work addresses verifying binarized neural networks (BNNs) under input perturbations by formulating the problem as an integer program and tackling two core challenges: a large integrality gap from big- formulations and limited scalability when considering many target misclassifications. It introduces a linear objective formulation that collapses all alternative classes into a single optimization, and layerwise derived valid inequalities that exploit the recursive BNN structure to tighten relaxations via outer/inner approximations and targeted subproblems. Theoretical developments include layer-propagation linearizations, convex-hull descriptions for neurons, and sufficient conditions for variable-fixings and two-variable cuts, complemented by a comprehensive computational study on MNIST-based networks showing faster verification and larger perturbation ranges with the proposed methods. The results demonstrate practical improvements in BNN verification performance and offer a path toward more scalable, exact verification and potential utility for counterfactual explanations in interpretable ML systems.

Abstract

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- 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.

Paper Structure

This paper contains 23 sections, 7 theorems, 56 equations, 13 tables, 6 algorithms.

Table of Contents

  1. Introduction
  2. IP Formulations
  3. Constraint Formulation
  4. Layer Propagation Constraint Formulation
  5. Input Perturbation Constraint Formulation
  6. Objective Formulation
  7. Valid Inequalities for Neurons
  8. Layerwise Derived Valid Inequalities
  9. Variable Fixing
  10. Two-variable Inequalities
  11. Algorithms
  12. Computational Study
  13. Test Instances
  14. Implementation Details
  15. Results
  16. ...and 8 more sections

Key Result

Lemma 0

Each $(\mathbf{x}^0, \mathbf{x}^1) \in X^0 \times \{0, 1\}^{n^1}$ satisfies eq:origFormPropConstr for $\ell=1$ if and only if it satisfies the following inequalities: For $\ell \in \{2, \ldots, L\}$, $(\mathbf{x}^{\ell - 1}, \mathbf{x}^\ell) \in \{0, 1\}^{n^{\ell - 1}} \times \{0, 1\}^{n^\ell}$ satisfies eq:origFormPropConstr if and only if it satisfies the following inequalities:

Theorems & Definitions (12)

  • Lemma 0
  • Lemma 1
  • Theorem 2
  • Theorem 3
  • Lemma 4
  • proof
  • Theorem 5
  • proof
  • Lemma 5
  • proof
  • ...and 2 more