Probabilistic Reach-Avoid for Bayesian Neural Networks

TL;DR

This paper presents a method to compute safety guarantees and synthesize optimal control policies for Bayesian neural network models in stochastic environments, enhancing safety certification in model-based reinforcement learning.

Contribution

It introduces a novel approach combining interval propagation and backward recursion to compute lower bounds on reach-avoid probabilities and synthesizes policies maximizing these bounds.

Findings

Over four-fold increase in certifiable states on benchmarks.

More than three-fold increase in guaranteed reach-avoid probability.

Effective safety certification for BNN-based control policies.

Abstract

Model-based reinforcement learning seeks to simultaneously learn the dynamics of an unknown stochastic environment and synthesise an optimal policy for acting in it. Ensuring the safety and robustness of sequential decisions made through a policy in such an environment is a key challenge for policies intended for safety-critical scenarios. In this work, we investigate two complementary problems: first, computing reach-avoid probabilities for iterative predictions made with dynamical models, with dynamics described by Bayesian neural network (BNN); second, synthesising control policies that are optimal with respect to a given reach-avoid specification (reaching a "target" state, while avoiding a set of "unsafe" states) and a learned BNN model. Our solution leverages interval propagation and backward recursion techniques to compute lower bounds for the probability that a policy's sequence of actions leads to satisfying the reach-avoid specification. Such computed lower bounds provide safety certification for the given policy and BNN model. We then introduce control synthesis algorithms to derive policies maximizing said lower bounds on the safety probability. We demonstrate the effectiveness of our method on a series of control benchmarks characterized by learned BNN dynamics models. On our most challenging benchmark, compared to purely data-driven policies the optimal synthesis algorithm is able to provide more than a four-fold increase in the number of certifiable states and more than a three-fold increase in the average guaranteed reach-avoid probability.