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

• URL: http://arxiv.org/abs/2203.07078v1
• Date: Fri, 11 Mar 2022 01:11:29 GMT
• Title: A Mixed Integer Programming Approach for Verifying Properties of Binarized Neural Networks
• Authors: Christopher Lazarus and Mykel J. Kochenderfer
• Abstract summary: 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.
• Score: 44.44006029119672
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• 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)
• Harnessing Neuron Stability to Improve DNN Verification [42.65507402735545]
  We present VeriStable, a novel extension of recently proposed DPLL-based constraint DNN verification approach. We evaluate the effectiveness of VeriStable across a range of challenging benchmarks including fully-connected feed networks (FNNs), convolutional neural networks (CNNs) and residual networks (ResNets) Preliminary results show that VeriStable is competitive and outperforms state-of-the-art verification tools, including $alpha$-$beta$-CROWN and MN-BaB, the first and second performers of the VNN-COMP, respectively.
  arXiv  Detail & Related papers  (2024-01-19T23:48:04Z)
• 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)
• You Can Have Better Graph Neural Networks by Not Training Weights at All: Finding Untrained GNNs Tickets [105.24703398193843]
  Untrainedworks in graph neural networks (GNNs) still remains mysterious. We show that the found untrainedworks can substantially mitigate the GNN over-smoothing problem. We also observe that such sparse untrainedworks have appealing performance in out-of-distribution detection and robustness of input perturbations.
  arXiv  Detail & Related papers  (2022-11-28T14:17:36Z)
• Recurrent Bilinear Optimization for Binary Neural Networks [58.972212365275595]
  BNNs neglect the intrinsic bilinear relationship of real-valued weights and scale factors. Our work is the first attempt to optimize BNNs from the bilinear perspective. We obtain robust RBONNs, which show impressive performance over state-of-the-art BNNs on various models and datasets.
  arXiv  Detail & Related papers  (2022-09-04T06:45:33Z)
• Sub-bit Neural Networks: Learning to Compress and Accelerate Binary Neural Networks [72.81092567651395]
  Sub-bit Neural Networks (SNNs) are a new type of binary quantization design tailored to compress and accelerate BNNs. SNNs are trained with a kernel-aware optimization framework, which exploits binary quantization in the fine-grained convolutional kernel space. Experiments on visual recognition benchmarks and the hardware deployment on FPGA validate the great potentials of SNNs.
  arXiv  Detail & Related papers  (2021-10-18T11:30:29Z)
• Neural Network Branch-and-Bound for Neural Network Verification [26.609606492971967]
  We propose a novel machine learning framework that can be used for designing an effective branching strategy. We learn two graph neural networks (GNNs) that both directly treat the network we want to verify as a graph input. We show that our GNN models generalize well to harder properties on larger unseen networks.
  arXiv  Detail & Related papers  (2021-07-27T14:42:57Z)
• 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)
• S2-BNN: Bridging the Gap Between Self-Supervised Real and 1-bit Neural Networks via Guided Distribution Calibration [74.5509794733707]
  We present a novel guided learning paradigm from real-valued to distill binary networks on the final prediction distribution. Our proposed method can boost the simple contrastive learning baseline by an absolute gain of 5.515% on BNNs. Our method achieves substantial improvement over the simple contrastive learning baseline, and is even comparable to many mainstream supervised BNN methods.
  arXiv  Detail & Related papers  (2021-02-17T18:59:28Z)
• Encoding the latent posterior of Bayesian Neural Networks for uncertainty quantification [10.727102755903616]
  We aim for efficient deep BNNs amenable to complex computer vision architectures. We achieve this by leveraging variational autoencoders (VAEs) to learn the interaction and the latent distribution of the parameters at each network layer. Our approach, Latent-Posterior BNN (LP-BNN), is compatible with the recent BatchEnsemble method, leading to highly efficient (in terms of computation and memory during both training and testing) ensembles.
  arXiv  Detail & Related papers  (2020-12-04T19:50:09Z)

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.