Probabilistic Reach-Avoid for Bayesian Neural Networks
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.
Code (1)
Tasks
Model-based Reinforcement LearningSimilar Papers 제목 키워드 기반
Stochastic Minimum-Cost Reach-Avoid Reinforcement Learning
We study stochastic minimum-cost reach-avoid reinforcement learning, where an agent must satisfy a reach-avoid specification with probability at least $p$ while minimizing expected cumulative costs in stochastic environm…
Reinforcement LearningSampling-based Approximations with Quantitative Performance for the Probabilistic Reach-Avoid Problem over General Markov Processes
This article deals with stochastic processes endowed with the Markov (memoryless) property and evolving over general (uncountable) state spaces. The models further depend on a non-deterministic quantity in the form of a …
Probabilistic Reachability and Invariance Computation of Stochastic Systems using Linear Programming
We consider the safety evaluation of discrete time, stochastic systems over a finite horizon. Therefore, we discuss and link probabilistic invariance with reachability as well as reach-avoid problems. We show how to effi…
Probabilistic Reach-Avoid Reachability in Nondeterministic Systems with Time-VaryingTargets and Obstacles
The probabilistic reachability problems of nondeterministic systems are studied. Based on the existing studies, the definition of probabilistic reachable sets is generalized by taking into account time-varying target set…
Bayesian Inference by Symbolic Model Checking
This paper applies probabilistic model checking techniques for discrete Markov chains to inference in Bayesian networks. We present a simple translation from Bayesian networks into tree-like Markov chains such that infer…
Bayesian InferencemodelTranslation