Infinite Time Horizon Safety of Bayesian Neural Networks
Mathias Lechner,u0110oru0111e u017dikeliu0107,Krishnendu Chatterjee,Thomas Henzinger
Bayesian neural networks (BNNs) place distributions over the weights of a neural network to model uncertainty in the data and the networks 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 posteriors support. Our method first computes a safe weight set and then alters the BNNs 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.
