Deep Neural Networks as 0-1 Mixed Integer Linear Programs: A Feasibility Study

Abstract

Deep Neural Networks (DNNs) are very popular these days, and are the subject of a very intense investigation. A DNN is made by layers of internal units (or neurons), each of which computes an affine combination of the output of the units in the previous layer, applies a nonlinear operator, and outputs the corresponding value (also known as activation). A commonly-used nonlinear operator is the so-called rectified linear unit (ReLU), whose output is just the maximum between its input value and zero. In this (and other similar cases like max pooling, where the max operation involves more than one input value), one can model the DNN as a 0-1 Mixed Integer Linear Program (0-1 MILP) where the continuous variables correspond to the output values of each unit, and a binary variable is associated with each ReLU to model its yes/no nature. In this paper we discuss the peculiarity of this kind of 0-1 MILP models, and describe an effective bound-tightening technique intended to ease its solution. We also present possible applications of the 0-1 MILP model arising in feature visualization and in the construction of adversarial examples. Preliminary computational results are reported, aimed at investigating (on small DNNs) the computational performance of a state-of-the-art MILP solver when applied to a known test case, namely, hand-written digit recognition.

submitted to an international conference

References in corpus (2)

• Intriguing properties of neural networks
• Bounding and Counting Linear Regions of Deep Neural Networks

Cited by in corpus (27)

• Efficient Neural Network Robustness Certification with General Activation Functions
• Provably Robust Deep Learning via Adversarially Trained Smoothed Classifiers
• Towards Fast Computation of Certified Robustness for ReLU Networks
• Automated Verification of Neural Networks: Advances, Challenges and Perspectives
• The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification
• NATTACK: Learning the Distributions of Adversarial Examples for an Improved Black-Box Attack on Deep Neural Networks
• Randomized Smoothing of All Shapes and Sizes
• Learning Security Classifiers with Verified Global Robustness Properties
• Towards Robust, Locally Linear Deep Networks
• Boosting Combinatorial Problem Modeling with Machine Learning
• Verification of Recurrent Neural Networks Through Rule Extraction
• Equivalent and Approximate Transformations of Deep Neural Networks
• Scalable Verification of GNN-based Job Schedulers
• On Training Robust PDF Malware Classifiers
• Improving the Tightness of Convex Relaxation Bounds for Training Certifiably Robust Classifiers
• Smart Feasibility Pump: Reinforcement Learning for (Mixed) Integer Programming
• Enhancing Certified Robustness via Smoothed Weighted Ensembling
• Towards Lower Bounds on the Depth of ReLU Neural Networks
• Accelerating Robustness Verification of Deep Neural Networks Guided by Target Labels
• Debona: Decoupled Boundary Network Analysis for Tighter Bounds and Faster Adversarial Robustness Proofs
• Traversing the Local Polytopes of ReLU Neural Networks: A Unified Approach for Network Verification
• Certified Defense via Latent Space Randomized Smoothing with Orthogonal Encoders
• ReLUSyn: Synthesizing Stealthy Attacks for Deep Neural Network Based Cyber-Physical Systems
• Dynamic Defense Approach for Adversarial Robustness in Deep Neural Networks via Stochastic Ensemble Smoothed Model
• Regularized Training and Tight Certification for Randomized Smoothed Classifier with Provable Robustness
• How Could Polyhedral Theory Harness Deep Learning?
• Approximating Optimisation Solutions for Travelling Officer Problem with Customised Deep Learning Network