On Integer Programming for the Binarized Neural Network Verification Problem
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
A Mixed Integer Programming Approach for Verifying Properties of Binarized Neural Networks
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 studie…
Collision AvoidanceModel CompressionNeural Network Verification as Piecewise Linear Optimization: Formulations for the Composition of Staircase Functions
We present a technique for neural network verification using mixed-integer programming (MIP) formulations. We derive a \emph{strong formulation} for each neuron in a network using piecewise linear activation functions. A…
Efficient and Robust Mixed-Integer Optimization Methods for Training Binarized Deep Neural Networks
Compared to classical deep neural networks its binarized versions can be useful for applications on resource-limited devices due to their reduction in memory consumption and computational demands. In this work we study d…
Taming Binarized Neural Networks and Mixed-Integer Programs
There has been a great deal of recent interest in binarized neural networks, especially because of their explainability. At the same time, automatic differentiation algorithms such as backpropagation fail for binarized n…
Training Experimentally Robust and Interpretable Binarized Regression Models Using Mixed-Integer Programming
In this paper, we explore model-based approach to training robust and interpretable binarized regression models for multiclass classification tasks using Mixed-Integer Programming (MIP). Our MIP model balances the optimi…
Classificationregression