Prior work on neural network verification has focused on specifications that
are linear functions of the output of the network, e.g., invariance of the
classifier output under adversarial perturbations of the input. In this paper,
we extend verification algorithms to be able to certify richer properties of
neural networks. To do this we introduce the class of convex-relaxable
specifications, which constitute nonlinear specifications that can be verified
using a convex relaxation. We show that a number of important properties of
interest can be modeled within this class, including conservation of energy in
a learned dynamics model of a physical system; semantic consistency of a
classifier's output labels under adversarial perturbations and bounding errors
in a system that predicts the summation of handwritten digits. Our experimental
evaluation shows that our method is able to effectively verify these
specifications. Moreover, our evaluation exposes the failure modes in models
which cannot be verified to satisfy these specifications. Thus, emphasizing the
importance of training models not just to fit training data but also to be
consistent with specifications.

本文介绍在神经网络验证中如何利用凸松弛来证明一系列比较丰富的非线性规约，包括物理系统学习到的动力学模型的能量守恒，分类器的输出标签在对抗性扰动下的语义一致性以及预测手写数字求和的系统所包含的误差等，实验验证了该方法的有效性。