  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.
