By Pushmeet Kohli, Krishnamurthy (Dj) Dvijotham, Jonathan Uesato, Sven Gowal, and the Robust & Verified Deep Learning group. This article is cross-posted from DeepMind.com.
Translated by Xiaohu Zhu, University AI

Bugs 和软件自从计算机程序设计的开始就是形影相随的。经过一段时间后，软件开发者们已经建立了一个最佳的在部署之前测试和调试的实践集，但是这些实践对现代深度学习系统并不太适用。今天，在机器学习领域的广泛实践是在一个训练数据集上训练系统，然后在另一个集合上进行测试。虽然这揭示了模型的平均情况性能，但即使在最坏的情况下，确保健壮性或可接受的高性能也是至关重要的。在本文中，我们描述了三种严格识别和消除学习到的预测模型中错误的方法：对抗性测试，健壮学习和形式验证。

机器学习系统默认不太健壮。即使在特定领域中表现优于人类的系统，如果引入微妙差异，也可能无法解决简单问题。例如，考虑图像扰动的问题：如果在输入图像中添加少量精心计算的噪声，那么比人类更好地对图像进行分类的神经网络会轻易地误以为树懒是赛车。

这不是一个全新的问题。计算机程序总是有 bugs。几十年来，软件工程师汇集了令人印象深刻的技术工具包，从单元测试到形式验证。这些方法在传统软件上运行良好，但是由于这些模型的规模和结构的缺乏（可能包含数亿个参数），因此采用这些方法来严格测试神经网络等机器学习模型是非常具有挑战性的。这需要开发用于确保机器学习系统在部署时健壮的新方法。

从程序员的角度来看，错误是与系统的规范（即预期功能）不一致的任何行为。作为我们解决智能问题的使命的一部分，我们对用于评估机器学习系统是否与训练集和测试集一致，以及描述系统的期望属性的规格列表的技术进行研究。这些属性可能包括对输入中足够小的扰动的健壮性，避免灾难性故障的安全约束，或产生符合物理定律的预测。

在本文中，我们将讨论机器学习社区面临的三个重要技术挑战，因为我们共同致力于严格地开发和部署与所需规格可靠一致的机器学习系统：

1. 有效地测试与规范的一致性。我们探索有效的方法来测试机器学习系统是否与设计者和系统用户所期望的属性（例如不变性或健壮性）一致。揭示模型可能与期望行为不一致的情况的一种方法是在评估期间系统地搜索最坏情况的结果。
2. 训练机器学习模型是与规格一致的。即使有大量的训练数据，标准的机器学习算法也可以产生预测模型，使预测与健壮性或公平型等理想规格不一致 —— 这要求我们重新考虑训练算法，这些算法不仅能够很好地拟合训练数据，而且能够与规格清单一致。
3. 形式证明机器学习模型是规格一致的。需要能够验证模型预测可证明与所有可能输入的感兴趣的规格一致的算法。虽然形式验证领域几十年来一直在研究这种算法，尽管这些方法取得了令人瞩目的进展，但却不能轻易地扩展到现代深度学习系统

与规格的一致性测试

对抗性例子的稳健性是深度学习中相对充分被研究的问题。这项工作的一个主要主题是评估强攻击的重要性，以及设计可以有效分析的透明模型。与社区的其他研究人员一起，我们发现许多模型在与弱对手进行评估时看起来很健壮。然而，当针对更强的对手进行评估时，它们显示出基本上0％的对抗准确率（Athalye等，2018，Uesato等，2018，Carlini和Wagner，2017）。

虽然大多数工作都集中在监督学习（主要是图像分类）的背景下的罕见失败，但是需要将这些想法扩展到其他设置。在最近关于揭示灾难性失败的对抗方法的工作中，我们将这些想法应用于测试旨在用于安全关键环境的强化学习智能体（Ruderman等，2018，Uesato等，2018b）。开发自治系统的一个挑战是，由于单个错误可能会产生很大的后果，因此非常小的失败概率也是不可接受的。

我们的目标是设计一个“对手”，以便我们提前检测这些故障（例如，在受控环境中）。如果攻击者可以有效地识别给定模型的最坏情况输入，则允许我们在部署模型之前捕获罕见的故障情况。与图像分类器一样，针对弱对手进行评估会在部署期间提供错误的安全感。这类似于红队的软件实践，虽然超出了恶意攻击者造成的失败，并且还包括自然出现的失败，例如由于缺乏泛化。

我们为强化学习智能体的对抗性测试开发了两种互补的方法。首先，我们使用无导数优化来直接最小化智能体的期望奖励。在第二部分中，我们学习了一种对抗值函数，该函数根据经验预测哪种情况最有可能导致智能体失败。然后，我们使用此学习函数进行优化，将评估重点放在最有问题的输入上。这些方法只构成了丰富且不断增长的潜在算法空间的一小部分，我们对严格评估智能体的未来发展感到兴奋。

这两种方法已经比随机测试产生了很大的改进。使用我们的方法，可以在几分钟内检测到需要花费数天才能发现甚至完全未被发现的故障（Uesato等，2018b）。我们还发现，对抗性测试可能会发现我们的智能体中的定性不同行为与随机测试集的评估结果不同。特别是，使用对抗性环境构造，我们发现执行 3D 导航任务的智能体平均与人类水平的性能相匹配，但令人诧异的是它仍然无法在简单迷宫上完全找到目标（Ruderman等，2018）。我们的工作还强调，需要设计能够抵御自然故障的系统，而不仅仅是针对对手

训练规格一致的模型

对抗性测试旨在找到违反规格的反例。因此，它往往会导致高估模型与这些规格的一致性。在数学上，规格是必须在神经网络的输入和输出之间保持的某种关系。这可以采用某些关键输入和输出参数的上界和下界的形式。

受此观察的启发，一些研究人员（Raghunathan 等，2018; Wong 等，2018; Mirman 等，2018; Wang 等，2018），包括我们在 DeepMind 的团队（Dvijotham 等，2018; Gowal 等，2018），研究了与对抗性测试程序无关的算法（用于评估与规范的一致性）。这可以从几何学上理解 —— 我们可以约束（例如，使用区间界限传播; Ehlers 2017，Katz 等人 2017，Mirman 等人，2018）通过在给定一组输入的情况下限制输出空间来最严重地违反规格。如果此界关于网络参数是可微分的并且可以快速计算，则可以在训练期间使用它。然后可以通过网络的每个层传播原始边界框。

我们证明了区间界传播是快速、有效的并且 —— 与先前的信念相反 —— 可以获得强有力的结果（Gowal 等，2018）。特别地，我们证明它可以降低 MNIST 和 CIFAR-1 数据集上的图像分类中的现有技术的可证明的错误率（即，任何对手可实现的最大错误率）。

展望未来，下一个前沿将是学习正确的几何抽象，以计算更严格的输出空间过度近似。我们还希望训练网络与更复杂的规格一致，捕获理想的行为，例如上面提到的不变性和与物理定律的一致性。

形式验证

严格的测试和训练可以大大有助于构建强大的机器学习系统。但是，没有多少测试可以正式保证系统的行为符合我们的要求。在大规模模型中，由于输入扰动的选择具有天文数字，因此列举给定输入集的所有可能输出（例如，对图像的无穷小扰动）是难以处理的。但是，与训练的情况一样，我们可以通过在输出集上设置几何边界来找到更有效的方法。形式验证是 DeepMind 正在进行的研究的主题。

机器学习社区已经开发了几个关于如何计算网络输出空间上的精确几何边界的有趣想法（Katz 等人 2017，Weng 等人，2018; Singh 等人，2018）。我们的方法（Dvijotham 等人，2018）基于优化和二元性，包括将验证问题制定为优化问题，试图找到被验证属性的最大违规。通过在优化中使用二元性的思想，该问题变得易于计算。这导致额外的约束，其使用所谓的切割平面来细化由间隔界限传播计算的边界框。这种方法虽然合理但不完整：可能存在感兴趣的属性为真的情况，但此算法计算的界限不足以证明该属性。但是，一旦我们获得了约束，这正式保证不会违反财产。下图以图形方式说明了该方法。

这种方法使我们能够将验证算法的适用性扩展到更一般的网络（激活函数和体系结构），一般规范和更复杂的深度学习模型（生成模型和神经过程等）和超越对抗性健壮性的规格（Qin，2018）。

展望

在高风险情况下部署机器学习带来了独特的挑战，并且需要开发可靠地检测不太可能的故障模式的评估技术。更广泛地说，我们认为学习与规格的一致性可以提供比仅仅从训练数据隐含地产生规格的方法的效率提高。我们对正在进行的对抗性评估、学习健壮模型和形式规格验证的研究感到非常兴奋。

需要做更多的工作来构建自动化工具，以确保现实世界中的 AI 系统能够做出“正确的事情”。特别是，我们对以下方向的进展感到兴奋：

1. 学习对抗性评估和验证：随着 AI 系统的规模化和变得越来越复杂，设计良好地适应的 AI 模型的对抗性评估和验证算法将变得越来越困难。如果我们可以利用 AI 的强大功能来促进评估和验证，那么这个过程可以进行自举规模化起来。
2. 开发用于对抗性评估和验证的公开工具：为 AI 工程师和从业者提供易于使用的工具非常重要，这些工具可以在 AI 系统导致广泛的负面影响之前阐明其可能的故障模式。这需要一定程度的对抗性评估和验证算法的标准化。
3. 扩大对抗性示例的范围：到目前为止，大多数关于对抗性示例的工作都集中在对小扰动（通常是图像）的模型不变性上。这为开发对抗性评估、健壮学习和验证方法提供了极好的测试平台。我们已经开始探索与现实世界直接相关的属性的替代规格，并对未来在这方面的研究感到兴奋。
4. 学习规范：在 AI 系统中捕获“正确”行为的规格通常难以精确陈述。当我们构建能够展示复杂行为并在非结构化环境中行动地越来越智能的智能体时，将需要构建可以使用部分人类规格并从评估反馈中学习进一步规格的系统。

DeepMind 致力于通过负责任的研发和部署机器学习系统来产生积极的社会影响。为了确保开发人员的贡献可靠，我们需要应对许多技术挑战。我们致力于参与这项工作，并很高兴与社区合作解决这些挑战。

This post describes the work of the Robust and Verified Deep Learning group (Pushmeet Kohli, DJ Krishnamurthy, Jonathan Uesato, Sven Gowal, Chongli Qin, Robert Stanforth, Po-Sen Huang) performed in collaboration with various contributors across DeepMind including Avraham Ruderman, Alhussein Fawzi, Ananya Kumar, Brendan O’Donoghue, Bristy Sikder, Chenglong Wang, Csaba Szepesvari, Hubert Soyer, Relja Arandjelovic, Richard Everett, Rudy Bunel, Timothy Mann, and Tom Erez. Thanks to Vishal Maini, Aleš Flidr, Damien Boudot, and Jan Leike for their contributions to the post.