On Integer Programming for the Binarized Neural Network Verification Problem

• URL: http://arxiv.org/abs/2510.01525v1
• Date: Wed, 01 Oct 2025 23:43:18 GMT
• Title: On Integer Programming for the Binarized Neural Network Verification Problem
• Authors: Woojin Kim, James R. Luedtke,
• Abstract summary: Binarized neural networks (BNNs) are feedforward neural networks with binary weights and activation functions.<n> verification problem seeks to determine whether a small perturbation of a given input can lead it to be misclassified by the BNN.
• Score: 3.342097413151171
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• S$^2$NN: Sub-bit Spiking Neural Networks [53.08060832135342]
  Spiking Neural Networks (SNNs) offer an energy-efficient paradigm for machine intelligence.<n>Despite recent advances in binary SNNs, the storage and computational demands remain substantial for large-scale networks.<n>We propose Sub-bit Spiking Neural Networks (S$2$NNs) that represent weights with less than one bit.
  arXiv  Detail & Related papers  (2025-09-29T04:17:44Z)
• NAS-BNN: Neural Architecture Search for Binary Neural Networks [55.058512316210056]
  We propose a novel neural architecture search scheme for binary neural networks, named NAS-BNN. Our discovered binary model family outperforms previous BNNs for a wide range of operations (OPs) from 20M to 200M. In addition, we validate the transferability of these searched BNNs on the object detection task, and our binary detectors with the searched BNNs achieve a novel state-of-the-art result, e.g., 31.6% mAP with 370M OPs, on MS dataset.
  arXiv  Detail & Related papers  (2024-08-28T02:17:58Z)
• Neural Network Verification with Branch-and-Bound for General Nonlinearities [63.39918329535165]
  Branch-and-bound (BaB) is among the most effective techniques for neural network (NN) verification.<n>We develop a general framework, named GenBaB, to conduct BaB on general nonlinearities to verify NNs with general architectures.<n>Our framework also allows the verification of general nonlinear graphs and enables verification applications beyond simple NNs.
  arXiv  Detail & Related papers  (2024-05-31T17:51:07Z)
• An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks [13.271286153792058]
  Quantized neural networks (QNNs) have been developed, with binarized neural networks (BNNs) restricted to binary values as a special case. This paper presents an automata-theoretic approach to synthesizing BNNs that meet designated properties.
  arXiv  Detail & Related papers  (2023-07-29T06:27:28Z)
• BNN-DP: Robustness Certification of Bayesian Neural Networks via Dynamic Programming [8.162867143465382]
  We introduce BNN-DP, an efficient framework for analysis of adversarial robustness of Bayesian Neural Networks. We show that BNN-DP outperforms state-of-the-art methods by up to four orders of magnitude in both tightness of the bounds and computational efficiency.
  arXiv  Detail & Related papers  (2023-06-19T07:19:15Z)
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks [94.63547069706459]
  #DNN-Verification problem involves counting the number of input configurations of a DNN that result in a violation of a safety property. We propose a novel approach that returns the exact count of violations. We present experimental results on a set of safety-critical benchmarks.
  arXiv  Detail & Related papers  (2023-01-17T18:32:01Z)
• Comparative Analysis of Interval Reachability for Robust Implicit and Feedforward Neural Networks [64.23331120621118]
  We use interval reachability analysis to obtain robustness guarantees for implicit neural networks (INNs) INNs are a class of implicit learning models that use implicit equations as layers. We show that our approach performs at least as well as, and generally better than, applying state-of-the-art interval bound propagation methods to INNs.
  arXiv  Detail & Related papers  (2022-04-01T03:31:27Z)
• A Mixed Integer Programming Approach for Verifying Properties of Binarized Neural Networks [44.44006029119672]
  We propose a mixed integer programming formulation for BNN verification. We demonstrate our approach by verifying properties of BNNs trained on the MNIST dataset and an aircraft collision avoidance controller.
  arXiv  Detail & Related papers  (2022-03-11T01:11:29Z)
• BCNN: Binary Complex Neural Network [16.82755328827758]
  Binarized neural networks, or BNNs, show great promise in edge-side applications with resource limited hardware. We introduce complex representation into the BNNs and propose Binary complex neural network. BCNN improves BNN by strengthening its learning capability through complex representation and extending its applicability to complex-valued input data.
  arXiv  Detail & Related papers  (2021-03-28T03:35:24Z)
• BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks [7.844146033635129]
  We study verification problems for Binarized Neural Networks (BNNs), the 1-bit quantization of general real-numbered neural networks. Our approach is to encode BNNs into Binary Decision Diagrams (BDDs), which is done by exploiting the internal structure of the BNNs. Based on the encoding, we develop a quantitative verification framework for BNNs where precise and comprehensive analysis of BNNs can be performed.
  arXiv  Detail & Related papers  (2021-03-12T12:02:41Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.