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

  • 2022-05-16 18:37:23
  • Christopher A. Strong, Sydney M. Katz, Anthony L. Corso, Mykel J. Kochenderfer
  • 0

Abstract

Deep neural networks often lack the safety and robustness guarantees neededto be deployed in safety critical systems. Formal verification techniques canbe used to prove input-output safety properties of networks, but whenproperties are difficult to specify, we rely on the solution to variousoptimization problems. In this work, we present an algorithm called ZoPE thatsolves optimization problems over the output of feedforward ReLU networks withlow-dimensional inputs. The algorithm eagerly splits the input space, boundingthe objective using zonotope propagation at each step, and improvescomputational efficiency compared to existing mixed-integer programmingapproaches. We demonstrate how to formulate and solve three types ofoptimization problems: (i) minimization of any convex function over the outputspace, (ii) minimization of a convex function over the output of two networksin series with an adversarial perturbation in the layer between them, and (iii)maximization of the difference in output between two networks. Using ZoPE, weobserve a $25\times$ speedup on property $1$ of the ACAS Xu neural networkverification benchmark compared to several state-of-the-art verifiers, and an$85\times$ speedup on a set of linear optimization problems compared to amixed-integer programming baseline. We demonstrate the versatility of theoptimizer in analyzing networks by projecting onto the range of a generativeadversarial network and visualizing the differences between a compressed anduncompressed network.

 

Quick Read (beta)

loading the full paper ...