Strong mixed-integer programming formulations for trained neural networks
Ross Anderson Joey Huchette Will Ma Christian Tjandraatmadja Juan Pablo Vielma
Abstract
We present strong mixed-integer programming (MIP) formulations for high-dimensional piecewise linear functions that correspond to trained neural networks. These formulations can be used for a number of important tasks, such as verifying that an image classification network is robust to adversarial inputs, or solving decision problems where the objective function is a machine learning model. We present a generic framework, which may be of independent interest, that provides a way to construct sharp or ideal formulations for the maximum of $d$ affine functions over arbitrary polyhedral input domains. We apply this result to derive MIP formulations for a number of the most popular nonlinear operations (e.g. ReLU and max pooling) that are strictly stronger than other approaches from the literature. We corroborate this computationally, showing that our formulations are able to offer substantial improvements in solve time on verification tasks for image classification networks.
中文速览
用混合整数规划（Mixed-Integer Programming, MIP）来对训练好的神经网络进行优化或验证，是一个关键但困难的问题——现有方法普遍采用"大M"松弛技术，导致线性规划松弛不够紧，求解效率低下。本文提出了一个通用框架，能够为"多个仿射函数取最大值"这一结构（涵盖ReLU、最大池化等神经网络中最常见的非线性操作）构造理论上最强的"理想"或"遗传锐利"MIP公式，其线性松弛恰好等于原问题的凸包。将这一框架应用到ReLU网络后，新公式在理论上严格强于文献中所有已有方法，且能以线性时间完成分离运算（separation）。在MNIST图像分类网络的对抗鲁棒性验证实验中，新公式结合少量割平面分离，可将Gurobi求解时间缩短数个数量级。这项工作为神经网络优化与形式化验证提供了迄今最强的MIP建模工具，对自动驾驶等安全敏感场景中的可信AI保障具有重要意义。
原文 arXiv:1811.01988;中英对照 + 大白话阅读 https://aha.fim.ai/paper/1811.01988v4