We introduce two algorithms for computing tight guarantees on the probabilistic robustness of Bayesian Neural Networks (BNNs). Computing robustness guarantees for BNNs is a significantly more challenging task than verifying the robustness of standard Neural Networks (NNs) because it requires searching the parameters' space for safe weights. Moreover, tight and complete approaches for the verification of standard NNs, such as those based on Mixed-Integer Linear Programming (MILP), cannot be directly used for the verification of BNNs because of the polynomial terms resulting from the consecutive multiplication of variables encoding the weights. Our algorithms efficiently and effectively search the parameters' space for safe weights by using iterative expansion and the network's gradient and can be used with any verification algorithm of choice for BNNs. In addition to proving that our algorithms compute tighter bounds than the SoA, we also evaluate our algorithms against the SoA on standard benchmarks, such as MNIST and CIFAR10, showing that our algorithms compute bounds up to 40% tighter than the SoA.

翻译：我们提出了两种算法，用于计算贝叶斯神经网络（BNN）概率鲁棒性的严格保证。与标准神经网络（NN）的鲁棒性验证相比，BNN的鲁棒性保证计算更具挑战性，因为需要搜索参数空间以找到安全权重。此外，标准神经网络的严格且完备的验证方法（例如基于混合整数线性规划的方法）无法直接用于BNN验证，因为其中涉及编码权重的变量连续相乘所导致的多项式项。我们的算法通过迭代扩展和网络梯度，高效且有效地搜索参数空间中的安全权重，并可配合任何BNN验证算法使用。除证明我们的算法能计算出比现有最优方法更紧的界外，我们还在MNIST和CIFAR10等标准基准上对算法进行了评估，结果表明我们的算法计算出的界比现有最优方法紧达40%。