确保你不确定：一个框架，用于确定概率规格
Make Sure You're Unsure: A Framework for Verifying Probabilistic Specifications
摘要：
大多数现实世界的应用需要处理随机性，如传感器噪声或预测不确定性，其中所需行为的正式规范本质上是概率性的。尽管形式化验证在保证神经网络的可靠性方面有希望，但在概率规范的方向上进展有限。在这个方向上，我们首先介绍了神经网络的概率规范的一般公式，它捕获了概率网络（例如，贝叶斯神经网络、MC-Dropout网络）和不确定输入（由传感器噪声或其他扰动引起的输入上的分布）。然后，我们提出了一个通用的技术来验证这样的规范，通过推广拉格朗日对偶的概念，取代标准拉格朗日乘数与“功能乘数”，可以是任意函数的激活在给定的层。我们表明，功能乘数的最佳选择导致精确的验证（即，健全和完整的验证），并为特定形式的乘法器，我们开发了易于处理的实用验证算法。我们通过将我们的算法应用于贝叶斯神经网络（BNN）和MC丢弃网络，并验证诸如对抗鲁棒性和对分布外（OOD）数据的鲁棒检测等属性，来经验性地验证我们的算法。在这些任务中，与以前的工作相比，我们能够提供更强的保证-例如，对于在CIFAR-10上训练的VGG-64 MC-Dropout CNN，我们改进了认证的AUC（真实AUC的验证下限），用于从$0\% \rightarrow 29\%$进行鲁棒的OOD检测（在CIFAR-100上）。类似地，对于在MNIST上训练的BNN，我们改进了来自$60.2\% \rightarrow 74.6\%$的鲁棒准确性。此外，在一个新的规范-分布鲁棒OOD检测-我们提高了认证的AUC从$5\% \rightarrow 23\%$。
英文摘要：
Most real world applications require dealing with stochasticity like sensor noise or predictive uncertainty, where formal specifications of desired behavior are inherently probabilistic. Despite the promise of formal verification in ensuring the reliability of neural networks, progress in the direction of probabilistic specifications has been limited. In this direction, we first introduce a general formulation of probabilistic specifications for neural networks, which captures both probabilistic networks (e.g., Bayesian neural networks, MC-Dropout networks) and uncertain inputs (distributions over inputs arising from sensor noise or other perturbations). We then propose a general technique to verify such specifications by generalizing the notion of Lagrangian duality, replacing standard Lagrangian multipliers with "functional multipliers" that can be arbitrary functions of the activations at a given layer. We show that an optimal choice of functional multipliers leads to exact verification (i.e., sound and complete verification), and for specific forms of multipliers, we develop tractable practical verification algorithms. We empirically validate our algorithms by applying them to Bayesian Neural Networks (BNNs) and MC Dropout Networks, and certifying properties such as adversarial robustness and robust detection of out-of-distribution (OOD) data. On these tasks we are able to provide significantly stronger guarantees when compared to prior work -- for instance, for a VGG-64 MC-Dropout CNN trained on CIFAR-10, we improve the certified AUC (a verified lower bound on the true AUC) for robust OOD detection (on CIFAR-100) from $0\% \rightarrow 29\%$. Similarly, for a BNN trained on MNIST, we improve on the robust accuracy from $60.2\% \rightarrow 74.6\%$. Further, on a novel specification -- distributionally robust OOD detection -- we improve the certified AUC from $5\% \rightarrow 23\%$.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
