【ETHZ博士论文】神经网络训练与认证，101页pdf

确保神经网络系统在关键任务应用中的安全性和可信度是其安全采用的关键。然而，尽管付出了大量努力，训练满足这些安全和可信属性的网络以及验证它们是否满足这些属性仍然是未解决的挑战。在本论文中，我们解决了这些挑战，并展示了它们是密切相关的。我们提出了两种新颖的神经网络验证方法，PRIMA和MN-BAB，在可扩展性和精度方面推动了神经网络验证的界限。然后，我们提出了一种新的认证训练方法SABR，利用这些更精确的验证方法，通过减少（过度）正则化来提高标准和认证准确性。

由于神经网络验证一般是NP完全的，大多数验证器通过引入非线性激活函数的过度近似来放松基础优化问题。PRIMA和MN-BAB的关键组件是多神经元松弛的高效计算和执行，该方法联合近似多个激活函数，而不是单独近似，从而捕捉复杂的相互依赖性并显著提高紧密性。为此，我们提出了SBLM，这是一种新的方法，通过将基础凸包问题分解为低维度来降低维度，和PDDM，一种具有多项式复杂性和低维度精确保证的近似凸包计算算法。我们将这些结合在PRIMA中，这是一种新的不完全神经网络验证器，将生成的多神经元约束纳入验证问题的LP公式中，并用CPU求解器求解。由于该求解器限制了PRIMA的可扩展性，我们提出了基于分支定界范式的完全验证器MN-BAB，该方法利用拉格朗日乘数法在完全GPU和高度并行化的验证器中强制执行我们的多神经元约束。我们显示MN-BAB在神经网络验证方面达到了新的最先进水平，将困难属性的验证速度提高了多达30倍。

尽管在神经网络验证方面取得了进展，但仍需要专门的训练方法来获得具有可证明保证的神经网络。然而，大多数这些认证训练方法通过优化最坏情况行为的保守边界，从而引起强烈的（过度）正则化，因此只能以标准性能为代价来实现可认证性。为了解决这一问题，我们引入了不健全认证训练范式及其第一个相应方法SABR。这一范式背后的关键见解是优化最坏情况损失的不健全但期望精确的近似，而不是健全的过度近似，以在不引起过度正则化的情况下实现鲁棒性。SABR通过传播小而精心选择的对抗性输入区域子集的区间边界来实现这一点。我们在广泛的实证评估中表明，SABR在不同扰动幅度和数据集上，在标准和可认证准确性方面均优于现有的认证防御方法，突出了不健全认证训练方法在缓解鲁棒性-准确性权衡方面的潜力。