Infinite Time Horizon Safety of Bayesian Neural Networks
Authors: Mathias Lechner
Đorđe Žikelić
Krishnendu Chatterjee
Thomas A Henzinger
Venue: NeurIPS 2021 Poster (2021)
Keywords: Bayesian neural networks
BNN
safety verification

Abstract: Bayesian neural networks (BNNs) place distributions over the weights of a neural network to model uncertainty in the data and the network's prediction.
We consider the problem of verifying safety when running a Bayesian neural network policy in a feedback loop with infinite time horizon systems.
Compared to the existing sampling-based approaches, which are inapplicable to the infinite time horizon setting, we train a separate deterministic neural network that serves as an infinite time horizon safety certificate.
In particular, we show that the certificate network guarantees the safety of the system over a subset of the BNN weight posterior's support. Our method first computes a safe weight set and then alters the BNN's weight posterior to reject samples outside this set. Moreover, we show how to extend our approach to a safe-exploration reinforcement learning setting, in order to avoid unsafe trajectories during the training of the policy. 
We evaluate our approach on a series of reinforcement learning benchmarks, including non-Lyapunovian safety specifications.

Infinite Time Horizon Safety of Bayesian Neural Networks
Mathias Lechner" IST Austria Klosterneuburg, Austria mlechner@ist.cm ac.tt.ccaa at
Dorde žikelić" IST Austria Klosterneuburg, Austria dzikelickist.ac
Krishnendu Chatterjee IST Austria Klosterneubrr, Austria kchatterjeeeisst ac at
Thomas A. Henzinger
IST Austria Klosterneuburg, Austria tah@ist. ac at
Abstract
Bayesian neural networks (BNNs) place distributions over the weights of a neural network model uncertainty in the data and the network's prediction. We consider the problem of verifying safety when running Bayesian neural network policy in a feedback loop with infinite time horizon systems. Compared the existing sampling-bass -ased approaches, which are inapplicable to the infinite time horizon setting, we train separate deterministic neural network that serves an infinite time horizon safety certificate. In particular, we show that the certificate network guarantees the safety of the system over subset of the BNN weight posterior's s support. Our method first computes safe weight set and then alters the BNN's weight posterior to reject samples outside this set. Moreover, we show how extend our approach a safc-exploration reinforcement learning setting, in order avoid unsafe trajectories during the training the policy. We evaluate our approach series of reinforcement learning benchmarks, including non-Lyapunovian safety specifications.
Introduction
The success of deep neural networks (DNNs) across different domains has created the desire to apply
them in safety-critical applications such autonomous vehicles [28 30] and healthcare systems [41]
The fundamental challenge for the deployment of DNNs in these domains is certifying their safety 3
Thus, formal safety verification of DNNs in isolation and closed control loops (26 23
17
43 13
has become an active research topic.
Bayesian neural networks (BNNs) are family of neural networks that place distributions over their weights [36]. This allows learning uncertainty in data and the network's prediction, while preserving the strong modelling capabilities of DNNs [32]. In particular, BNNs can learn arbitrary data distributions from much simpler (c.g. Gaussian) weight distributions. This makes BNNs very appealing for robotic and medical applications 333 where uncertainty is central component of data.
Despite the large body of literature on verifying safety DNNs, the formal safety verification of BNNs has received less attention. Notably, 8 obtaining probabilistic guarantees about BNNs. Although these approaches provide some insight
45 34] have proposed sampling-basee techniques for
Equual Contribution.
35th Conference on Neural Information Processing Systems (NcurIPS 2021).

---

into BNN safety, they suffer from two key limitations. First, sampling provides only bounds on the probability of the BNN's safety which is insufficient for systems with critical safety implications. For instance, having an autonomous vehicle with a 99.9% safety guarantee is still insufficient for deployment if millions of vehicles are deployed. Second, samples can only simulate the system for a finite time, making it impossible to reason about the system's 's safety over an unbounded time horizon.
In this work, we study the safety verification problem for BNN policies in safety-critical sys- tems over the infinite time horizon. Formally, we consider discrete-ting time closed-loop systems defined by dynamical system and BNN pol- icy. Given a set of initial states and set of unsafe (or bad) states, the goal of the safety verification problem is to verify that no system execution starting in an initial state can reach an unsafe state. Unlike existing literature which considers probability of safety, we verify sure safety, i.e. safety of every system execution of the system. In particular, we present a method for computing safe weight sets for which every system execution is safe as long as the BNN samples its weights from this set.
Posterior
Safe ++- Unsafe
Posterior
(+ rejection sampling)
Safe
Unsafe
Figure I: BNNs are typically unsafe by default. Top figure: The posterior of a typical BNN has unbounded support, resulting in a non-zero proba- bility of producing an unsafe action. Bottom figure: Restricting the support of the weight distributions via rejection sampling ensures BNN safety.
Our approach to restrict the support of the weight distribution is necessary as BNNs with Gaussian weight priors typically produce out- put posteriors with unbounded support. Conse-
quently, there is a low but non-zero probability for the output variable to lie in an unsafe region, see Figure D This implies that BNNs are usually unsafe by default. We therefore consider the more general problem of computing safe weight sets. Verifying that a weight set is safe allows re-calibrating the BNN policy by rejecting unsafe weight samples in order to guarantee safety.
As most BNNs employ uni-modal weight priors, e.g. Gaussians, we naturally adopt weight sets in the form of products of intervals centered at the means of the BNN's weight distributions. To verify safety of weight set, we search for a safety certificate in the form of a safe positive invariant (also known as safe inductive invariant). A safe positive invariant is set of system states that contains all initial states, is closed under the system dynamics and does not contain any unsafe state. The key advantage of using safe positive invariants is that their existence implies the infinite time horizon safety. We parametrize safe positive invariant candidates by (deterministic) neural networks that classify system states for determining set inclusion. Moreover, invariant as a learning problem. A separated verifier module then checks if a candidate is indeed a safe positive invariant by checking the required properties via constraint solving. In case the verifier finds a counterexample demonstrating that the candidate violates the safe positive invariant condition, re-train the candidate the found counterexample. We repeat this procedure until the verifier concludes that the candidate is a safe positive invariant ensuring that the system is safe.
phrase the search for an
The safe weight set obtained by our method can be used for safe exploration reinforcement learning. In particular, generating rollouts during learning by sampling from the safe weight set allows an exploration of the environment while ensuring safety. Moreover, projecting the (mean) weights onto the safe weight set after each gradient update further ensures that the improved policy stays safe.
Contributions Our contributions can be summarized as follows:
1. We define safety verification problem for BNN policies which overcomes the unbounded posterior issue by computing and verifying safe weight sets. The problem generalizes the sure safety verification of BNNs and solving allows re-calibrating BNN policies via rejection sampling to guarantee safety.
2. We introduce method for computing safe weight sets in BNN policies in the form of products of intervals around the BNN weights' means. To verify safety of a weight set, our novel algorithm learns a safe positive invariant in the form of deterministic neural network.
3. We evaluate our methodology on series of benchmark applications, including linear systems and nyn-Lyapunovian safety specifications.

---

2 Related work
Verification of feed-forward NN Verification of robustness and safety properties in forward DNNs has received much attention but remains an active research topic [26] 23 40
7 43 As
the majority of verification techniques were designed for deterministic NNs, they cannot be readily applied to BNNs. The safety verification of samples to obtain statistical guarantees on the safety probability. The work of [45] also presents a sampling-base approach, however it provides certified lower bounds on the safety probability.
BNNs has been considered in [8] by using
The literature discussed above considers NNs in isolation, which can provide input-output guarantees on a NN but are unable to reason holistically about the safety of the system that the NN is applied in. Verification methods that concern the safety of NNs interlinked with a system require different approaches than standalone NN verification, which we will discuss in the rest of this section.
Finite time horizon safety of BNN policies The work in 34 extends the method of [8] to verifying safety in closed-loop systems with BNN policies. However, similar to the standalone setting of [8] their method obtains only statistical guarantees the safety probability and for the system's execution over a finite time horizon.
Safe RL Safe reinforcement learning has been primarily studied in the form of constrained Markov decision processes (CMDPs) 2 [8. Compared to standard MDPs, an agent acting in a CMDP must satisfy an expected auxiliary cost term aggregated over an episode. The CMDP framework has been the base of several RL algorithms [44), notably the Constrained Policy Optimization (CPO) [. Despite these algorithms providing decent performance, the key limitation of CMDPs is that the constraint is satisfied in expectation, which makes violations unlikely but nonetheless possible. Consequently, the CMDP framework is unsuited for systems where constraint violations are critical.
Lyapunov-based stability Safety in the context of "taabiiity", i.e. always returning to a ground state, can be proved by Lyapunov functions 4. Lyapunov functions have originally been considered to study stability of dynamical systems 29 Intuitively, a I Lyapunov function assigns a non-negative value to each state, and is required to decrease with respect to the system's dynamics at any state outside of the stable set. A Lyapunov- based method is proposed in [ to ensure safety in CMDPs during training. Recently, the work of [9] presented a method for learning a policy well as a neural network Lyapunov function which guarantees the stability of the policy. Similarly to our work, their learning procedure is counterexample-basee and safety definitions that do not require returning to a set of ground states.
However, unlike (9) our work considers BNN policies
Barrier functions for dynamical systems Barrier functions can be used to prove infinite time
horizon safety dynamical systems [38 39 Recent works have considered learning neural network
barrier functions [7]. and a counterexample-baae
learning procedure is presented in 37
Finite time horizon safety of NN policies Safety verification of continuous-time closed-loop systems with deterministic NN policies has been considered in [24, 19], which reduces safety verification to the reachability analysis in hybrid systems (10). The work of [13] presents a method which computes a polynomial approximation of the NN policy to allow an efficient approximation of the reachable state set. Both works consider finite time horizon systems.
Our safety certificate most closely resembles inductive invariants for safety analysis in programs and positive invariants for dynamical systems (5].
14
3 Preliminaries and problem statement
We consider a discrete-time dynamical system
x f(x,, uz), Xo E No.
The dynamics are defined by the function f X' x u + X' where X C I.' is the state space and U S RR" is the control action space, X, S X is the set of initial states and E N20 denotes a discretized time. At each time step t. the action is defined by the (possibly probabilistic) positional policy x X' - D(U), which maps the current state x, to distribution π Txx)) E D(U) over the set of actions. We use D(U) to denote the set of all probability distributions over U. The next action is then sampled according to U, ~ π (x1), and together with the current state x, of the system gives rise to the next state X 1 of the system according to the dynamics/ f. Thus, the dynamics f together
3

---

with the policy т form closed-loop system (or feedback loop system). The aim of the policy is to maximize the expected cumulative reward (possibly discounted) from each starting state. Given a set of initial states Xg of the system, we say that sequence of state-action pairs (X,, uz) is trajectory if X E Xg and we have 11, E (x)p(==(x)) and X = [(,,, Ut) for each t E Ngo-
A neural network (NN) is function π : _R + R" that consists of several sequentially composed layers ग = 1 which picks a single action with probability 1. Each layer 4 is parametrized by learned weight values of the appropriate dimensions and an activation function a.
o lg. Formally, a NN policy maps each system state to Dirac-delta distribution
(x) = a (W,x x + by), W. E R b, E R"
= max 0}, although other piecewise linear activation such as the leaky-ReLU 25 and PReLU are applicable as well.
In this work, we consider ReLU activation functions xxx (cLU(x)
In Bayesian neural networks (BNNs), weights are random variables and their values are sampled, each according some distribution. Then each vector of sampled weights gives rise to a (deterministic) neural network. Given a training set D. in order to train the BNN we assume a prior distribution p( w. b) over the weights. The learning then amounts computing the posterior distribution p( (w, b 'D) via the application of the Bayes rule. As analytical inference of the posterior is in general infeasible due to non-linearity introduced by the BNN architecture (32], practical training algorithms rely on approximate inference, e.g. Hamiltonian Monte Carlo (3... variational inference [6] or dropout (15).
When the policy in dynamical system is BNN, the policy maps each system state x; to probability distribution (x:) over the action space. Informally. this distribution is defined as follows. First, BNN weights w, b are sampled according to the posterior BNN weight distribution, and the sampled weights give rise to a deterministic NN policy Tw.b- The action of the system is then defined as u, Tw,b(x)) (x,). Formal definition of the distribution =xx)) is straightforward and proceeds by considering the product measure of distributions of all weights.
Problem statement We now define the two safety problems that we consider in this work. The first problem considers feed-forward BNNs, and the second problem considers closed-loop systems with BNN policies. While our solution to the first problem will be subprocedure in our solution to the second problem, the reason why we state as a separate problem is that we believe that our solution to the first problem is also of independent interest for the safety analysis of feed-forward BNNs.
Let be a BNN. Suppose that the vector (w, b) of BNN weights in has dimension p + q, where p is the dimension of w and is the dimension of b. For each 1 < i S p, let μı, denote the mean of the random variable w.. Similarly, for each S S q, let p444 denote the mean of the random variable b, Then, for each E [0, oo). we define the set W of weight vectors via
p+y
W = II [p 4 + RRtt.
We now proceed to defining our safety problem for feed-forward BNNs. Suppose that we given feed-forward BNN n, a set Xo S 1 of input points and set X., C II" of unsafe (or bad) output points. For a concrete vector (w, b) of weight values, let Tw.b b to be the (deterministic) NN defined by these weight values. We say that Tw,b is safe if for each x E Xy we have (x) & Xu, i.e. evaluating Tw all input points does not lead to unsafe output.
Problem 1 (Feed-forwand BNNs). Let x be a ferd-forward BNN, Xo R. a set of input points and X, C R a set of unsafe output points. Let c E [0, co). Determine whether each deterministic NN in [Twb (w. b) E Wr] is safe.
Next, we define our safety problem for closed-loop systems with BNN policies. Consider a closed- loop system defined by dynamics function f. a BNN policy and an initial set of states Xg- Let X., C X' be a set of unsafe (or bad) states. We say that trajectory (x,, u, ) is safe if x, g X,, for all t E No, hence if it does not reach any unsafe states. Note that this definition implies infinite time horizon safety of the trajectory. Given e E [0, so). define the set Traj!** to be the set of all system trajectories in which each sampled weight vector belongs to W*.

---

Problem 2 (Closed-lowe loop systems with BNN policies). Consider a closed-loop system defined by dynamics functiin f. BNN policy π. and set of initial states Ng. Let X, be set of unsafe states. Let E [0, c0). Determine whether each trajectory in Traj." is safe.
Note that the question of whether the BNN policy π is safe (i.e. whether each trajectory of the system is safe) is a special case of the above problem which corresponds to c cc.
4
Main results
In this section we present our method for solving the safety problems defined in the previous section, with Section 4.1 considering Problem and Section [4.2] considering Problem Both problems consider safety verification with respect to a given value of c E [0, oo), so in Section 4.3 we present our method for computing the value of e for which our solutions to Problem and Problem may be used to verify safety. We then show in Section 4.4 how our new methodology can be adapted to the safe exploration RL setting.
4.1 Safe weight sets for feed-forward BNNs
Consider ferdrforward BNN set Xo C R of inputs and a set X. S IR" of unsafe output of the BNN. Fix E [0, oo]. To solve Problem [ we show that the decision problem of whether each deterministic NN in {Twb (w, b) E W safe can be encoded system of constraints and reduced to constraint solving.
Suppose that / o M, the matrix of the same dimension as W,, with each entry equal to the mean of the corresponding random variable weight in W, Similarly, define the vector m, of means of random variables in b;- The real variables of our system of constraints are as follows, each of appropriate dimension:
o lg consists of A layers, with each (x) = ReLU (W x + b,). Denote by
Xy encodes the BNN inputs, encodes the BNN outputs;
xin xi..... xin encode vectors of input values of each neuron in the hidden layers;
x ..... Xi-1 encode vectors of output values of each neuron in the hidden layers; Xos and Xn,neg are dummy variable vectors of the same dimension as Xe and which will be used to distinguish between positive and negative NN inputs Xo, respectively.
We use 1 to denote the vector/matrix whose all entries are equal to 1, of appropriate dimensions defined by the formula in which it appears. Our system of constraints is as follows:
Xg Xo.
Xi E X
(Input-output conditions)
x Re for each sisl-1
(ReLU encoding)
(M; - c- 1) 1)x; out (m; - -m;- 1) x x for each 1 1//5--
(BNN hidden layers)
x,11 < (M; +e- 1)x,ur + (m, + 1), for each 15i5/-1
Nos ReLU((x), Xo,neg (eLL((-Xx)
(Mo 10x0, pos + (Mo 1)x0,00g (mo - E 1) S xin
(BNN input layer)
x < (Mo + e 1)x," out + (Mo e 1)xo, + (mo- + e
Denote by Φ( No, Xy, E) the system of constraints defined above. The proof of Theorem shows that encodes that Xo E Xo is an input point for which the corresponding output point of π is unsafe, i.e.
π (Xn) E X,, The first equation encodes the input and output conditions. The second equation encodes the ReLU onput-output relation for each hidden layer neuron. The remaining equations encode the relation between neuron values in successive layers of the BNN as well as that the sampled BNN weight vector in W For hidden layers, we know that the output value of each neuron is nonnegative, i.e. xut > 0 for the i-th hidden layer where 1 < l 1, and so
(M, 1)x;" out < (M, + 1)x,"
5

---

Hence, the BNN weight relation with neurons in the successive layer as well as the fact that the sampled weights are in W is encoded as in equations 3-4 above. For the input layer, however, we do not know the signs of the input neuron values Xo and so we introduce dummy variables equation
Xp.pos (xn) and Xg,eey = - ReReUe(UXXpp
This allows encoding the BNN weight relations between the input layer and the first hidden layer as well as the fact that the sampled weight vector is in W as in equations 6-7. Theorem [
shows that Problem is equivalent to solving the system of constraints (TT, No, Xu, e). Its proof can be found in the Supplementary Material.
[
Theorem 1. Let E [0, oo]. Then each deterministii NN in {Tw.b b () E W is safe if and only if the system of constraints ((I, No, Na. E) is not satisfiable.
Solving the constraints Observe that e, M, and m 1 1sis 1, are constant values that are known at the time of constraint encoding. Thus, in (1, only the ReLU constraints and possibly the input-output conditions are not linear. Depending on the form of Xy and X₂ and on how we encode the ReLU constraints, we may solve the system ((x,, Xo: Xy, t) in several ways:
1. MILP. It is shown in 31 12 43 that the ReI.U relation between two real variables can be encoded via mixed-integer linear constraints (MILP) by introducing 0/1-integer variables to encode whether given neuron is active or inactive. Hence, if No and X., are given by linear constraints, we may solve ( No, Nu. e) by MILP solver. The ReLU encoding requires that each neuron value is bounded, which is ensured if Xo is a bounded set and if e < co. 20, we may use algorithms based on the Reluplex calculus 26 (7) to solve D(T, No, Au. e). Reluplex is an extension of the standard simplex algorithm for solving systems of linear constraints, designed to allow ReLU constraints as well. While Reluplex does not impose the boundedness condition, it is in general less scalable than -lo.--sol
2. Reluplex. In order to allow unbounded X, and
3. NRA-SMT. A Alternatively, if Xo or X, are given by non-linear constraints we may solve them by using an NRA-SMT--ollver (non-linear real arithmetic satisfiability modulo theory), e.g. ddRaal [16.. To use NRA-SMT-solver, we replace the integer 0/1-variables of the ReLU neuron relations encoding with real variables that satisfy the constraint a(x - 1) = O. While NRA-SMT is less scalable compared to MILP, we note that it has been used in previous works on RL stability verification [9]
Safety via rejection sampling As discussed in Section once the safety of NNs in { (w. b) E W has been verified, we can "re-calibrate" the BNN to reject sampled weights which are not in W Hence, rejection sampling gives rise to a safe BNN.
4.2 Safe weight sets for closed-loop systems with BNN Policies
Now consider a closed-loop system with a dynamics function f X x X' with X C 1 and U C IR", a BNN policy ग, an initial state set X C X' and an unsafe state set Xr S X. Fix e [0, co]. In order to solve Problem 2 and verify safety of each trajectory contained in Trajf our method searches for positive lnvariant-like safety certificate that we define below.
Positive invariants for safety A positive invariant in a dynamical system is a set of states which contains all initial states and which is closed under the system dynamics. These conditions ensure that states of all system trajectories are contained in the positive invariant. Hence, a positive invariant which does not contain any unsafe states can be used certify safety of every trajectory over infinite time horizon. In this work, however, we are not trying to prove safety of every trajectory, but only of those trajectories contained in Traj! To that end, we define -sfe positive invariants. Intuitively, a - positive invariant is required to contain all initial states, to be closed under the dynamics f and the BNN policy when the sampled weight vector is in W", and not to contain any unsafe state.
Definition (W"- -afe positive invariants). A set Inv C X is said to be a -ps-issitive invariant if X C Inv, for each E Inv and (w, b) E WT we have that [(x, (x)) E Invv, and Inv O X., 0.
Theorem 2 shows that Wsssafe positive invariants can be used to verify safety of all trajectories in The proof is straightforward and is deferred to the Supplementary Material,
Traj!"" in Problem 2
Theorem 2. If there exists WT positive invariant, then each trajectory in Traj. is safe.

---

Algorithm 1 Learning algorithm for -sfe positive invariants
Input Dynamics function f. BNN policy æ, Initial state set No. Unsafe state set Nu [0, oo]
Ro, Ry < random samples of Kn, Ru
Dapec < X. {0} U Ry {1), Dce t {
Optional (bootstrapping): Socotstrap < sample finite trajectories with initial state sampled from X
Dxpec= Dspec (x,, 0)] 78 E Shootstrap that starts in E A' and reaches X.,) } [ 1) E Shootstrap that starts in x E X and does not reach X.
Pre-train neural network g on datasets Dspee and Doe with loss function L while timeout reached do if 3xx x', u, w, b) s.t. (x"((x) 2 0, (x) < O, (w, b) E W u (x), x'= = ((), then
Doe + Dee U {(xxx'}
else if (x) s.t. x E No, ( < 0 then
Dxpec Dspec U {(x, 1)}
else if 3(x) s.t. E Nus gl
2 0 then
Dxpes + Depec U {(x, 0)}
else
Return Safe
end if
Train neural network glvv on datasets Dapec and Dee with loss function C
end while
Return Unsafe
Learning positive invariants We now present learning algorithm for a W -sae positive invariant. learns a neural network ginv : R" + E, where the positive invariant is then defined as the set Inv = {x X (x) 2 0). The pseudocode is given in Algorithm
The algorithm first samples &o from No and Xr from Xr and initializes the specification set Depec to X. {0} U Ro {1} and the counterexample set Dce to empty set. Optionally, the algorithm also bootstraps the positive invariant network by initializing D Depee with random samples from the state space X' labeled with Monte-Carlo estimates of reaching the unsafe states. The rest of the algorithm consists of two modules which are composed into loop: the learner and the verifier. In each loop iteration, the learner first learns W -afe positive invariant candidate which takes the form of neural network glnv, This is done by minimizing the loss function L that depends on Dapec and Doe:
(mg
Σ
(o Inu (x).
+ (x))
Σ Loo (T ("" (1)
Depes!
Dee
(x.1)) Dapce
(x,x))EDe
where X is a tuning parameter and Lets binary classification loss function, e.g. the 0/1-loss Lan (2.y) 1 [ 2 0] * y] or the logistic loss (ing(,,y) = = 2. y + log(1 + exp(-=))
as differentiable alternative. The term Loe is the counterexample loss which we define via
Lee (2, 1 > 0]
< fcn fet (2',
(2)
Intuitively, the first sum eq. [ forces g Inv to be nonnegative at initial states and negative at unsafe states contained in D Dppce and the second term forces each counterexample in Dee not to destroy the closedness of Inv under the system dynamics.
Once gnv is learned, the verifier checks whether Inv is indeed W/f-safe positive invariant. To do this, the verifier needs to check the three defining properties of WT positive invariants:
1. Closedness of Inv under system dynamics. The verifier checks if there exist states x E Inv, x' & Inv and BNN weight vector (w, b) W such that f(x, T Tw,b (x)) x'. To do this, it introduces real variables x, x' E Rmm E I and y. y E IR, and solves:
maximize y y' subject to
0,y 0, 'TV (x), v = lny((x))) x' f(x u) u an output of ग on input x and weights (w, b) E W
7

---

The conditions y g" (x) and s' = (x""(x)) are encoded by using the existing techniques for encoding deterministic NNs as systems of MILPPRelulle//NRASSM condition in the third equation is encoded simply by plugging variable vectors x and u into the equation for f- Finally, for condition in the fourth equation we use our encoding from Section 4.1 where we only need to omit the Input-output condition. The optimization objec- tive is added in order to search for the "worst" counterexample. We note that MILP [20] and SMT [16] solvers allow optimizing linear objectives, and recently Reluplex algorithm [26] has also been extended to allow solving optimization problems 42]. a counterexample (x,x') is found, it is added to Dee and the learner tries to learn a candidate. If the system of constraints is unsatisfiable, the verifier proceeds to the second check.
constraints. The
2. Non-negativity
Xg. The verifier checks if there exists such x is found, (x, 1) is added to Dapec and the learner then tries to learn a new candidate. If the system of constraints is unsatisfiable, the verifier proceeds the third check.
Xy for which (x" < 0. If
3. Negativity on X,, The verifier checks there exists x E Xr with g 2 0. If such x is found, (x. 0) is added to spec and the learner then tries learn new candidate. If the system of constraints is unsatisfiable, the veririfer concludes that Inv is a -possiiveee invariant which does not contain any unsafe state and so each trajectory in Traj f. is safe.
Theorem 3 shows that neural networks plav for which Inv is a W -sae positive invariants are global minimizers of the loss function L with the 0/1 ollclaasifiiaation loss. Theorem establishes the correctness of our algorithm. Proofs can be found in the Supplementary Material.
Theorem 3. The loss function C is nonnegative for any neural network g. i.e. C(g) 2 O. Moreover, if Inv is a W2-saf positive invariant and Let the 0/1-loss, then L(g"nv) O. Hence, neural networks glnv for which Inv is a W -safe positive invariant are globul minimizers of the loss function L when foss is the 0/1-loss.
Theorem 4. the verifier in Algorithm 7 Ashows that constraints in three checks are unsatisfiable, then the computed Inv is indeed a W -aae positive invariant. Hence, Algorithm ii correct.
Safety via rejection sampling As discussed in Section 1 once the safety of all trajectories in Trajf has been verified, we can "re-calibrate" the BNN policy to reject sampled weights which are not in W Hence, rejection sampling gives rise to a safe BNN policy.
4.3 Computation of safe weight sets and the value of
Problems and asssume a given value of e for which safety needs be verified. In order compute the largest value of e for which our approach can verify safety, we start with a small value of e and iteratively increase it until we reach value that cannot be certified or until the timeout reached, in order to compute as large safe weight set as possible. In each iteration, our Algorithm [ does not start from scratch but is initialized with the "nv and Dxpec from the previous successful iteration, i.e. attempting to enlarge the current safe weight set. Our iterative process significantly speeds up the search process compared to naively restarting our algorithm in every iteration.
4.4 Safe exploration reinforcement learning
Given a safe but non-optimal initial policy To, safe exploration reinforcement learning (SERL) concerns the problem of improving the expected return of яo while ensuring safety when collecting samples of the environment [44] [|35] 35). Our method from Section (.22 computing safe weight sets can be adapted to this setting with minimal effort. In particular, the safety bound for the intervals centered at the weight means can be used in combination with the rejection sampling to generate safe but randomized rollouts on the environment. Moreover, provides bounds on the gradient updates when optimizing the policy using Deep Q-learning or policy gradient methods, i.e., performing projected gradient descent. We sketch an algorithm for SERL in the Supplementary Material.
5 Experiments
We perform experimental evaluation of our proposed method for learning positive invariant neural networks that prove infinite time horizon safety. Our evaluation consists of an ablation study where we disable different core components of Algorithm I and measure their effects on the obtained
8

---

(a) Vector field of the system when controlled by the posterior's mean. Green/red arrows indicate empiri- cal safe/unsafe estimates.
(b) First guess of g/ Green area shows g niv orange area "M < 0. Red markers show the found counterexample.
(c) Final g proving the safety of system. Previous counterexam- ples marked in red.
Figure 2: Invariant learning shown on the inverted pendulum benchmark.
safety bounds and the algorithm's 's runtime. First, we run the algorithm without any re-training on the counterexamples. In the second step, we run A initializing Dapes with samples from Xo and X₂ only. Finally, we bootstrap the positive invariant network by initializing D with random samples from the state space labeled with Monte-Carke estimates of reaching the unsafe states. We consider environments with piecewise linear dynamic function, initial and unsafe state sets so that the verification steps of our algorithm can be reduced to MILP-solving using Gurobi (00). Details on our evaluation are in the Supplementary Material. Code is publicly available D.
We conduct our evaluation on three benchmark environments that differ in terms of complexity and safety specifications. We train two BNN policies for each benchmark- weights from the second layer on (with (O, 0.1) prior) and one with Bayesian weights in all layers (with (0, 0.05) prior). Recall, in our BNN encoding in Section 4.1 we showed that encoding of the BNN input layer requires additional constraints and extra care, since we do not know the signs of input neuron values. Hence, we consider two BNN policies in our evaluation in order to study how the encoding of the input layer affects the safe weight set computation.
pair, one with Bayesian
Our first benchmark represents an unstable linear dynamical system of the form I++1 = Ax, + Buy- A BNN policy stabilizes the system towards the point (0, 0). Consequently, the set of unsafe states is defined as {x E R2 |x 2 1.2], and the initial states as {z E R² |x] S 0.63.
Our second benchmark is the inverted pendulum task, which is classical non-linear control problem. The two state variables a and b represent the angle and angular velocity of pendulum that must be controlled in an upward direction. The actions produced by the policy correspond to torque applied to the anchor point. Our benchmark concerns a variant of the original problem where the non- loneariyyy in f is expressed by piecewise linear functions. The resulting system, highly unstable, as shown in Figure 2 The set of initial states corresponds to pendulum states in an almost upright position and with small angular velocity. The of unsafe states represents the pendulum falling down. Figure 2 visualizes the system and the learned invariant's decision boundary for the inverted pendulum task.
with trained policy, is
While the previous two benchmarks concern stability specifications, we evaluate our method on a non-Lyapunovian safety specification in our third benchmark. In particular, our third benchmark is a collision avoidance task, where the system does not stabilize to the same set of terminal states in every execution. The system is described by three variables. The first variable specifies the agent's own vertical location, while the other two variables specify an intruder's ' vertical and horizontal position. The objective is avoid colliding with the intruder who is moving toward the agent by lateral movement commands as the policy's actions. The initial states represent far-away intruders, and crashes with the intruder define the unsafe states.
Table [ shows the results of our evaluation. Our results demonstrate that re-training with the counterexamples is the key component that determines our algorithm's 's success. In all cases, except for the linear dynamical system, the initial guess the invariant candidate violates the invariant

---

Table 1: Results of our benchmark evaluation. The epsilon values are multiples of the weight's standard deviation σ. We evaluated several epsilon values, and the table shows the largest that could be proven safe. A dash "_" indicates an unsuccessful invariant search. Runtime in seconds.
No re-training
Init D Spec with Ag and Xu Verified
Bootstrapping D spec
Environment
Verified Runtime
Runtime
Verified
Runtime
Unstable LDS
3
1.5g
569
2a
760
Unstable LDS (all)
0.20
0.5g
0.5g
96
Pendulum
2
2g
220
2a
40
Pendulum (all)
0.2g
1729
1.5g
877
Collision avoid.
2
2x
154
Collision avoid. (all)
1.5g
225
Moreover, boostrapping Dapee with random points labeled by empirical estimates of reaching the unsafe states improves the search process significantly.
condition.
Conclusion
In this work formulated the safety verification problem for BNN policies in infinite time horizon systems, that asks to compute safe BNN weight sets for which every system execution is safe as long the BNN samples its weights from this set. Solving this problem allows re-calibrating the BNN policy to reject unsafe weight samples in order to guarantee system safety. We then introduced a methodology for computing safe weight sets in BNN policies in the form of products of intervals around the BNN weight's means, and a method for verifying their safety by learning positive invariant-like safety certificate. We believe that our results present an important first step in guaranteeing safety of BNNs for deployment in safety-critical scenarios. While adopting products of intervals around the BNN's weight means is natural choice given that BNN priors are typically unimodal distributions, this is still a somewhat restrictive shape for safe weight sets. Thus, an interesting direction of future work would be study more general forms of safe weight sets that could be used for re-calibration of BNN posteriors and their safety verification. Another interesting problem would be design an approach for refuting weight set unsafe which would complement our method, or consider closed-loop systems with stochastic environment dynamics.
Any verification method for neural networks, even suffers from scalability limitations due to the underlying complexity class [26] 24). Promising research
for neural networks in feedback loops,
directions on improving the scalability of our approach by potentially speeding up the constraint solving step are gradient based optimization techniques [22] and to incorporate the constraint solving step already in the training procedure 46
Since the aim of Al safety is to ensure that systems do not behave in undesirable ways and that safety violating events avoided,
not aware of any potential negative societal impacts.
Acknowledgments
This research was supported in part by the Austrian Science Fund (FWF) under grant Z211-NI (Wittgenstein Award), ERC CoG 863818 (FoRM-SMArt), and the European Union's Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie Grant Agreement No. 665385.
References
[1] Joshua Achiam, David Held, Aviv Tamar, and Pieter Abbeel. Constrained policy optimization. In International Conference on Machine Learning, pages 22-31. PMLR, 2017.
[2] Eitan Altman. Constrained Markov decision processes, volume 7. CRC Press, 1999.
[3] Dario Amodei, Chris Olah, Jacob Steinhardt, Paul Christiano, John Schulman, and Dan Mané. Concrete problems in ai safety. arXiv preprint arXiv:1606.06565, 2016.
10

---

[4] Felix Berkenkamp. Matteo Turchetta, Angela P. Schoellig, and Andreas Krause. Safe model-based reinforcement learning with stability guarantees. In Isabelle Guyon, Ulrike Von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett, editors, Advances Neural Information Processing Systems 30: Annual Con- ference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, pages 908-918, 2017. URL BRRLhtpps: / http:////roceeeeeeeeeeee
www.gs..nurrip.pp cctppe//207/ Abstract .html html
[5] Franco Blanchini and Stefano Miani. Ser-theoretic methods in control. Springer, 2008.
[6] Charles Blundell, Julien Cornebise, Koray Kavukcuoglu, and Daan Wierstra. Weight uncertainty in neural network. In International Conference on Machine Learning, pages 1613-1622. PMLR, 2015.
[7] Rudy Bunel, Ilker Turkaslan, Philip H. S. Torr, Pushmeet Kohli, and Pawan Kumar Mudigonda. A unified view of piecewise linear neural network verification. In Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa- Bianchi, and Roman Garnett, edi- tors, Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurlPS 20/8, December 3-8, 2018, Montréal, Canada, neurips.... wtcc/pppp//2018800
pages 4795-4804, 2018. URL hattps::/proceeetet 9e53225aabc335533366666aaaaa Abstrattta html
[8] Luca Cardelli, Marta Kwiatkowska, Luca Laurenti, Nicola Paoletti, Andrea Patane, and Matthew Wicker. Statistical guarantees for the robustness of bayesian neural networks. In Sarit Kraus, editor, Proceedings of the Twenty-Fighth International Joint Conference on Artificial Intelli- gence, IJCAI 2019, Macao, China, August 10-16, 2019, pages 5693-57000 ijeai.org, 2019. doi: 10.24966fiecaa.211177799 URL httllhttts://do..ooo 10. 24963/1jcaii 2019/789
[9] Ya-Chien Chang. Nima Roohi, and Sicun Gao. Neural Yyарuпоv control. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d' Alché-Buc, Emily B. Fox, and Roman Garnett, editors, Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurlPS 2019, December 8-14, 2019, Vancouver, BC, Canada, pages 3240-3249, 2019. URL Utthtttss Absttact. html
neurips wwcc/aape//aa 2019/
[10] Xin Chen, Erika Ábrahám, and Sriram Sankaranarayanan Flow*: An analyzer for non- linear hybrid systems. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification 25th International Conference. CAV 2013, Saint Petersburg, Russia, July 13- 19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pages 258-263. Springer, 2013. doi: 10. (0000997-3366223997777 178-3-642-55 39799-8-198888
18. htRpsttps:/// http///o..oorrg/// 10. 1007/
[11] Yinlam Chow, Ofir Nachum, Edgar A. Duéitez-Gzzmán, and Mohammad Ghavamzadeh. A lyapunov-based approach to safe reinforcement learning. In Samy Bengio, Hanna M. Wal- lach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi, and Roman Garnett, editors, Advances in Neural Information Processing Systems 31: Anmual Conference
Neural In- formation Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada. pages 8103-8112, 12. 2018. URL http:ppppppp.peppptttttt 445544405bb327766644bebff06666 wbw.://999940bttt.to.....
neurips. cc/ wwwpp//p////ppeeee Staper/2018/harr 2018/hash/
[12] Souradeep Dutta, Susmit Jha, Sriram Sankaramarayanan, and Ashish Tiwari. Output range analysis for deep feedforward neural networks. In NASA Formal Methods Symposium, pages 121-138. Springer, 2018
[13] Souradeep Dutta, Xin Chen, and Sriram Sankaranarayanan. Reachability analysis for neural feedback systems using regressive polynomial rule inference. In Necmiye Ozay and Pavithra Prabhakar, editors, Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Montreul, QC, Canada, April 16-18, 2019, pages 157-168. ACM, 2019. doi: 10. 14533322504433 1807. URL, httts::/t//ooii orgoiio.rg/1 1145/
3302504 .31950043311807 3311807

---

[14] Robert W. Floyd. Assigning meanings to programs. Proceedings of Symposium on Applied Mathematics. 19:19-32, 32, 1967. URL http://laser cs. umass. edu/ courses 621 Sar00//apers//eee
pdf
[15] Yarin Gal and Zoubin Ghahramani. Dropout as a bayesian approximation: Representing model uncertainty in deep learning. In Maria-Florina Balcan and Kilian Q. Weinberger, editors, Proceedings of the 33nd International Conference on Machine Learning, ICML 2016, New York City, NY, USA, June 19-24, 2016, volume 48 of JMLR Workshop and Conference Proceedings, pages 1050-1059. JMLR.org, 2016. URL httphttp:/// httt:://pproeeeding..... mlr www.mmrr...ss... pll.s///////////// gal16 html
[16] Sicun Gao, Jeremy Avigad. and Edmund M Clarke. ó-complete decision procedures for satisfiability over the reals. In International Joint Conference on Automated Reasoning, pages 286-300, Springer, 2012.
[17] Timon Gehr, Matthew Mirman, Dana Trachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin T. Vechev. A12: safety and robustness certification of neural networks with abstract interpretation. In 2018 IEEE Symposium on Security and Privacy, SP 2018, Proceedings, 21-23 May 2018, San Francisco, California, USA, pages 3-18. IEEE Computer Society, 2018. doi: 10.1 109/1002008.000000 8.00058.. URL URR.https://// http::://doo.. 1o0o 1109/SP. http///......... 20..20018.000 00058
[18] Peter Geibel. Reinforcement learning for mdps with constraints. In Johannes Fürnkranz, Tobias Scheffer, and Myra Spiliopoulou, editors, Machine Learning: ECML 2006, 17th European Conference on Machine Learning, Berlin, Germany, September 18-22, 2006, Proceedings, volume 4212 of Lecture Notes Computer Science, pages 646 653. Springer, 2006. doi: (0.1007/118718421 63. URL https:://oii..... org/ 10. 1007 01000/111888822211
[19] Sophie Gruenbacher, Jacek Cyranka, Mathias Lechner, Md Ariful Islam, Scott A Smolka, and Radu Grosu. Lagrangian reachtubes: The next generation. 2020 59th IEEE Conference on Decision and Control (CDC), pages 1556-1563. IEEE, 2020.
[20] LLC Gurobi Optimization. Gurobi optimizer reference manual, 2021. URL http: www
gurobi com
[21] Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun. Delving deep into rectifiers: Surpassing human-level performance imagenet classification. In 2015 IEEE International Conference on Computer Vision, ICCV 2015, Santiago, Chile, December 7-13, 2015, pages 1026-1034. IEEE Computer Society, 2015, doi: 10.1 0..100//CC2.221..223...
URL https
110./ICCVIICCC 2015. 123
[22] Patrick Henriksen and Alessio R. Lomuscio. Efficient neural network verification via adaptive refinement and adversarial search. In ECAL, volume 325 of Frontiers in Artificial Intelligence and Applications, pages 2513-2520. IOS Press, 2020.
[23] Thomas A. Henzinger, Mathias Lechner, and Dorde Zikelic. Scalable verification of quantized neural networks. In AAAI, pages 3787-3795. AAAI Press, 2021.
[24] Radoslav Ivanov, James Weimer, Rajeev Alur, George J. Pappas, and Insup Lee. Verisig: verifying safety properties of hybrid systems with neural network controllers. In Necmiye Ozay and Pavithra Prabhakar, editors, Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Montreal, QC. Canada, April 16-18, 2019, pages 169-178. ACM, 2019. doi: 10.1145/3302504.33115 / //doi.org/ 10. 1145/300254.33. 3311806
URL https
[25] Kevin Jarrett, Koray Kavukeuoglu, Marc' Aurelio Ranzato, and Yann LeCun. What is the best stale architecture for object recognition? In IEEE 12th International Conference on Computer Vision, ICCV 2009, Kyoto, Japan, September 27 October 4, 2009, pages 2146-2153. IEEE Computer Society, 2009. doi: 10. 10.100//CCC2222995555550 54.509999549999... URL https 7/doi. 100...19///00 1109/ICCV 2009. 55594699
[26] Guy Katz, Clark W. Barrett, David I.. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification 29th International Conference, CAV 2017,
12

---

Heidelberg, Germany, July 24-28, 2017. Proceedings. Part I, volume 10426 of Lecture Notes in Computer Science, pages 97-117. Springer, 2017. doi: 10. 00007/978---31--3388--78 URL
https://doi. http::///ooo.oo//////1 000779988-3-31--638877
[27] Guy Katz, Derek A. Huang, Duligur lbeling. Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljic, David L. Dill, Mykel J. Kochenderfer, and Clark W. Barrett. The marabou framework for verification and analysis of deep neural networks. In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verifica- lion - slst International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I, volume 11561 of Lecture Notes in Computer Science, pages 443-452. Springer, 2019. doi: 10. 10.1007/978-311 0-1-0-300255---- 26. URL htttp:://doii org/ 10. 1007/ 978-3-030 178-3-030-25540-44
[28] Alex Kendall, Jeffrey Hawke, David Janz, Przemyslaw Mazur, Daniele Reda, John-Mark Allen, Vinh-Dieu Lam, Alex Bewley, and Amar Shah. Learning to drive in a day. In 2019 International Conference Robotics and Automation (ICRA), pages 8248 -284. IEEE, 2019.
[29] Hassan K Khalil and Jessy W Grizzle. Nonlinear systems, volume 3. Prentice hall Upper Saddle River, NJ, 2002.
[30] Mathias Lechner, Ramin Hasani, Alexander Amini, Thomas A Henzinger, Daniela Rus, and Radu Grosu, Neural circuit policies enabling auditable autonomy. Nature Machine Intelligence, ((00):642-652 2020.
[31] Alessio Lomuscio and Lalit Maganti. An approach to reachability analysis for feed-forward relu neural networks. arXiv preprint arXiv:/706.07355. 2017.
[32] David J. C. MacKay. A practical bayesian framework for backpropagation networks. Neural Comput., 4(3):448 472, 1992. doi: 10.1166//ecco.11922...344
URL httpp:///o//
1162/neco. 1992 4.3.4.3.44. 448
[33] Rowan McAllister, Yarin Gal, Alex Kendall, Mark Van Der Wilk, Amar Shah, Roberto Cipolla, and Adrian Weller. Concrete problems for autonomous vehicle safety: Advantages of bayesian deep learning. International Joint Conferences on Artificial Intelligence, Inc., 2017.
[34] Rhiannon Michelmore, Matthew Wicker, Luca Laurenti, Luca Cardelli, Yarin Gal, and Marta Kwiatkowska. Uncertainty quantification with statistical guarantees in end-to-end au- tonomous driving control. In 2020 IEEE International Conference on Robotics and Automation, ICRA 2020, Paris, France, May 31 August 31, 2020, pages 7344-7350. IEEE, 2020. doi: 10.1 1091019//444955..00 2020.91900.99920
httlttttt////o.oo
(119//IIIA494444 2020
9196844
[35] Yashwanth Kumar Nakka, Anqi Liu, Guanya Shi, Anima Anandkumar, Yisong Yue, and Soon-
Jo Chung. Chance-constrained trajectory optimization for safe exploration and learning of nonlinear systems. IEEE Robotics and Automation Letters, 6(2):389-396, 2020.
[36] Radford M Neal. Bayesian learning for neural networks, volume 1 118. Springer Science & Business Media, 2012.
[37] Andrea Peruffo, Daniele Ahmed, and Alessandro Abate. Automated and formal synthesis of neural barrier certificates for dynamical models. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 April 1, 2021, Proceedings, Part I, volume 12651 of Lecture Notes in Computer Science, pages 370-388. Springer, 2021. I. doi: 10. 030---000-7770000 0200--06-------2---2-----
20. URL TRLhhtts:://ao org/10
[38] Stephen Prajna and Ali Jadbabaie. Safety verification of hybrid systems using barrier certificates. In Rajeev Alur and George J. Pappas, editors. Hybrid Systems: Computation and Control, 7th International Workshop, HSCC 2004, Philadelphia, PA, USA, March 25-27, 2004, Proceedings, volume 2993 of Lecture Notes in Computer Science, pages 472- Springer, 2004. doi: 10. 0-7778--3-500--4433333
32. URL /ttp::t://aiiioo/////..../ 1107:////11110000///00//
32
13

---

[39] Stephen Prajna, Ali Jadbabaie, and George J. Pappas. A framework for worst-case and stochas- tic safety verification using barrier certificates. IEEE Trans. Autom. Control., 5415):1415- 1428, 2007. doi: 10.1 10.1109/AAC222079907775
Utt.htss:: org/10.////. 201111///TC.200 2007
902736
[40] Wenjie Ruan, Xiaowei Huang, and Marta Kwiatkowska. Reachability analysis of deep neu- ral networks with provable guarantees. In Jérôme Lang, editor. Proceedings of the Twenty- Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden, pages 2651-2659. ijcai.org. 2018. doi: 10. 10.24963/jjeai.000 2018//36.. URL
httts://doi.orgee 10. 24963/ 2 2018/368
[41] Dinggang Shen, Guorong Wu, and Heung-11 Suk. Deep learning in medical image analysis. Annual review of biomedical engineering. 19:221-248, 2017.
[42] Christopher A Strong, Haoze Wu, Aleksandar Zeljić, Kyle Julian, Guy Katz, Clark Barrett, and Mykel J Kochenderfer. Global optimization of objective functions represented by relu networks. arXiv preprint urXiv:20100032288 2020.
[43] Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In 7th International Conference Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. URL https
/ //openreview net/forumm iid Hyrrrummiid-HIIIiRReeeP HyGIdiRqtm
[44] Eiji Uchibe and Kenji Doya. Constrained reinforcement learning from intrinsic and extrinsic rewards. In 2007 IEEE 6th International Conference on Development and Learning, pages 163-168. IEEE, 2007.
[45] Matthew Wicker, Luca Laurenti, Andrea Patane, and Marta Kwiatkowska. Probabilistic safety for bayesian neural networks. In Ryan P. Adams and Vibhav Gogate, editors, Proceedings of the Thirty-Sixth Conference on Uncertainty Artificial Intelligence, UAI 2020, virtual online, August 3-6, 2020, volume 124 of Proceedings of Machine Learning Research, pages 1198-1207. AUAI Press, 2020. URL http:tt::////ceeeiiiiii
mlr www.ppres//iee ht////114/////// wwtp//////ceee http:wiccker// html
[46] Huan Zhang, Hongge Chen, Chaowei Xiao, Sven Gowal, Robert Stanforth, Bo Li, Duane S. Boning, and Cho-Jui Hsieh. Towards stable and efficient training of verifiably robust neural networks. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net, 2020. URL https://openrevilt net/forum? iiciumm?ii-eeeee hit.rrmmmidSSkkukrrrerr
[47] Hengjun Zhao, Xia Zeng, Taolue Chen, and Zhiming Liu. Synthesizing barrier certificates using neural networks. In Aaron D. Ames, Sanjit Seshia, and Jyotirmoy Deshmukh, editors, HSCC '20: 23rd ACM International Conference on Hybrid Systems: Compulation and Control, Sydney, New South Wales, Australia, April 21-24, 2020, pages 25:1-25:111 ACM, 2020. doi: 10.114533365365.3888
URL https:
10. 1051111333661161555 30t.//333533665563 338222666666366222222333333333
Checklist
1. For all authors...
(a) Do the main claims made in the abstract and introduction accurately reflect the paper's
contributions and scope? [Yes]
(b) Did you describe the limitations of your work? [Yes] In our conclusion in Section 6 we say that the current form of safety weight set is somewhat restrictive although it is naturally motivated. Thus, an interesting direction of future work is to consider more general safe weight sets. Another potential limitation is the scalability of some of the constraint solving techniques that we use in this work, which we discuss in Section 4.1 However, all of the constraint-solving techniques we discuss were already used in previous work for RL safety and stability verification.
(c) Did you discuss any potential negative societal impacts of your work? [Yes] As the aim of Al safety is to guarantee that safety-critical events are avoided, we are not aware of any negative societal impact of our work. See Section 6
14

---

(d) Have you read the ethics review guidelines and ensured that your paper conforms to them? [Yes]
2. If you including theoretical results...
(a) Did you state the full set of assumptions of all theoretical results? [Yes] In Section we say that our work considers NNs with ReLU activation functions and that our framework be applied to other piecewise linear activations. Thus, when verify safe weight sets, our safety certificate also takes the form of a deterministic NN with ReLU activations. When it comes to solving systems of constraints in algorithm, in Section 4.1 we clearly state the assumptions each constraint solving technique makes. (b) Did you include complete proofs of all theoretical results? [Yes] All proofs are included in the Supplementary Material.
3. If you experiments...
(a) Did you include the code, data, and instructions needed to reproduce the main experi- mental results (either the supplemental material or as a URL)? [Yes] Weights, code, and data are provided.
(b) Did you specify all the training details (e.g., data splits, hyperparameters, how they were chosen)? [Yes]
(c) Did you report error bars (e.g., with respect to the random seed after running experi- ments multiple times)? [N/A]
(d) Did you include the total amount compute and the type of resources used (e.g., type of GPUs, internal cluster, cloud provider)? [Yes]
4. If you are using existing assets (e.g., code, data, models) or curating/releasing new assets...
(a) If your work uses existing assets, did you cite the creators? [Yes]
(b) Did you mention the license of the assets? [Yes]
(c) Did you include any assets either in the supplemental material or as URL? [Yes]
(d) Did you discuss whether and how consent
obtained from people whose data you're
using/curating? [N/A] MIT license, not applicable
(e) Did you discuss whether the data you are using/curating contains personally identifiable information or offensive content? [Yes]
5. If you used crowdsourcing conducted research with human subjects...
(a) Did you include the full text of instructions given to participants and screenshots, if applicable? [N/A] We did not use crowdsourcing or conduct research with human subjects.
(b) Did you describe any potential participant risks, with links Institutional Review Board (IRB) approvals. if applicable? [N/A] We did not use crowdsourcing or conduct research with human subjects.
(c) Did you include the estimated hourly wage paid to participants and the total amount spent on participant compensation? [N/A] We did not use crowdsourcing or conduct research with human subjects.
15


Reviews:
[{"review_id": "sqjVuaYHgH8", "reviewer": "Reviewer_RfGA", "summary": "In this paper the authors consider the problem of verifying safety in BNNs.  At a high level, they seek a way to compute a set of safe weight sets of a BNN such that its outputs can not fall within some “unsafe set.” They show doing so for two contexts, the first aiding the second. In the first context they take a standard feed forward BNN, while in the second they consider a closed loop system under some dynamics where the policy at each time point is implemented by a BNN.", "questions": "", "limitations": "", "rating": 7, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "# Strengths\nThe authors do a good job of why this is an important problem in the literature; i.e. safety critical applications and in the context of exploration RL where a policy would like to be designed such that we don’t wind up in “unsafe” states.  Literature review is also highly appreciated and does a good job of further motivating the problem and the authors contributions. By starting with the problem of vanilla feed forward BNNs the extension to closed loop systems governed by some dynamics is made more natural.\n\nOutlining several ways of solving the constraints (MILP, Reluplex, NRA-SMT) demonstrates that there are several ways of approaching the problem each with their own strengths and weaknesses; and also that there exist methods that make it viable to do so.\n\nI find the learner and verifier algorithm for learning safe positive invariants creative as well.  Though complicated (which I do not find a downside) as far as I can tell the logic is sound and trying to give the correct intuition was also appreciated.\n\nChoice of experiments seem sufficient as well; the paper is fairly theory heavy so having some simple experiments to show the efficacy of the proposed approach was good. Also glad to see runtimes listed as this would have been one of my bigger questions.\n\n\n\n# Other/Questions\nI am wondering how is epsilon usually chosen? I’m not sure this is an appropriate question but perhaps a little more intuition regarding this could have been given in the paper. As a follow up to this I would also like to ask why a uniform epsilon across all weights/biases (I see this was addressed in the conclusion but Im still curious)? \n\nAs this does not seem like a well explored problem in the literature I think the work presented here is a good first step; as such systems become more prominent guaranteeing safety critical aspects will become increasingly more necessary.\n\n# POST REBUTTAL\nHaving read through the reviews as well as the authors responses I am satisfied and leave my score unchanged. To the authors, thanks for some clarifications about eps. I also wanted to say that I think the suggestions offered by axJp seem like they will be a great addition to the final paper.", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "The authors adequately addressed the limitations and potential negative societal impact of their work.", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "7"}, "extra_text": {}}, {"review_id": "sngHolcPFva", "reviewer": "Reviewer_axJp", "summary": "This paper considers a safety verification problem for a BNN policy over an infinite time horizon, in the setting of a discrete-time closed-loop dynamical system. Since most BNN policies do not satisfy safety properties due to the unbounded supports of the BNNs’ weights, the paper considers the problem of finding an appropriate subset (called safe weight sets) of such an unbounded support which makes the desired safety properties hold. This problem can be viewed as a generalization of the original safety verification problem. The paper solves the generalized problem by computing a safe inductive invariant, which is represented by a separate NN, searched by a training procedure, and verified by a separate verifier module. The proposed method is evaluated on several benchmarks, and produces promising results.\n", "questions": "", "limitations": "", "rating": 7, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "## Strengths.\n\n(1) This paper considers an important, interesting problem. In particular, it introduces a new problem of computing safe weight sets, which generalizes the original safety verification problem, to make the original verification problem produce more meaningful results. Further, a solution to the new problem can allow us to make a BNN policy safe via rejection sampling, which can be used importantly in safe-critical settings.\n\n(2) The following parts of the proposed method look novel to me: using a NN to represent a safe inductive invariant, and casting the search problem for a safe inductive invariant into a NN learning problem. Note that most other parts of the method (considering inductive invariants, applying a verifier, and utilizing counterexamples from the verifier) are somewhat standard at least in the programming languages area.\n\n(3) The proposed method for the new generalized problem is shown to perform well on several benchmarks. \n\n(4) The paper is overall well-written (except for two specific points described below). Also the technical contents of the paper are sound.\n\n## Weaknesses.\n\n(1) The writing needs a bit more improvement. First, throughout the paper I got the impression that safe weight sets are automatically searched or learned by the proposed method, but this turns out not to be the case---the proposed method assumes a particular safe weight set (namely the product of intervals of radius \\epsilon), and does not give any efficient way of finding safe weight sets. This point should be clarified in the paper.\n\nSecond, according to the experimental results, the bootstrap trick seems to be critical to good performance but it is not explained in detail in the text. Some more details on the bootstrap trick should be provided.\n\n(2) The paper has two main limitations. First, as mentioned in Sec 6, the paper considers only a simple form of safe weight sets. Relaxing this restriction would be an important future work. Second, finding or learning safe weight sets automatically and efficiently is another important problem not resolved by this paper---in the experiments different \\epsilon values are simply tried. Even with the two limitations, I think this paper still maintains its significance as it provides first steps towards more practical safety verification of BNNs.\n\n## Questions & Comments.\n\n- Can you show that the verified \\epsilon values in Table 1 (e.g., 2\\sigma) is (or close to) maximal? That is, can you show concretely that a large \\epsilon value indeed makes \\pi unsafe? If possible, that would strengthen the experimental results.\n\n- Why do the experiments use two different BNN policies? Was there any particular criteria to choose the two particular BNNs used in the paper?\n\n- Line 131-132. Several “U”s here should be in \\mathcal.\n- Line 168. Provide the type of \\pi (i.e., \\pi : X \\to X), as this \\pi is different from \\pi : X \\to D(U) in the above.\n- From Line 201. Several “l”s in the subscript of x (e.g., x_l) should be “k”.\n- Line 210. “x^out_0” should be “x_0,pos”.\n- Line 219, 221. “Equations 3-4” and “equation 5” do not exist in the above equations.\n\n-----\n\n**Updates after author response.** Thank the authors for answering my questions. I am still positive on the paper and will keep the same score.", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "For limitations, refer to the main review. Societal impact is discussed in the paper.", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "8"}, "extra_text": {}}, {"review_id": "YbZTPHz35f4", "reviewer": "Reviewer_Md7z", "summary": "We extend verifications of (piece-wise linear or SMT compliant) neural networks to bayesian neural networks. ", "questions": "", "limitations": "", "rating": 6, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "### Clarity\nThis paper is clear, I have no problem following it\n\n### Originality\nI think this work is predictable, as just adding another quantifier \"\\forall range of values in BNN weights\" is SMT compliant, and most verification techniques to verify deterministic NN can be ported over more or less directly. However this does not diminish the contribution of this work: Being able to verify a non-deterministic agent (such as one used in exploration and learning of an environment) behaviour in an infinite time-horizon system is a very important problem, especially in the domain of safe exploration that this paper considers.\n\n### Quality\nThe proofs on using invariants to guarantee safety in the infinite horizon setting is a good and sound. The key contribution to me is how this paper bypass the undecidable hardness of generating an invariant by using learning to _propose_ an invariant, then using a decision procedure to _verify_ it, making it tractable. The decision (the same as other NN+SMTVerification works) is made to treat distributions as ranges, then applying rejection sampling makes this approach compliant to off-the-shelf SMT/Linear solvers, which has an easier time encoding ranges of values and existence of values as opposed to reasoning over distributions.\n\n### Significance\nThe complaint here is the typical one for verification: How does this scale to a realistic scenario? Presumably given a sufficiently difficult environment, with non-linear dynamics or a sufficiently complex neural network (say a transformer with some nonlinearity), this approach will be not applicable. In a sense, if the best example is a 2D 2 dot AND 1 dot is restricted to a line (not even on an arbitrary spline, presumably spline breaks SMT?) simulation, how do we proceed in taking this technique and apply it to a more complex domain (such as 2D 5 dots, maybe 1 is a car and other 4 pedestrians, with some constraints on the paths they can take)? While I am not concerned that the results present in this work are preliminary and stilted, what are some avenues forward that you can see (assuming solver techs are not going to improve)?\n\nSimilarly, \"However, all of the constraint-solving techniques we discuss were already used in previous work for RL safety and stability verification\" is bit of a kicking the can down the road for me.\n\ngoing to keep my original score after reading the review, as the same message stands: this is a good paper, but the best example is 2D with 2 dots and 1 dot is restricted to a line.", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "this work addresses them adequately ", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "1 hour"}, "extra_text": {}}, {"review_id": "RE5zfQiJQQH", "reviewer": "Reviewer_dPLB", "summary": "The paper considers the problem of safely controlling a known, discrete-time system with a stochastic BNN policy with ReLU activations where randomness enters through the policy's weights. Safety is defined in terms of avoiding a set of states that are known to be safe over an infinite time horizon. The paper first considers the problem of determining whether BNN outputs lie in a set of unsafe actions. To this end, the paper proposes to approximate weights by bounding boxes in a set W_epsilon and verifies safety through a corresponding mixed-interger linear program. While the BNN's distribution typically has unbounded support, for any verified epsilon it can be made safe through rejections sampling.\n\nThe developed methodology is then used for the safe control problem, where a neural network is used together with a classification problem in order to learn an invariant set under the policy. The algorithm proceeds iteratively by fitting the neural network and then finding counter-examples through a mixed-integer program that are then added to the training set. The result is a trained classifier for safe/unsafe states for a given policy and value epsilon.\n\nThe approach is evaluated on two linear and one piecewise-linear dynamic systems with action dimension one and state dimensions between one and three, showing that for these problems the proposed method can verify safety within a reasonable runtime.", "questions": "", "limitations": "", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "The paper is clearly written and easy to follow. There are some minor inconsistencies in variable naming that I list at the end of the review. The problem setting that the paper sets out to solve is interesting and safety is certainly a relevant concern for neural networks. However, it is not clear how one would obtain a policy that has uncertain weights, given that it is usually the environment that is unknown. The paper could better motivate why this approach is significance of the problem.\n\nThe methodology in the paper focuses on two problems. The first one considers verifying that the output of a network does not lie withing a given set, which is verified using a MILP. While I'm not sure the particular problem of encoding weight uncertainty in the MILP has been considered, since epsilon is assumed to be known the structure is very close to previous constructions. As such I see the main contribution of the paper in how the second problem is solved.\n\nOne of my biggest concerns is that the paper over-promises initially and is not explicit about all the limitations. In the abstract the paper promises to provide infinite-horizon safety for general BNN policies in reinforcement learning. This scope the reduces over the course of the paper:\n- First environments are restricted to be deterministic and fully known, which means that we are no longer in the reinforcement learning setting, but instead dealing with control (known environment).\n- Next the BNN policy is replaced by a policy where each weight is allowed to vary independently within a Box. This is reasonable for a prior BNN (i.e., all weights are sampled iid), but any kind of trained/posterior weights are generally strongly correlated. For this setting assuming independent bounding boxes can potentially be a strong over-approximation. At the same time there is a statement that we can verify the full BNN support by letting epsilon -> infinity, which is essentially allowing weights to shift between +/-infinity, arguably not a useful scenario.\n- Lastly, to find counter-examples the paper proposes a complex non-convex problem, which as far as I can tell can only be solved using the introduced methodology if the environment dynamics are piecewise-linear. This also shows in the experiments, where the piecewise-linear inverted pendulum is essentially linearized at two points, one of which seems to excluded through the constraint set.\n\nTogether these are strong limitations imposed on the approach that would need to be discussed and evaluated in the paper and should be clear from the beginning.\n\nThe experiments are restricted to synthetic (policy is pre-defined and weight uncertainty is set to low, manually defined values), simple, and low dimensional problems (state dimension < 3, action dimension = 1, and 2-layer networks with 16 units). There is no discussion on the scalability of the approach and there are no comparisons the existing method (e.g., the sampling-based methods mentioned in the related work). Additionally, only single-runs are reported, even though the training process for the neural network classifier is likely to be noisy so that error bars on compute time and performance would be appropriate. In my opinion indicated this as [N/A] in the checklist is not appropriate here.\n\n### Summary\n\nOverall between the lack of motivation for the setting (where does my BNN policy come from), the limited discussion of the requirements, limitations and assumptions, together with the limited experiments without comparison against other methods make this paper, in my opinion, not ready for NeurIPS in its current form. \n\n### Stylistic and minor comments\n\n- Fig. 1 should not be wrapped in the text, since NeurIPS has a single-column format.\n- X_u is defined as both the set of unsafe actions and states depending on context. Maybe differentiating between these two sets notationally could improve clarity.\n- pi is defined as a composition of ReLU layers, but presumably there's no ReLU on the output\n- There is some confusion between the number of layers in Sec. 4.1. In the text it is \"k\", while in the system constraints it is \"l\"\n- In the system constraints, x_l is not defined in terms of x_{l-1}/x_{k-1}. \n- The paper checklist 4b) indicates that licences of cited assets are provided (e.g., gurobi) are stated, but I could not find any mention of them in the text or appendix.\n\n### Post-rebuttal\n\nIncreased score after reading the author response, but the concerns about restrictive assumptions, scalability, and practical relevance remain.", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "Limitations\n-----------\nSocietal impact is addressed, but limitations are not discussed sufficiently as mentioned in the main review\n- Ignoring potential correlations between BNN weights\n- Box-approximations to non-Gaussian distributions in general\n- known, deterministic dynamics. Piecewise-linearity\n- Scalability of the MIPs", "review_text": "", "extra_scores": {"ethical_concerns": "They are addressed at the end of the conclusion", "needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "3"}, "extra_text": {}}]

Author rebuttal:

Meta-review: The manuscript provides a theoretical framework and analysis for verifying safety in BNNs. Reviewers generally agree that it is well written and novel. Reviewers have also noted limitations and strong assumptions, and I believe the rebuttal process has been instrumental to improving the manuscript. I strongly suggest making the proposed changes in the final manuscript.
Decision: Accept (Poster)