ZoPE: A Fast Optimizer for ReLU Networks with Low-Dimensional Inputs

TL;DR

ZoPE is a novel, efficient algorithm for solving optimization problems over low-dimensional inputs of ReLU networks, significantly speeding up verification tasks and enabling new analysis methods.

Contribution

Introduces ZoPE, a fast optimizer for ReLU networks that uses zonotope propagation and input space splitting, outperforming existing mixed-integer programming methods.

Findings

25x speedup on ACAS Xu verification benchmark

85x faster on linear optimization problems

Enables new network analysis and visualization techniques

Abstract

Deep neural networks often lack the safety and robustness guarantees needed to be deployed in safety critical systems. Formal verification techniques can be used to prove input-output safety properties of networks, but when properties are difficult to specify, we rely on the solution to various optimization problems. In this work, we present an algorithm called ZoPE that solves optimization problems over the output of feedforward ReLU networks with low-dimensional inputs. The algorithm eagerly splits the input space, bounding the objective using zonotope propagation at each step, and improves computational efficiency compared to existing mixed-integer programming approaches. We demonstrate how to formulate and solve three types of optimization problems: (i) minimization of any convex function over the output space, (ii) minimization of a convex function over the output of two networks in series with an adversarial perturbation in the layer between them, and (iii) maximization of the difference in output between two networks. Using ZoPE, we observe a $25\times$ speedup on property $1$ of the ACAS Xu neural network verification benchmark compared to several state-of-the-art verifiers, and an $85\times$ speedup on a set of linear optimization problems compared to a mixed-integer programming baseline. We demonstrate the versatility of the optimizer in analyzing networks by projecting onto the range of a generative adversarial network and visualizing the differences between a compressed and uncompressed network.