神经网络的鲁棒性：一种概率与实践的方法

神经网络在软件中正变得日益普遍，因此能够验证其行为十分重要。由于验证神经网络的正确性极具挑战性，通常侧重于验证这些系统的其他性质。其中一个重要性质是鲁棒性。然而，大多数现有的鲁棒性定义关注于输入为对抗性的最坏情况场景。此类鲁棒性概念过于严格，实际神经网络不太可能满足且难以验证。观察到神经网络的实际输入来自非对抗性的概率分布，我们提出了一种新颖的鲁棒性概念：概率鲁棒性，它要求神经网络相对于输入分布以至少 $(1 - \epsilon)$ 的概率保持鲁棒。这种概率方法是实用的，并提供了一种估计神经网络鲁棒性的原则性方式。我们还提出了一种基于抽象解释和重要性采样的算法，用于检查神经网络是否具有概率鲁棒性。我们的算法使用抽象解释来近似神经网络的行为，并计算违反鲁棒性的输入区域的过近似。然后它使用重要性采样来抵消这种过近似的影响，并准确估计神经网络违反鲁棒性性质的概率。