Verified Safe Reinforcement Learning for Neural Network Dynamic Models

TL;DR

This paper presents a new method for training neural network controllers that are both high-performing and formally verified for safety over extended horizons in nonlinear dynamical systems.

Contribution

It introduces a curriculum learning scheme, incremental verification, and multiple controllers to improve verified safety in neural network control policies.

Findings

Controllers achieved safety over horizons much longer than previous methods.

High reward performance maintained alongside verified safety.

Demonstrated effectiveness on five diverse safe control problems.

Abstract

Learning reliably safe autonomous control is one of the core problems in trustworthy autonomy. However, training a controller that can be formally verified to be safe remains a major challenge. We introduce a novel approach for learning verified safe control policies in nonlinear neural dynamical systems while maximizing overall performance. Our approach aims to achieve safety in the sense of finite-horizon reachability proofs, and is comprised of three key parts. The first is a novel curriculum learning scheme that iteratively increases the verified safe horizon. The second leverages the iterative nature of gradient-based learning to leverage incremental verification, reusing information from prior verification runs. Finally, we learn multiple verified initial-state-dependent controllers, an idea that is especially valuable for more complex domains where learning a single universal verified safe controller is extremely challenging. Our experiments on five safe control problems demonstrate that our trained controllers can achieve verified safety over horizons that are as much as an order of magnitude longer than state-of-the-art baselines, while maintaining high reward, as well as a perfect safety record over entire episodes. Our code is available at https://github.com/jlwu002/VSRL.