Infinite Time Horizon Safety of Bayesian Neural Networks

TL;DR

This paper introduces a novel method for verifying the safety of Bayesian neural network policies over infinite time horizons by training a deterministic safety certificate network, enabling safe reinforcement learning and system guarantees.

Contribution

It proposes a deterministic safety certificate network for infinite horizon safety verification of BNNs, extending to safe exploration in reinforcement learning.

Findings

Successfully verifies safety over infinite horizons.

Effectively integrates safety certificates with BNNs.

Demonstrates applicability on various RL benchmarks.

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.