【牛津大学博士论文】高效的神经网络验证与训练，244页pdf

尽管神经网络在各种应用中的高度公开化的成就备受瞩目，但它们尚未在安全关键的应用中得到广泛部署。实际上，关于深度学习系统的鲁棒性、公平性、隐私性和可解释性存在基本的疑虑。在这篇论文中，我们致力于通过提出有关神经网络验证和训练的贡献，提高对深度学习系统的信任。首先，通过为流行的网络松弛设计双重求解器，我们提供了快速且可扩展的神经网络输出边界。具体来说，我们提出了两种求解元素激活函数凸壳的求解器，以及基于ReLU激活与前线性层组合凸壳的两种算法。我们展示了这些方法比现有求解器明显快，并且改善了以往双重算法的速度-精度权衡。为了有效地利用它们进行正式的神经网络验证，我们围绕边界算法设计了一个大规模并行的分枝定界框架。我们的贡献，作为OVAL验证框架的一部分，已经公开发布，它们改善了现有网络验证器的可扩展性，并对更近期的算法开发产生了影响。其次，我们提出了一种直观且经济的算法，通过分枝定界来训练神经网络以进行可验证性。我们的方法被证明可以在验证对小的敌对性扰动的鲁棒性方面达到最先进的性能，同时比之前的算法降低了训练成本。最后，我们进行了全面的实验评估，评估了一次训练网络执行多个任务的专门训练方案，显示它们与简单基线的性能相当。我们对我们的惊人结果提供了部分解释，旨在进一步激发对深度多任务学习理解的研究。

在过去的几年里，神经网络在各种备受关注的应用中取得了显著的性能，从蛋白质折叠（Senior等人，2020；Jumper等人，2021）到快速矩阵乘法（Fawzi等人，2022）。由于这些成就的宣传，基于神经网络的系统现在常常出现在主流信息媒体中（Geddes，2022；Larousserie，2022；Iannaccone，2022），这导致了媒体曝光率的持续增加。直接的结果是，人们对机器学习算法的可信度产生了极大的兴趣（Varshney，2022）。特别的，人们的努力已经朝着确保神经网络的公平性（Du等人，2020），可解释性（Angelov和Soares，2020），鲁棒性（Carlini和Wagner，2017）和隐私性（Abadi等人，2016）方向发展。深度学习在计算机视觉方面的进展（Krizhevsky等人，2012；Voulodimos等人，2018）尤其迅速，其中已经在标准化任务上取得了超过人类的性能（O’Mahony等人，2019）。然而，对敌对性例子的发现（Szegedy等人，2014；Goodfellow等人，2015），即人类无法察觉的扰动可以显著改变网络预测，对这种进步的基础产生了严重的质疑。因此，越来越多的注意力开始致力于提供关于神经网络行为的正式保证（Liu等人，2021b）。此外，人们注意到深度学习的实践常常基于民间观察和固定的流程，而不是对正在使用的复杂算法的严谨理解（Sculley等人，2018；Hutson，2018）。幸运的是，有许多工作试图提供对预先存在的算法的全面评估（Greff等人，2017；Lucic等人，2018），常常揭示了更简单基线的竞争性能（Brockschmidt，2020；Narang等人，2021）。 在这篇论文中，我们通过开发或为神经网络验证和训练的高效算法提供支持，向可信任的深度学习迈进一步。在概述这篇论文中提出的各项贡献（§1.4）之前，我们现在将介绍神经网络验证（§1.2）以及我们感兴趣的背景下的神经网络训练（§1.3）。