确保你不确定:一个验证概率规范的框架

大多数现实世界应用需要处理随机性,如传感器噪声或预测不确定性,其中期望行为的形式化规范本质上是概率性的。尽管形式化验证在确保神经网络可靠性方面前景广阔,但在概率规范方向上的进展有限。在此方向上,我们首先引入神经网络概率规范的一般表述,其涵盖了概率网络(例如贝叶斯神经网络、MC-Dropout 网络)与不确定输入(由传感器噪声或其他扰动产生的输入分布)。然后我们提出一种验证此类规范的一般技术,通过推广 Lagrangian 对偶的概念,将标准 Lagrangian 乘子替换为可以是给定层激活值任意函数的“函数乘子”。我们证明函数乘子的最优选择导致精确验证(即可靠且完备的验证),并且对于特定形式的乘子,我们开发了可处理的实用验证算法。我们通过将算法应用于贝叶斯神经网络(BNNs)和 MC Dropout 网络,并认证诸如对抗鲁棒性和分布外(OOD)数据的鲁棒检测等性质,在经验上验证了我们的算法。在这些任务上,与先前工作相比我们能够提供更强的保证——例如,对于在 CIFAR-10 上训练的 VGG-64 MC-Dropout CNN,我们将鲁棒 OOD 检测(在 CIFAR-100 上)的认证 AUC(真实 AUC 的验证下界)从 $0\% \rightarrow 29\%$ 提升。类似地,对于在 MNIST 上训练的 BNN,我们将鲁棒准确率从 $60.2\% \rightarrow 74.6\%$ 提升。此外,在一个新规范——分布鲁棒 OOD 检测上,我们将认证 AUC 从 $5\% \rightarrow 23\%$ 提升。