Infinite Time Horizon Safety of Bayesian Neural Networks
Year: 2022

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.

heading: 1 Introduction
text: The success of deep neural networks (DNNs) across different domains has created the desire to apply them in safety-critical applications such as 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 a family of neural networks that place distributions over their weights [36]. This allows learning uncertainty in the 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 (e.g. Gaussian) weight distributions. This makes BNNs very appealing for robotic and medical applications [33] where uncertainty is a central component of data.
Despite the large body of literature on verifying safety of DNNs, the formal safety verification of BNNs has received less attention. Notably, [8, 45, 34] have proposed sampling-based techniques for obtaining probabilistic guarantees about BNNs. Although these approaches provide some insight
∗Equal Contribution.
35th Conference on Neural Information Processing Systems (NeurIPS 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 safety over an unbounded time horizon.
In this work, we study the safety verification problem for BNN policies in safety-critical systems over the infinite time horizon. Formally, we consider discrete-time closed-loop systems defined by a dynamical system and a BNN policy. Given a set of initial states and a 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.
Our approach to restrict the support of the weight distribution is necessary as BNNs with Gaussian weight priors typically produce output 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 1. 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 a 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 a 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, we phrase the search for an 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, we re-train the candidate on 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.
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 a 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 it allows re-calibrating BNN policies via rejection sampling to guarantee safety. 2. We introduce a 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 a deterministic neural network. 3. We evaluate our methodology on a series of benchmark applications, including non-linear systems and non-Lyapunovian safety specifications.

heading: 2 Related work
text: Verification of feed-forward NN Verification of robustness and safety properties in feed-forward DNNs has received much attention but remains an active research topic [26, 23, 17, 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 feed-forward BNNs has been considered in [8] by using samples to obtain statistical guarantees on the safety probability. The work of [45] also presents a sampling-based approach, however it provides certified lower bounds on the safety probability.
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 on 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, 18]. 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) [1]. Despite these algorithms providing a 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 ”stability”, 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 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 [11] to ensure safety in CMDPs during training. Recently, the work of [9] presented a method for learning a policy as well as a neural network Lyapunov function which guarantees the stability of the policy. Similarly to our work, their learning procedure is counterexample-based. However, unlike [9], our work considers BNN policies and safety definitions that do not require returning to a set of ground states.
Barrier functions for dynamical systems Barrier functions can be used to prove infinite time horizon safety in dynamical systems [38, 39]. Recent works have considered learning neural network barrier functions [47], and a counterexample-based 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 [14] and positive invariants for dynamical systems [5].

heading: 3 Preliminaries and problem statement
text: We consider a discrete-time dynamical system
xt+1 = f(xt,ut), x0 ∈ X0.
The dynamics are defined by the function f : X × U → X where X ⊆ Rm is the state space and U ⊆ Rn is the control action space, X0 ⊆ X is the set of initial states and t ∈ N≥0 denotes a discretized time. At each time step t, the action is defined by the (possibly probabilistic) positional policy π : X → D(U), which maps the current state xt to a distribution π(xt) ∈ 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 ut ∼ π(xt), and together with the current state xt of the system gives rise to the next state xt+1 of the system according to the dynamics f . Thus, the dynamics f together
with the policy π form a closed-loop system (or a 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 X0 of the system, we say that a sequence of state-action pairs (xt,ut)∞t=0 is a trajectory if x0 ∈ X0 and we have ut ∈ supp(π(xt)) and xt+1 = f(xt,ut) for each t ∈ N≥0. A neural network (NN) is a function π : Rm → Rn that consists of several sequentially composed layers π = l1 ◦ · · · ◦ lk. Formally, a NN policy maps each system state to a Dirac-delta distribution which picks a single action with probability 1. Each layer li is parametrized by learned weight values of the appropriate dimensions and an activation function a,
li(x) = a(Wix + bi),Wi ∈ Rni×mi ,bi ∈ Rni .
In this work, we consider ReLU activation functions a(x) = ReLU(x) = max{x,0}, although other piecewise linear activation such as the leaky-ReLU [25] and PReLU [21] are applicable as well.
In Bayesian neural networks (BNNs), weights are random variables and their values are sampled, each according to 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 to 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 [36], variational inference [6] or dropout [15].
When the policy in a dynamical system is a BNN, the policy maps each system state xt to a probability distribution π(xt) 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 πw,b. The action of the system is then defined as ut = πw,b(xt). Formal definition of the distribution π(xt) 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 a subprocedure in our solution to the second problem, the reason why we state it 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 q is the dimension of b. For each 1 ≤ i ≤ p, let µi denote the mean of the random variable wi. Similarly, for each 1 ≤ i ≤ q, let µp+i denote the mean of the random variable bi. Then, for each ∈ [0,∞], we define the set Wπ of weight vectors via
Wπ = p+q∏ i=1 [µi − , µi + ] ⊆ Rp+q.
We now proceed to defining our safety problem for feed-forward BNNs. Suppose that we are given a feed-forward BNN π, a set X0 ⊆ Rm of input points and a set Xu ⊆ Rn of unsafe (or bad) output points. For a concrete vector (w,b) of weight values, let πw,b to be the (deterministic) NN defined by these weight values. We say that πw,b is safe if for each x ∈ X0 we have πw,b(x) 6∈ Xu, i.e. if evaluating πw,b on all input points does not lead to an unsafe output.
Problem 1 (Feed-forward BNNs). Let π be a feed-forward BNN, X0 ⊆ Rm a set of input points and Xu ⊆ Rn a set of unsafe output points. Let ∈ [0,∞]. Determine whether each deterministic NN in {πw,b | (w,b) ∈Wπ } is safe.
Next, we define our safety problem for closed-loop systems with BNN policies. Consider a closedloop system defined by a dynamics function f , a BNN policy π and an initial set of states X0. Let Xu ⊆ X be a set of unsafe (or bad) states. We say that a trajectory (xt,ut)∞t=0 is safe if xt 6∈ Xu for all t ∈ N0, hence if it does not reach any unsafe states. Note that this definition implies infinite time horizon safety of the trajectory. Given ∈ [0,∞], define the set Trajf,π to be the set of all system trajectories in which each sampled weight vector belongs to Wπ .
Problem 2 (Closed-loop systems with BNN policies). Consider a closed-loop system defined by a dynamics function f , a BNN policy π and a set of initial states X0. Let Xu be a set of unsafe states. Let ∈ [0,∞]. Determine whether each trajectory in Trajf,π 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 =∞.

heading: 4 Main results
text: In this section we present our method for solving the safety problems defined in the previous section, with Section 4.1 considering Problem 1 and Section 4.2 considering Problem 2. Both problems consider safety verification with respect to a given value of ∈ [0,∞], so in Section 4.3 we present our method for computing the value of for which our solutions to Problem 1 and Problem 2 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.

heading: 4.1 Safe weight sets for feed-forward BNNs
text: Consider a feed-forward BNN π, a set X0 ⊆ Rm of inputs and a set Xu ⊆ Rn of unsafe output of the BNN. Fix ∈ [0,∞]. To solve Problem 1, we show that the decision problem of whether each deterministic NN in {πw,b | (w,b) ∈ Wπ } is safe can be encoded as a system of constraints and reduced to constraint solving.
Suppose that π = l1 ◦ · · · ◦ lk consists of k layers, with each li(x) = ReLU(Wix + bi). Denote by Mi the matrix of the same dimension as Wi, with each entry equal to the mean of the corresponding random variable weight in Wi. Similarly, define the vector mi of means of random variables in bi. The real variables of our system of constraints are as follows, each of appropriate dimension:
• x0 encodes the BNN inputs, xl encodes the BNN outputs; • xin1 , . . . , x in l−1 encode vectors of input values of each neuron in the hidden layers; • xout1 , . . . , x out l−1 encode vectors of output values of each neuron in the hidden layers; • x0,pos and x0,neg are dummy variable vectors of the same dimension as x0 and which will be used to distinguish between positive and negative NN inputs in x0, 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:
x0 ∈ X0, xl ∈ Xu (Input-output conditions)
xouti = ReLU(x in i ), for each 1 ≤ i ≤ l − 1 (ReLU encoding)
(Mi − · 1)xouti + (mi − · 1) ≤ xini+1, for each 1 ≤ i ≤ l − 1 xini+1 ≤ (Mi + · 1)xouti + (mi + · 1), for each 1 ≤ i ≤ l − 1
(BNN hidden layers)
x0,pos = ReLU(x0), x0,neg = −ReLU(−x0) (M0 − · 1)x0,pos + (M0 + · 1)x0,neg + (m0 − · 1) ≤ xin1 xin1 ≤ (M0 + · 1)xout0 + (M0 − · 1)x0,neg + (m0 + · 1)
(BNN input layer)
Denote by Φ(π,X0,Xu, ) the system of constraints defined above. The proof of Theorem 1 shows that it encodes that x0 ∈ X0 is an input point for which the corresponding output point of π is unsafe, i.e. xl = π(x0) ∈ Xu. The first equation encodes the input and output conditions. The second equation encodes the ReLU input-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 is in Wπ . For hidden layers, we know that the output value of each neuron is nonnegative, i.e. xouti ≥ 0 for the i-th hidden layer where 1 ≤ i ≤ l − 1, and so
(Mi − · 1)xouti ≤ (Mi + · 1)xouti .
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 x0 and so we introduce dummy variables x0,pos = ReLU(x0) and x0,neg = −ReLU(−x0) in equation 5. 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 1 shows that Problem 1 is equivalent to solving the system of constraints Φ(π,X0,Xu, ). Its proof can be found in the Supplementary Material.
Theorem 1. Let ∈ [0,∞]. Then each deterministic NN in {πw,b | (w,b) ∈ Wπ } is safe if and only if the system of constraints Φ(π,X0,Xu, ) is not satisfiable.
Solving the constraints Observe that , Mi and mi, 1 ≤ i ≤ l − 1, are constant values that are known at the time of constraint encoding. Thus, in Φ(π,X0,Xu, ), only the ReLU constraints and possibly the input-output conditions are not linear. Depending on the form of X0 and Xu and on how we encode the ReLU constraints, we may solve the system Φ(π,X0,Xu, ) in several ways:
1. MILP. It is shown in [31, 12, 43] that the ReLU relation between two real variables can be encoded via mixed-integer linear constraints (MILP) by introducing 0/1-integer variables to encode whether a given neuron is active or inactive. Hence, if X0 and Xu are given by linear constraints, we may solve Φ(π,X0,Xu, ) by a MILP solver. The ReLU encoding requires that each neuron value is bounded, which is ensured if X0 is a bounded set and if <∞. 2. Reluplex. In order to allow unbounded X0 and = ∞, we may use algorithms based on the Reluplex calculus [26, 27] to solve Φ(π,X0,Xu, ). 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 MILP-solving. 3. NRA-SMT. Alternatively, if X0 or Xu are given by non-linear constraints we may solve them by using an NRA-SMT-solver (non-linear real arithmetic satisfiability modulo theory), e.g. dReal [16]. To use an NRA-SMT-solver, we can replace the integer 0/1-variables of the ReLU neuron relations encoding with real variables that satisfy the constraint x(x− 1) = 0. 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 1, once the safety of NNs in {πw,b | (w,b) ∈ 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.

heading: 4.2 Safe weight sets for closed-loop systems with BNN Policies
text: Now consider a closed-loop system with a dynamics function f : X × U → X with X ⊆ Rm and U ⊆ Rn, a BNN policy π, an initial state set X0 ⊆ X and an unsafe state set Xu ⊆ X . Fix ∈ [0,∞]. In order to solve Problem 2 and verify safety of each trajectory contained in Trajf,π , our method searches for a positive invariant-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 to 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 Trajf,π . To that end, we define W π -safe positive invariants. Intuitively, a Wπ -safe 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 1 (Wπ -safe positive invariants). A set Inv ⊆ X is said to be a Wπ -positive invariant if X0 ⊆ Inv, for each x ∈ Inv and (w,b) ∈Wπ we have that f(x, πw,b(x)) ∈ Inv, and Inv ∩Xu = ∅.
Theorem 2 shows that Wπ -safe positive invariants can be used to verify safety of all trajectories in Trajf,π in Problem 2. The proof is straightforward and is deferred to the Supplementary Material.
Theorem 2. If there exists a Wπ -safe positive invariant, then each trajectory in Traj f,π is safe.
Algorithm 1 Learning algorithm for Wπ -safe positive invariants
Input Dynamics function f , BNN policy π, Initial state set X0, Unsafe state set Xu, ∈ [0,∞] X̃0, X̃u ← random samples of X0,Xu Dspec ← X̃u × {0} ∪ X̃0 × {1}, Dce ← {} Optional (bootstrapping): Sbootstrap ← sample finite trajectories with initial state sampled from X
Dspec ← Dspec ∪ {(x, 0)| ∃s ∈ Sbootstrap that starts in x ∈ X and reaches Xu} ∪ {(x, 1)| ∃s ∈ Sbootstrap that starts in x ∈ X and does not reach Xu}
Pre-train neural network gInv on datasets Dspec and Dce with loss function L while timeout not reached do
if ∃(x,x′,u,w,b) s.t. gInv(x) ≥ 0, gInv(x′) < 0, (w,b) ∈ Wπ , u = πw,b(x), x′ = f(x,u) then Dce ← Dce ∪ {(x,x′)} else if ∃(x) s.t. x ∈ X0, gInv(x) < 0 then Dspec ← Dspec ∪ {(x, 1)} else if ∃(x) s.t. x ∈ Xu, gInv(x) ≥ 0 then Dspec ← Dspec ∪ {(x, 0)} else Return Safe end if Train neural network gInv on datasets Dspec and Dce with loss function L
end while Return Unsafe
Learning positive invariants We now present a learning algorithm for a Wπ -safe positive invariant. It learns a neural network gInv : Rm → R, where the positive invariant is then defined as the set Inv = {x ∈ X | gInv(x) ≥ 0}. The pseudocode is given in Algorithm 1.
The algorithm first samples X̃0 from X0 and X̃u from Xu and initializes the specification set Dspec to X̃u×{0} ∪ X̃0×{1} and the counterexample set Dce to an empty set. Optionally, the algorithm also bootstraps the positive invariant network by initializing Dspec 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 a loop: the learner and the verifier. In each loop iteration, the learner first learns a Wπ -safe positive invariant candidate which takes the form of a neural network gInv. This is done by minimizing the loss function L that depends on Dspec and Dce:
L(gInv) = 1 |Dspec| ∑ (x,y)∈Dspec Lcls ( gInv(x), y ) + λ 1 |Dce| ∑ (x,x′)∈Dce Lce ( gInv(x), gInv(x′) ) , (1)
where λ is a tuning parameter and Lcls a binary classification loss function, e.g. the 0/1-loss L0/1(z, y) = 1[1[z ≥ 0] 6= y] or the logistic loss Llog(z, y) = z − z · y + log(1 + exp(−z)) as its differentiable alternative. The term Lce is the counterexample loss which we define via
Lce(z, z′) = 1 [ z > 0 ] 1 [ z′ < 0 ] Lcls ( z, 0 ) Lcls ( z′, 1 ) . (2)
Intuitively, the first sum in eq. (1) forces gInv to be nonnegative at initial states and negative at unsafe states contained in Dspec, and the second term forces each counterexample in Dce not to destroy the closedness of Inv under the system dynamics.
Once gInv is learned, the verifier checks whether Inv is indeed a Wπ -safe positive invariant. To do this, the verifier needs to check the three defining properties of Wπ -safe positive invariants:
1. Closedness of Inv under system dynamics. The verifier checks if there exist states x ∈ Inv, x′ 6∈ Inv and a BNN weight vector (w,b) ∈Wπ such that f(x, πw,b(x)) = x′. To do this, it introduces real variables x,x′ ∈ Rm, u ∈ Rn and y, y′ ∈ R, and solves:
maximize y − y′ subject to y ≥ 0, y′ < 0, y = gInv(x), y′ = gInv(x′) x′ = f(x,u)
u is an output of π on input x and weights (w,b) ∈Wπ
The conditions y = gInv(x) and y′ = gInv(x′) are encoded by using the existing techniques for encoding deterministic NNs as systems of MILP/Reluplex/NRA-SMT constraints. The 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 objective 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]. If a counterexample (x,x′) is found, it is added to Dce and the learner tries to learn a new candidate. If the system of constraints is unsatisfiable, the verifier proceeds to the second check. 2. Non-negativity on X0. The verifier checks if there exists x ∈ X0 for which gInv(x) < 0. If such x is found, (x, 1) is added to Dspec and the learner then tries to learn a new candidate. If the system of constraints is unsatisfiable, the verifier proceeds to the third check. 3. Negativity on Xu. The verifier checks if there exists x ∈ Xu with gInv(x) ≥ 0. If such x is found, (x, 0) is added to Dspec and the learner then tries to learn a new candidate. If the system of constraints is unsatisfiable, the veririfer concludes that Inv is a Wπ -positive invariant which does not contain any unsafe state and so each trajectory in Trajf,π is safe.
Theorem 3 shows that neural networks f Inv for which Inv is a Wπ -safe positive invariants are global minimizers of the loss function L with the 0/1-classification loss. Theorem 4 establishes the correctness of our algorithm. Proofs can be found in the Supplementary Material. Theorem 3. The loss function L is nonnegative for any neural network g, i.e. L(g) ≥ 0. Moreover, if Inv is a Wπ -safe positive invariant and Lcls the 0/1-loss, then L(gInv) = 0. Hence, neural networks gInv for which Inv is a Wπ -safe positive invariant are global minimizers of the loss function L when Lcls is the 0/1-loss. Theorem 4. If the verifier in Algorithm 1 shows that constraints in three checks are unsatisfiable, then the computed Inv is indeed a Wπ -safe positive invariant. Hence, Algorithm 1 is 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.

heading: 4.3 Computation of safe weight sets and the value of
text: Problems 1 and 2 assume a given value of for which safety needs to be verified. In order to compute the largest value of for which our approach can verify safety, we start with a small value of and iteratively increase it until we reach a value that cannot be certified or until the timeout is reached, in order to compute as large safe weight set as possible. In each iteration, our Algorithm 1 does not start from scratch but is initialized with the gInv and Dspec 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.

heading: 4.4 Safe exploration reinforcement learning
text: Given a safe but non-optimal initial policy π0, safe exploration reinforcement learning (SERL) concerns the problem of improving the expected return of π0 while ensuring safety when collecting samples of the environment [44, 1, 35]. Our method from Section 4.2 for 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.

heading: 5 Experiments
text: We perform an 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 1 and measure their effects on the obtained
(a) Vector field of the system when controlled by the posterior’s mean. Green/red arrows indicate empirical safe/unsafe estimates. (b) First guess of gInv. Green area shows gInv > 0, orange area gInv < 0. Red markers show the found counterexample. (c) Final gInv proving the safety of the system. Previous counterexamples marked in red.
Figure 2: Invariant learning shown on the inverted pendulum benchmark.
safety bounds and the algorithm’s runtime. First, we run the algorithm without any re-training on the counterexamples. In the second step, we run Algorithm 1 by initializing Dspec with samples from X0 and Xu only. Finally, we bootstrap the positive invariant network by initializing Dspec with random samples from the state space labeled with Monte-Carlo estimates of reaching the unsafe states. We consider environments with a 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 [20]. Details on our evaluation are in the Supplementary Material. Code is publicly available 2.
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-ablation pair, one with Bayesian weights from the second layer on (with N (0, 0.1) prior) and one with Bayesian weights in all layers (withN (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.
Our first benchmark represents an unstable linear dynamical system of the form xt+1 = Axt +But. A BNN policy stabilizes the system towards the point (0, 0). Consequently, the set of unsafe states is defined as {x ∈ R2 | |x|∞ ≥ 1.2}, and the initial states as {x ∈ R2 | |x|∞ ≤ 0.6}. Our second benchmark is the inverted pendulum task, which is a classical non-linear control problem. The two state variables a and b represent the angle and angular velocity of a pendulum that must be controlled in an upward direction. The actions produced by the policy correspond to a torque applied to the anchor point. Our benchmark concerns a variant of the original problem where the non-linearity in f is expressed by piecewise linear functions. The resulting system, even with a trained policy, is 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 set 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.
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 to 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 1 shows the results of our evaluation. Our results demonstrate that re-training with the counterexamples is the key component that determines our algorithm’s success. In all cases, except for the linear dynamical system, the initial guess of the invariant candidate violates the invariant
2https://github.com/mlech26l/bayesian_nn_safety
condition. Moreover, boostrapping Dspec with random points labeled by empirical estimates of reaching the unsafe states improves the search process significantly.

heading: 6 Conclusion
text: In this work we 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 as 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 a 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 a 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 to 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 to design an approach for refuting a weight set as unsafe which would complement our method, or to consider closed-loop systems with stochastic environment dynamics.
Any verification method for neural networks, even more so for neural networks in feedback loops, suffers from scalability limitations due to the underlying complexity class [26, 24]. Promising research 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 AI safety is to ensure that systems do not behave in undesirable ways and that safety violating events are avoided, we are not aware of any potential negative societal impacts.

heading: Acknowledgments
text: This research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award), ERC CoG 863818 (FoRM-SMArt), and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.

Review summaries:
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. 

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.  The 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.  The 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.

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.