Make Sure You’re Unsure: A Framework for Verifying Probabilistic Specifications
Year: 2022

Abstract:
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 CIFAR10 in a verification-agnostic manner, we improve the certified AUC (a verified lower bound on the true AUC) for robust OOD detection (on CIFAR-100) from 0%→ 29%. Similarly, for a BNN trained on MNIST, we improve on the `∞ robust accuracy from 60.2%→ 74.6%. Further, on a novel specification – distributionally robust OOD detection – we improve on the certified AUC from 5%→ 23%.

heading: 1 Introduction
text: While neural networks (NNs) have shown significant promise in a wide-range of applications (for e.g., [He et al., 2016, Yu and Deng, 2014]), a key-bottleneck towards their wide-spread adoption in safety-critical applications is the lack of formal guarantees regarding safety and performance. In this direction, there has been considerable progress towards developing scalable methods that can provide formal guarantees regarding the conformance of NNs with desired properties [Katz et al., 2017, Dvijotham et al., 2018b, Raghunathan et al., 2018]. However, much of this progress has been in the setting where the specifications and neural networks do not exhibit any probabilistic behaviour, or is mostly specialized for specific probabilistic specifications [Weng et al., 2019, Wicker et al., 2020].
∗Equal contribution. Authors listed in alphabetical order. Correspondance to lberrada@deepmind.com, sdathath@deepmind.com, dvij@cs.washington.edu. †DeepMind, London, United Kingdom.
35th Conference on Neural Information Processing Systems (NeurIPS 2021).
In contrast, we introduce a general framework for verifying specifications of neural networks that are probabilistic. The framework enables us to handle stochastic neural networks such as Bayesian Neural Networks or Monte-Carlo (MC) dropout networks, as well as probabilistic properties, such as distributionally robust out-of-distribution (OOD) detection. Furthermore, the specification can be defined on the output distribution from the network, which allows us to handle operations such as the expectation on functions of the neural network output.
Probabilistic specifications are relevant and natural to many practical problems. For instance, for robotics applications, there is uncertainty arising from noisy measurements from sensors, and uncertainty regarding the actions of uncontrolled agents (e.g. uncertainty regarding the behaviour of pedestrians for a self-driving vehicle). Often these uncertainties are modelled using a probabilistic approach, where a distribution is specified (or possibly learnt) over the feasible set of events [Thrun et al., 2005]. In such cases, we want to provide guarantees regarding the network’s conformance to desired properties in the distributional setting (e.g. given a model of the pedestrian’s uncertain behaviour, guarantee that the probability of collision for the autonomous vehicle is small). A more general problem includes scenarios where there is uncertainty regarding the parameters of the distribution used to model uncertainty. Here, in this general setting, we seek to verify the property that the network behaviour conforms with the desired specification under uncertainty corresponding to an entire set of distributions.
The key to handling the aforementioned complexity in the specifications being verified through our framework is the generalization of the Lagrangian duality. Specifically, instead of using the standard Lagrange duality where the multipliers are linear, we allow for probabilistic constraints (constraints between distributions) and use functional multipliers to replace the linear Lagrange multipliers. This allows us to exploit the structure of these probabilistic constraints, enabling us to provide stronger guarantees and facilitates the verification of verification-agnostic networks (networks that are not designed to be verifiable). In our paper, we focus on verification-agnostic networks as this is desirable for many reasons, as noted in Dathathri et al. [2020]. To summarize, our main contributions are:
• We derive a general framework that extends Lagrangian duality to handle a wide range of probabilistic specifications. Our main theoretical result (Theorem 1) shows that our approach (i) is always sound and computes an upper bound on the maximum violation of the specification being verified, and (ii) is expressive enough to theoretically capture tight verification (i.e. obtaining both sound and complete verification). • We develop novel algorithms for handling specific multipliers and objectives within our
framework (Propositions 1, 2). This allows us to apply our framework to novel specifications (such as distributionally robust OOD detection, where input perturbations are drawn from entire sets of distributions) by better capturing the probabilistic structure of the problem.
• We empirically validate our method by verifying neural networks, which are verificationagnostic, on a variety of probabilistic specifications. We demonstrate that even with relatively simple choices for the functional multiplier, our method strongly outperforms prior methods, which sometimes provide vacuous guarantees only. This further points towards the potential for significant improvements to be had by developing tractable optimization techniques for more complex and expressive multipliers within our framework.

heading: 2 Probabilistic Specifications

heading: 2.1 Notation
text: Let us consider a possibly stochastic neural network φ : X → P (Y), where X is the set of possible input values to the model, Y is the set of possible output values, and P (Y) is the set of distributions over Y . We assume that Y is a subset of Rl (unless specified otherwise), where l is the number of labels, and the output of the model are logits corresponding to unnormalized log-confidence scores assigned to the labels {1, . . . , l}. The model is assumed to be a sequence of K layers, each of them possibly stochastic. For k ∈ {1, . . . ,K}, πk (xk|xk−1) denotes the probability that the output of layer k takes value xk when its input value is xk−1. We write xk ∼ πk (xk−1) to denote that xk is drawn from the distribution over outputs of layer k given input xk−1 to layer k. We further assume that each πk (x) has the form σ(w̃x+ b̃), where σ is a non-linear activation function (e.g., ReLU, sigmoid, MaxOut), and w̃ and b̃
are random variables. The stochasticity for layer πk is assumed to be statistically independent of the stochasticity at other layers. For a BNN, w̃ and b̃ follow a diagonal Gaussian distribution (i.e., a Gaussian distribution with a diagonal covariance matrix), and for a MC-Dropout network they follow a Bernoulli-like distribution.
Given a distribution p0 over the inputs X , we use φ(p0) to denote (with a slight abuse) the distribution of the random variable φ(X0), where X0 ∼ p0.

heading: 2.2 Problem Formulation.
text: We now introduce the general problem formulation for which we develop the verification framework. Definition 1 (Probabilistic verification problem). Given a (possibly stochastic) neural network φ : X → P (Y), a set of distributions over the input P0 and a functional ψ : P (Y) 7→ R, the probabilistic verification problem is to check that the following is true:
∀ p0 ∈ P0, ψ (φ (p0)) ≤ 0. (1)

heading: 2.3 Examples of Specifications
text: Below we provide examples of probabilistic specifications which are captured by the above problem formulation, and that we further empirically validate our framework on. In Appendix A, we provide further examples of relevant specifications (e.g., ensuring reliable uncertainty calibration) that can be handled by our problem setup.
Distributionally Robust OOD Detection. We consider the problem of verifying that a stochastic neural network assigns low confidence scores to all labels for OOD inputs, even in the presence of bounded noise perturbations to the inputs. Given a noise distribution perturbing an OOD image xood, we require that the expected softmax is smaller than a specified confidence threshold pmax for each label i. Since the precise noise distribution is most often unknown, we wish to consider an entire class Pnoise of noise distributions. Denoting by δx the Dirac distribution around x, the problem is then to guarantee that for every p0 in P0 = {δxood + ω : ω ∈ Pnoise} and for each possible label i, ψ(φ(p0)) := Ey∼φ(p0)[softmax (y)i] − pmax ≤ 0. Robust OOD detection under bounded `∞ perturbations as considered in Bitterwolf et al. [2020] is a special case of this problem where Pnoise is restricted to a set of δ distributions over points with bounded `∞ norm.
Robust Classification. We also extend the commonly studied robust classification problem [Madry et al., 2017] under norm-bounded perturbations, to the setting of probabilistic neural networks (e.g. BNNs). Define P0 to be the set of δ input distributions centered at points within an -ball of a nominal point xnom, with label i ∈ {1, . . . , l}: P0 = {δx : ‖x− xnom‖ ≤ }. For every p0 ∈ P0, we wish to guarantee that the stochastic NN correctly classifies the input, i.e. for each j, ψ(φ(p0)) := Ey∼φ(p0)[softmax (y)i − softmax (y)j ] ≤ 0. Note that it is important to take the expectation of the softmax (and not logits) since this is how inference from BNNs is performed.

heading: 3 The Functional Lagrangian Framework
text: We consider the following optimization version: OPT = max
p0∈P0 ψ (φ (p0)) , (2)
Having OPT ≤ 0 here is equivalent to satisfying specification (1) . However, solving problem (2) directly to global optimality is intractable in general, because it can possibly be a challenging nonlinear and stochastic optimization problem. However, to only verify that the specification is satisfied, it may suffice to compute an upper bound on OPT. Here, we describe how the functional Lagrangian framework allows to derive such bounds by decomposing the overall problem into smaller, easier sub-problems.

heading: 3.1 General Framework
text: Let Xk denote the feasible space of activations at layer k, and let pk denote the distribution of activations at layer k when the inputs follow distribution p0 (so that pK = φ (p0)).
Assumptions. In order to derive our verification framework, we make the following assumptions: (A1): ∃ l0 ≤ u0 ∈ Rn such that for each input distribution p0 ∈ P0, Support (p0) ⊆ X0 = [l0, u0]. (A2): Each layer is such that if x ∈ Xk = [lk, uk], then Support (πk (x)) ⊆ Xk+1 = [lk+1, uk+1]. Assumption (A1) is natural since the inputs to neural networks are bounded. Assumption (A2) can be restrictive in some cases: it requires that the layer output is bounded with probability 1, which is not true, for example, if we have a BNN with a Gaussian posterior. However, we can relax this assumption to requiring that the output is bounded with high probability, as in Wicker et al. [2020].
Functional Lagrangian Dual. In order to derive the dual, we begin by noting that problem (2) can be equivalently written in the following constrained form:
max p0∈P0,p1,...,pK ψ (pK) s.t. ∀ k ∈ {0, . . . ,K − 1},∀ y ∈ Xk+1, pk+1 (y) = ∫ Xk πk (y|x) pk (x) dx.
For the k-th constraint, let us assign a Lagrangian multiplier λk+1(y) to each possible y ∈ Xk+1. Note that λ (y) is chosen independently for each y, hence λ is a functional multiplier. We then integrate over y, which yields the following Lagrangian penalty to be added to the dual objective:
− ∫ Xk+1 λk+1 (y) pk+1 (y) dy + ∫ Xk,Xk+1 λk+1 (y)πk (y|x) pk (x) dxdy. (3)
We now make two observations, which are described here at a high level only and are available in more details in appendix B. First, if we sum these penalties over k and group terms by pk, it can be observed that the objective function decomposes additively over the pk distributions. Second, for k ∈ {1, . . . ,K − 1}, each pk can be optimized independently (since the objective is separable), and since the objective is linear in pk , the optimal pk is a Dirac distribution, which means that the search over the probability distribution pk can be simplified to a search over feasible values xk ∈ Xk. This yields the following dual:
max pK∈PK
( ψ (pK)− ∫ XK λK (x) pK (x) dx ) + K−1∑ k=1 max x∈Xk (∫ Xk+1 λk+1 (y)πk (y|x) dy − λk (x) )
+ max p0∈P0 ∫ X0 (∫ X1 λ1 (y)π0 (y|x) dy ) p0 (x) dx, (4)
where we define PK , φ(P0). In the rest of this work, we refer to this dual as g (λ), and we use the following notation to simplify equation (4):
g (λ) = max p0∈P0 g0(p0, λ1) + K−1∑ k=1 max xk∈Xk gk(xk, λk, λk+1) + max pK∈PK gK(pK , λK). (5)
The dual g (λ) can be seen as a generalization of Lagrangian relaxation [Bertsekas, 2015] with the two key modifications: (i) layer outputs are integrated over possible values, and (ii) Lagrangian penalties are expressed as arbitrary functions λk (x) instead of being restricted to linear functions.
Main Result. Here, we relate the functional Lagrangian dual to the specification objective (2). Theorem 1. For any collection of functions λ = (λ1, . . . , λK) ∈ RX1 × . . .× RXK , we have that g (λ) ≥ OPT. In particular, if a choice of λ can be found such that g (λ) ≤ 0, then specification (1) is true. Further, when ψ (pK) = Ey∼pK [c (y)], the dual becomes tight: g (λ?) = OPT if λ? is set to:
λ?K (x) = c (x) ;∀ k ∈ {K − 1, . . . , 1}, λ?k (x) = E y∼πk(x)
[ λ?k+1 (y) ] .
Proof. We give a brief sketch of the proof - the details are in Appendix B. The problem in constrained form is an infinite dimensional optimization with decision variables p0, p1, . . . , pK and linear constraints relating pk and pk+1. The Lagrangian dual of this optimization problem has objective g (λ). By weak duality, we have g(λ) ≥ OPT. The second part of the theorem is easily observed by plugging in λ? in g (λ) and observing that the resulting optimization problem is equivalent to (2).
Example. Let P0 be the set of probability distributions with mean 0, variance 1, and support [−1, 1], and let N[a,b](µ, σ2) denote the normal distribution with mean µ and variance σ2 with truncated support [a, b]. Now consider the following problem, for which we want to compute an upper bound:
OPT = max p0∈P0 EX1 [exp(−X1)] s.t. X1|X0 ∼ N[0,1](X20 , 1) and X0 ∼ p0. (6)
This problem has two difficulties that prevent us from applying traditional optimization approaches like Lagrangian duality [Bertsekas, 2015], which has been used in neural network verification Dvijotham et al. [2018b]. The first difficulty is that the constraint linking X1 to X0 is stochastic, and standard approaches can not readily handle that. Second, the optimization variable p0 can take any value in an entire set of probability distributions, while usual methods can only search over sets of real values. Thus standard methods fail to provide the tools to solve such a problem. Since the probability distributions have bounded support, a possible way around this problem is to ignore the stochasticity of the problem, and to optimize over the worst-case realization of the random variable X1 in order to obtain a valid upper bound on OPT as: OPT ≤ maxx1∈[0,1] exp(−x1) = 1. However this is an over-pessimistic modeling of the problem and the resulting upper bound is loose. In contrast, Theorem 1 shows that for any function λ : R→ R, OPT can be upper bounded by:
OPT ≤ max x1∈[0,1],p0∈P0 exp(−x1)− λ(x1) + EX0∼p0 [EX1|X0∼N[0,1](X20 ,1)[λ(X1)]].
This inequality holds true in particular for any function λ of the form x 7→ θx where θ ∈ R, and thus:
OPT ≤ inf θ∈R max x1∈[0,1],p0∈P0 exp(−x1)− θx1 + EX0∼p0 [EX1|X0∼N[0,1](X20 ,1)[θX1]],
= inf θ∈R max x1∈[0,1],p0∈P0
exp(−x1)− θx1 + θEX0∼p0 [X20 ],
= inf θ∈R max x1∈[0,1]
exp(−x1)− θx1 + θ ≈ 0.37.
Here, our framework lets us tractably compute a bound on OPT that is significantly tighter compared to the naive support-based bound.

heading: 3.2 Optimization Algorithm
text: Parameterization. The choice of functional multipliers affects the difficulty of evaluating g (λ). In fact, since neural network verification is NP-hard [Katz et al., 2017], we know that computing g (λ?) is intractable in the general case. Therefore in practice, we instantiate the functional Lagrangian framework for specific parameterized classes of Lagrangian functions, which we denote as λ (θ) = {λk (x) = λk (x; θk)}Kk=1. Choosing the right class of functions λ(θ) is a trade-off: for very simple classes (such as linear functions), g(λ(θ)) is easy to compute but may be a loose upper bound on (2), while more expressive choices lead to tighter relaxation of (2) at the cost of more difficult evaluation (or bounding) of g(λ(θ)).
Algorithm 1 Verification with Functional Lagrangians
Input: initial dual parameters θ(0), learning-rate η, number of iterations T . for t = 0, . . . , T − 1 do {optimization loop}
for k = 0 to K do {potentially in parallel}
d (k) θ = ∇θ [ max xk gk(xk, λk, λk+1) ] {potentially approximate maximization}
end for θ(t+1) = θ(t) − η ∑K k=0 d (k) θ {or any gradient based optimization}
end for Return: Exact value or guaranteed upper bound on g(λ(θ(T ))) {final evaluation}
Optimization. With some abuse of notation, for convenience, we write g0 (x0, λ0, λ1) := g0 (p0, λ1) and gK (xK , λK , λK+1) := gK (pK , λK), with λ0 = λK+1 = 0. Then the problem of obtaining the best bound can be written as: minθ ∑K k=0 maxxk gk (xk, λk, λk+1), where the inner maximizations are understood to be performed over the appropriate domains (P0 for x0, Xk for xk,
l = 1, . . . ,K−1 and PK for xK ). The overall procedure is described in Algorithm 1: θ is minimized by a gradient-based method in the outer loop; in the inner loop, the decomposed maximization problems over the xk get solved, potentially in parallel. During optimization, the inner problems can be solved approximately as long as they provide sufficient information about the descent direction for θ.
Guaranteeing the Final Results. For the final verification certificate to be valid, we do require the final evaluation to provide the exact value of g(λ(θ(T ))) or an upper bound. In the following section, we provide an overview of novel bounds that we use in our experiments to certify the final results.

heading: 3.3 Bounds for Specific Instantiations
text: The nature of the maximization problems encountered by the optimization algorithm depends on the verification problem as well as the type of chosen Lagrangian multipliers. In some easy cases, like linear multipliers on a ReLU layer, this results in tractable optimization or even closed-form solutions. In other cases however, obtaining a non-trivial upper bound is more challenging. In this section, we detail two such situations for which novel results were required to get tractable bounds: distributionally robust verification and expected softmax-based problems. To the best of our knowledge, these bounds do not appear in the literature and thus constitute a novel contribution.
Distributionally Robust Verification with Linexp Multipliers. We consider the setting where we verify a deterministic network with stochastic inputs and constraints on the input distribution p0 ∈ P0. In particular, we consider P0 = {µ + ω : ω ∼ Pnoise}, where Pnoise denotes a class of zero-mean noise distributions that all satisfy the property of having sub-Gaussian tails (this is true for many common noise distributions including Bernoulli, Gaussian, truncated Gaussian):
Sub-Gaussian tail: ∀i,∀t ∈ R, E [exp (tωi)] ≤ exp ( t2σ2/2 ) .
We also assume that each component of the noise ωi is i.i.d. The functional Lagrangian dual g (λ) only depends on the input distribution p0 via g0, which evaluates to g0 (p0, λ1) = Ex∼p0 [λ1 (x)]. If we choose λ1 to be a linear or quadratic function, then g (λ) only depends on the first and second moments of p0. This implies that the verification results will be unnecessarily conservative as they don’t use the full information about the distribution p0. To consider the full distribution it suffices to add an exponential term which evaluates to the moment generating function of the input distribution. Therefore we choose λ1 (x) = αTx+ exp ( γTx+ κ ) and λ2 (x) = βTx. The following result then gives a tractable upper bound on the resulting maximization problems:
Proposition 1. In the setting described above, and with s as the element-wise activation function:
max p0∈P0
g0 (p0, λ1) ≤ αT (wµ+ b) + exp (∥∥wT γ∥∥2 σ2/2 + γT b+ κ) ,
max x∈X1 g1 (x, λ1, λ2) ≤ max x∈X2,z=s(x)
βT (w2z + b2)− αTx− exp ( γTx+ κ ) .
The maximization in the second equation can be bounded by solving a convex optimization problem (Appendix C.3).
Expected Softmax Problems. Several of the specifications discussed in Section 2.3 (e.g., distributionally robust OOD detection) require us to bound the expected value of a linear function of the softmax. For specifications whose function can be expressed as an expected value: ψ (pK) = Ex∼pK [c (x)], by linearity of the objective w.r.t. the output distribution pK , the search over the distribution pk can be simplified to a search over feasible output values xK :
max pK∈PK ψ (pK)− ∫ XK λK (x) pK (x) dx = max x∈XK c (x)− λK (x) . (7)
Given this observation, the following lets us certify results for linear functions of the softmax (x):
Proposition 2. For affine λK , and c(x) with the following form c (x) = µT softmax (x), maxx∈XK c (x)− λK (x) can be computed in time O(3d), where XK ⊆ Rd.
We provide a proof of this proposition and a concrete algorithm for computing the solution in Appendix C.2. This setting is particularly important to measure verified confidence and thus to perform robust OOD detection. We further note that while the runtime is exponential in d, d corresponds to the number of labels in classification tasks which is a constant value and does not grow with the size of the network or the inputs to the network. Further, the computation is embarassingly parallel and can be done in O(1) time if 3d computations can be run in parallel. For classification problems with 10 classes (like CIFAR-10 and MNIST), exploiting this parallelism, we can solve these problems on the order of milliseconds on a cluster of CPUs.

heading: 4 Related Work
text: Verification of Probabilistic Specifications. We recall that in our work, P0 refers to a space of distributions on the inputs x to a network φ, and that we address the following problem: verify that ∀p ∈ P0, φ (p) ∈ Pout, where Pout represents a constraint on the output distribution. In contrast, prior works by Weng et al. [2019], Fazlyab et al. [2019], and Mirman et al. [2021] study probabilistic specifications that involve robustness to probabilistic perturbations of a single input for deterministic networks. This setting can be recovered as a special case within our formalism by letting the class P0 contain a single distribution p. Conversely, Dvijotham et al. [2018a] study specifications involving stochastic models, but can not handle stochasticity in the input space.
Wicker et al. [2020] define a notion of probabilistic safety for BNNs: Pw∼pw [∀x ∈ X , φw(x) ∈ C] ≥ pmin, where P is the probability of any event, φw denotes the network with parameters w, pw denotes the distribution over network weights (e.g., a Gaussian posterior) and C is a set of safe outputs, and this allows for computation of the probability that a randomly sampled set of weights exhibits safe behaviour. However, in practice, inference for BNNs is carried out by averaging over predictions under the distribution of network weights. In this less restrictive and more practical setting, it suffices if the constraint is satisfied by the probabilistic prediction that averages over sampled weights: ∀x ∈ X , Pw∼pw [φw(x) ∈ C] ≥ pmin, where φw(x) denotes the distribution over outputs for x ∈ X . Further, Wicker et al. [2020] also observe that minx∈X Pw∼pw [φw(x) ∈ C] ≥ Pw∼pw [∀x ∈ X , φw(x) ∈ C], making the second constraint less restrictive. Cardelli et al. [2019] and Michelmore et al. [2020] consider a similar specification, but unlike the approaches used here and by Wicker et al. [2020], these methods can give statistical confidence bounds but not certified guarantees.
Wicker et al. [2021] improve the classification robustness of Bayesian neural networks by training them to be robust based on an empirical estimate of the average upper bound on the specification violation, for a fixed set of sampled weights. In contrast, our approach provides meaningful guarantees for BNNs trained without considerations to make them more easily verifiable, and the guarantees our framework provides hold for inference based on the true expectation, as opposed to a fixed set of sampled weights.
Our work also generalizes Bitterwolf et al. [2020], which studies specifications of the output distribution of NNs when the inputs and network are deterministic. In contrast, our framework’s flexibility allows for stochastic networks as well. Furthermore, while Bitterwolf et al. [2020] are concerned with training networks to be verifiable, their verification method fails for networks trained in a verification-agnostic manner. In our experiments, we provide stronger guarantees for networks that are trained in a verification-agnostic manner.
Lagrangian Duality. Our framework subsumes existing methods that employ Lagrangian duality for NN verification. In Appendix D.1, we show that the functional Lagrangian dual instantiated with linear multipliers is equivalent to the dual from Dvijotham et al. [2018b]. This is also the dual of the LP relaxation [Ehlers, 2017] and the basis for other efficient NN verification algorithms ([Zhang et al., 2018, Singh et al., 2018], for example), as shown in Liu et al. [2021]. For the case of quadratic multipliers and a particular grouping of layers, we show that our framework is equivalent to the Lagrangian dual of the SDP formulation from Raghunathan et al. [2018] (see Appendix D.2).
We also note that similar mathematical ideas on nonlinear Lagrangians have been explored in the optimization literature [Nedich and Ozdaglar, 2008, Feizollahi et al., 2017] but only as a theoretical construct - this has not lead to practical algorithms that exploit the staged structure of optimization problems arising in NN verification. Further, these approaches do not handle stochasticity.

heading: 5 Experiments
text: Here, we empirically validate the theoretical flexibility of the framework and its applicability to across several specifications and networks. Crucially, we show that our framework permits verification of probabilistic specifications by effectively handling parameter and input stochasticity across tasks. For all experiments, we consider a layer decomposition of the network such that the intermediate inner problems can be solved in closed form with linear multipliers (See Appendix C.4). We use different bound-propagation algorithms to compute activation bounds based on the task, and generally refer to these methods as BP. Our code is available at https://github.com/deepmind/jax_verify.

heading: 5.1 Robust OOD Detection on Stochastic Neural Networks
text: Verification Task. We consider the task of robust OOD detection for stochastic neural networks under bounded `∞ inputs perturbation with radius . More specifically, we wish to use a threshold on the softmax value (maximized across labels) to classify whether a sample is OOD. By using verified upper bounds on the softmax value achievable under -perturbations, we can build a detector that classifies OOD images as such even under perturbations. We use the Area Under the Curve (AUC) to measure the performance of the detector. Guaranteed AUC (GAUC) is obtained with verified bounds on the softmax, and Adversarial AUC (AAUC) is based on the maximal softmax value found through an adversarial attack. We consider two types of stochastic networks: i) Bayesian neural networks (BNNs) whose posterior distribution is a truncated Gaussian distribution. We re-use the MLP with two hidden layers of 128 units from Wicker et al. [2020] (denoted as MLP) and truncate their Gaussian posterior distribution to three standard deviations, ii) we consider MCDropout convolutional neural networks, namely we use LeNet (as in Gal and Ghahramani [2016]) and VGG-style models [Simonyan and Zisserman, 2015]. For MLP and LeNet, we use MNIST as training data, and EMNIST as out-of-distribution data. For the VGG models, we use CIFAR-10 as training data, and CIFAR-100 as out-of-distribution data.
Method. We use linear Lagrangian multipliers, which gives closed-form solutions for all intermediate inner maximization problems (Appendix C.4). In addition, we leverage Proposition 2 to solve the final inner problem with the softmax specification objective. Further experimental details, including optimization hyper-parameters, are available in Appendix E.1. We compute activation bounds based on an extension of Bunel et al. [2020] to the bilinear case, referred to as BP in Table 1. The corresponding bounds are obtained with probability 1, and if we were to relax these guarantees to only hold up to some probability lower than 1, we note that the method of [Wicker et al., 2020] would offer tighter bounds.
Results. The functional Lagrangian (FL) approach systematically outperforms the BoundPropagation (BP) baseline. We note that in particular, FL significantly outperforms BP on dropout CNNs, where BP is often unable to obtain any guarantee at all (See Table 1). As the size of the VGG
model increases, we can observe that the median runtime of BP increases significantly, while the additional overhead of using FL remains modest.

heading: 5.2 Adversarial Robustness for Stochastic Neural Networks
text: Verification Task. For this task, we re-use the BNNs trained on MNIST [LeCun and Cortes, 2010] from Wicker et al. [2020] (with the Gaussian posterior truncated to three standard deviations bounded). We use the same setting as Wicker et al. [2020] and study the classification robustness under `∞ perturbations for 1-layered BNNs and 2-layered BNN at radii of = 0.025 and = 0.001 respectively. We recall, as mentioned earlier in Section 4, that the specification we study is different from that studied in [Wicker et al., 2020].
Method We use the same solving methodology as in Section 5.1. To compute bounds on the activations, we use the bilinear LBP method proposed in Wicker et al. [2020].
Results. Across settings (Table 2) our approach is able to significantly improve on the guarantees provided by the LBP baseline, while also noting that our method incurs an increased compute cost.

heading: 5.3 Distributionally Robust OOD Detection
text: Verification Task. We bound the largest softmax probability across all labels for OOD inputs over noisy perturbations of the input where the noise is drawn from a family of distributions with only two constraints for each p ∈ Pnoise: ω ∈ [− , ] with prob. 1,Eω∼p [exp (ωt)] ≤ exp ( σ2t2/2 ) , for given constraints , σ > 0. The first constraint corresponds to a restriction on the support of the noise distribution, and the second constraint requires that the noise distribution is sub-Gaussian with parameter σ. We note that no prior verification method, to the best of our knowledge, addresses this setting. Thus, as a baseline, we use methods that only use the support of the distribution and perform verification with respect to worst-case noise realizations within these bounds.
Method. We use a 3-layer CNN trained on MNIST with the approach from Hein et al. [2019] (details in Appendix E.3), and we employ EMNIST as the out-of-distribution data to be detected. We use functional multipliers of the form: λk (x) = θTk x for k > 1 and linear-exponential multipliers for the input layer: λ1 (x) = θT1 x + exp ( γT1 x+ κ1 ) (method denoted by FL-LinExp). As baselines, we consider a functional Lagrangian setting with linear multipliers that only uses information about the expectation of the noise distribution (method denoted by FL-Lin), and a BP baseline that only uses information about the bounds on the support of the noise distribution (− , ) (activation bounds are computed using Bunel et al. [2020]). The inner maximization of gk for K − 1 ≥ k ≥ 2 can be done in closed form and we use approaches described in Propositions 1 and 2 to respectively solve max g0,max g1 and max gK . We use = 0.04, σ = 0.1.
Results. FL-LinExp achieves the highest guaranteed AUC (See Table 3), showing the value of accounting for the noise distribution, instead of relying only on bounds on the input noise.

heading: 6 Conclusion
text: We have presented a general framework for verifying probabilistic specifications, and shown significant improvements upon existing methods, even for simple choices of the Lagrange multipliers where we can leverage efficient optimization algorithms. We believe that our approach can be significantly extended by finding new choices of multipliers that capture interesting properties of the verification problem while leading to tractable optimization problems. This could lead to discovery of new verification algorithms, and thus constitutes an exciting direction for future work.
Limitations. We point out two limitations in the approach suggested by this work. First, the guarantees provided by our approach heavily depend on the bounding method used to obtain the intermediate bounds – this is consistent with prior work on verifying deterministic networks [Dathathri et al., 2020, Wang et al., 2021], where tighter bounds result in much stronger guarantees. Second, as noted in Section 3.1, our approach can only handle probability distributions that have bounded support, and alleviating this assumption would require further work.
Broader Impact and Risks. Our work aims to improve the reliability of neural networks in settings where either the model or its inputs exhibit probabilistic behaviour. In this context, we anticipate this work to be largely beneficial and do not envision malicious usage. However, the guarantees of our method crucially depend on having an accurate modeling of the uncertainty. Failing that can result in an overestimation of the reliability of the system, which can have catastrophic consequences in safety-critical scenarios. In this regard, we advocate special care in the design of the specification when applying our approach to real-world use cases.

Review summaries:
The paper targets the verification of probabilistic specifications of neural networks, e.g., where the specification to a deterministic network can be probabilistic, or for verifying deterministic specifications over a probabilistic neural network. The authors pose the probabilistic verification as an intractable stochastic optimization problem. They leverage functional lagrangian framework to solve the problem approximately. The framework enables the decomposition of the problem into smaller sub-problems which are relatively tractable to solve. The authors experimentally demonstrate the effectiveness of their approach on three specifications against Wicket et al. and obtain more precise results while remaining scalable.

This paper proposes a general framework for probabilistic robustness verification, with both stochastic networks and probabilistic specifications. The core technique is based on the generalization of Lagrangian duality where the multipliers are functional multipliers and probabilistic constraints are allowed. Under the proposed framework, the paper demonstrates several applications, including robust OOD detection on stochastic NN, adversarial robustness verification for stochastic NN, and distributionally robust OOD detection. 

The paper proposes a framework for giving mathematical guarantees on neural networks with probabilistic specifications, e.g. for robustness across distributions or for robustness of models with non-deterministic outputs. The authors first formulate the abstract framework in terms of functional lagrangians and then show how to apply these by using concrete applications and concrete function classes for the lagrangians.