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.
翻译:深心神经网络往往缺乏安全临界系统中需要部署的安全性和稳健性保障。 正式的核查技术可以用来证明网络的输入- 输出安全性, 但是当特性难以指定时, 我们依赖各种优化问题的解决方案。 在这项工作中, 我们提出了一个叫做 ZOPE 的算法, 解决在Feedforward ReLU网络输出上最优化的问题, 并带有低维输入。 算法急切地分割输入空间, 将每个步骤使用zonootope传播的目标捆绑在一起, 并改进计算效率, 与现有的混合整数英吋编程方法相比。 我们展示了如何制定和解决三种最优化问题:(一) 最大限度地减少产出空间上的任何convex功能;(二) 最大限度地减少两个网络系列输出的 convex功能, 并在两个网络的平面上进行对抗性扰动。 使用ZoPE, 我们观察到在ACAS Xulu 网络的房地产价格不一美元方面, 我们观察到一个25\timetal 的直观性网络的加速速度, 对比一个Slimalimalalalal- trainaltial- tralial- transilal- translational- transalitional- salitionaltialational