近期，将对机器学习的功能性性质，比如：可解释性(透明性)，可验证性(可信的)，可组合性(可拓展性)，鲁棒性等等，在这方面进行讨论。我目前在看这篇论文，此外会相应地对一些知识进行补充了解。
An Abstract Domain for Certifying Neural Networks(对神经网络认证的一种抽象Domain)
具体参考：在计算机领域里Domain指的是什么？
Abstract：
提出新的神经网络可扩展性(scalable)和精确性(precise)的证明方法，这种方法背后是一种新的抽象Domain，其结合了带间隔的浮点多面体(float point polyhedra with intervals)，并配备了专门为神经网络设置的抽象变压器(abstract transformer)。具体地讲，这个变压器是for(为了)affine transform，the rectifed linear unit (ReLU)，sigmoid, tanh, and maxpool functions.这个方法在DeepPoly的系统中是实现了，并在一系列数据集、神经架构(包括防御网络)和规范(specifcations)上对其进行了广泛的评估。我们的实验结果表明，在扩展到大型网络时，DeepPoly比以前的工作更精确。我们还展示了如何将DeepPoly与基于跟踪分区的抽象引用形式(a form of abstraction refnement based on trace partitioning)相结合。这使我们能够首次证明，当输入图像受到复杂的扰动时，如采用线性插值的旋转，网络的鲁棒性。(rotations that employ linear interpolation).
在过去的几年里，深层神经网络已经变得越来越流行，现在已经开始渗透到安全的关键领域，如自动驾驶和医学诊断，在这些领域中，人们常常依赖它们来做出重要的决策。由于这种广泛采用，确保神经网络的行为可靠和符合预期变得更加重要。不幸的是，由于这些系统的黑箱性质，对其进行推理是具有挑战性的：很难理解网络的功能，因为它通常由难以解释的数千或数百万实值权重参数化。此外，人们还发现，神经网络有时会异常脆弱，表现出非鲁棒性行为，例如，将两个非常相似的输入(例如，亮度或一个像素不同的图像)分类到不同的标签。为了解决神经网络推理的挑战，最近的研究已经开始探索新的方法和系统，这些方法和系统可以自动证明给定的网络满足特定的兴趣特性(例如，对某些扰动的鲁棒性，前/后条件)。尽管这些工作取得了一定的进展，但是要想成功地解决整个神经网络的推理挑战还需要更多的研究。特别是，我们仍然缺乏一个可以扩展到大型网络的分析器，它能够处理流行的神经结构(例如前馈、卷积)，而且还非常精确地证明了应用程序所需的相关属性。
论文中提到的前人的工作：
自动定义性质：基于SMT方案：https://ai.yanxishe.com/page/blogDetail/5573 （论文1）
基于linear approximations线性逼近：https://arxiv.org/pdf/1804.09699.pdf（ReLU Networks，论文2）
基于abstract interpretation抽象解释：这里引用了3篇论文（论文3,4,5）
作者比较论文1处理小型网络比较精确（浅层网络？）论文3处理的网络比论文1要更大，但它依赖于现有的通用抽象域，这些域既不能扩展到更大的神经网络（原文翻译，引用了一个更大的网络）或者说不是很精确。论文2处理的比论文3要好，但只能处理前馈网络，对于卷积网络没有进行处理。论文1,2不能很好处理浮点算法。论文5处理浮点算法很好，但处理较大扰动时候不够精确（鲁棒性较差咯？）
在这项工作中，我们提出了一种新的方法和系统，称为DeepPoly，它在解决验证神经网络的可扩展性和准确性方面的挑战方面向前迈出了一步。DeepPoly背后的关键技术思想是一种专门针对神经网络设置的新型抽象解释器。具体地说(见abstract）这些抽象的转换器经过精心设计，以利用这些函数的关键特性，平衡分析的可伸缩性和精确性。
这篇论文如何证明鲁棒性：举例了2种扰动。为了直观地理解DeepPoly可以解决的问题，请考虑fig.1所示的图像。在这里，我们将说明两种鲁棒性:基于L范数的摄动(第一行)和图像旋转(第二行)。具体参考：什么是L范数扰动和图像选择？
Fig. 1. Two different atacks applied to MNIST images.
这篇论文的主要贡献：
神经网络认证的一个新的抽象领域。该域将基于间隔的浮点多面体与自定义抽象转换器结合在一起。这些抽象的变压器仔细地平衡了分析的可扩展性和精确性(第4节)。
一种证明比目前考虑的更复杂的扰动特性的方法，包括基于抽象输入的线性插值的旋转。据我们所知，这是第一次验证这种扰动(第5节)
我们的方法在一个名为DeepPoly的系统中得到了完整的并行实现，该系统可以处理前馈和卷积神经网络，对一系列数据集和网络(包括防御数据集和网络)的广泛评估表明，DeepPoly比以前的工作更精确，但可以扩展到大型网络(第6节)
我们相信DeepPoly是解决神经网络推理挑战的一个有前途的步骤，也是证明复杂的特性(例如旋转)和其他分析应用的有用的构建块。例如，在培训过程中使用我们的分析是未来应用程序的一个很有前途的方向。特别地，因为我们的神经元输出的抽象转换器是“点向的”(即，可以并行计算)。我们可以直接将这些变压器插入最新的系统中，这些系统使用GPU上的抽象解释来训练神经网络。由于我们的变压器比Mirman等[2018]的变压器精度高得多，我们希望它们能够帮助提高经过训练的网络的整体鲁棒性。
overview：
在本节中，我们通过一个简单的说明性示例概述了我们的抽象领域。在具有ReLU激活的前馈网络上运行示例。我们考虑如图2所示的具有ReLU激活的简单全连通前馈神经网络。这个网络已经被训练过了，我们已经在fgure中显示了学习的权重。网络由四层组成:输入层、隐藏层和输出层，各有两个神经元。边缘上的权值代表了在每一层进行的affine变换所使用的权值矩阵的已知系数。注意，这些值通常是详细的浮点数(例如0.031)，但是，这里我们使用整数来简化表示。每个神经元的习得偏误显示在它的上方或下方。一层的所有偏差构成了affine变换的平移向量。
网友评论