In this paper, we introduce BNN-DP, an efficient algorithmic framework for
analysis of adversarial robustness of Bayesian Neural Networks (BNNs). Given a
compact set of input points $T\subset \mathbb{R}^n$, BNN-DP computes lower and
upper bounds on the BNN's predictions for all the points in $T$. The framework
is based on an interpretation of BNNs as stochastic dynamical systems, which
enables the use of Dynamic Programming (DP) algorithms to bound the prediction
range along the layers of the network. Specifically, the method uses bound
propagation techniques and convex relaxations to derive a backward recursion
procedure to over-approximate the prediction range of the BNN with piecewise
affine functions. The algorithm is general and can handle both regression and
classification tasks. On a set of experiments on various regression and
classification tasks and BNN architectures, we show that BNN-DP outperforms
state-of-the-art methods by up to four orders of magnitude in both tightness of
the bounds and computational efficiency.

本文介绍了 BNN-DP，它是一种用于分析贝叶斯神经网络的对抗鲁棒性的高效算法框架。该算法使用动态规划算法来限定网络的预测范围，同时具备一般性和高效性。

BNN-DP: 通过动态规划对贝叶斯神经网络进行鲁棒性认证

BNN-DP: Robustness Certification of Bayesian Neural Networks via Dynamic  Programming

Bound propagation methods, when combined with branch and bound, are among the
most effective methods to formally verify properties of deep neural networks
such as correctness, robustness, and safety. However, existing works cannot
handle the general form of cutting plane constraints widely accepted in
traditional solvers, which are crucial for strengthening verifiers with
tightened convex relaxations. In this paper, we generalize the bound
propagation procedure to allow the addition of arbitrary cutting plane
constraints, including those involving relaxed integer variables that do not
appear in existing bound propagation formulations. Our generalized bound
propagation method, GCP-CROWN, opens up the opportunity to apply general
cutting plane methods for neural network verification while benefiting from the
efficiency and GPU acceleration of bound propagation methods. As a case study,
we investigate the use of cutting planes generated by off-the-shelf mixed
integer programming (MIP) solver. We find that MIP solvers can generate
high-quality cutting planes for strengthening bound-propagation-based verifiers
using our new formulation. Since the branching-focused bound propagation
procedure and the cutting-plane-focused MIP solver can run in parallel
utilizing different types of hardware (GPUs and CPUs), their combination can
quickly explore a large number of branches with strong cutting planes, leading
to strong verification performance. Experiments demonstrate that our method is
the first verifier that can completely solve the oval20 benchmark and verify
twice as many instances on the oval21 benchmark compared to the best tool in
VNN-COMP 2021, and also noticeably outperforms state-of-the-art verifiers on a
wide range of benchmarks. GCP-CROWN is part of the $\alpha,\!\beta$-CROWN
verifier, the VNN-COMP 2022 winner. Code is available at
this http URL

本文将界定传播程序推广到允许添加任意切割平面约束，包括涉及松弛整数变量的约束，并将其命名为广义界定传播程序 (GCP-CROWN)，提高了神经网络验证的效率和 GPU 加速，实现了全面解决 Oval 20 基准和优于当今众多基准的状态表现验证工具在 Oval 21 基准上的效果。