神经网络非线性规范的验证
Verification of Non-Linear Specifications for Neural Networks
摘要：
关于神经网络验证的先前工作集中于作为网络输出的线性函数的规范，例如，在输入的对抗扰动下分类器输出的不变性。在本文中，我们扩展验证算法，能够证明更丰富的神经网络的属性。要做到这一点，我们介绍了类的凸松弛规格，构成非线性规格，可以使用凸松弛验证。我们表明，一些重要的属性感兴趣的可以在这一类建模，包括能量守恒的物理系统的学习动力学模型;语义一致性的分类器的输出标签下的对抗扰动和边界错误的系统，预测手写数字的总和。我们的实验评估表明，我们的方法是能够有效地验证这些规格。此外，我们的评估暴露了模型中无法验证以满足这些规范的失效模式。因此，强调训练模型的重要性不仅要适合训练数据，而且要与规范一致。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
