Joint Differentiable Optimization and Verification for Certified Reinforcement Learning

TL;DR

This paper introduces a joint differentiable framework for reinforcement learning and formal verification, enabling the synthesis of controllers with safety guarantees in safety-critical systems.

Contribution

It proposes a novel bilevel optimization approach that integrates learning and verification, improving the certification process during controller training.

Findings

Outperforms SVG and PPO in safety and stability certification

Successfully synthesizes controllers with barrier and Lyapunov functions

Demonstrates effectiveness across various safety-critical examples

Abstract

In model-based reinforcement learning for safety-critical control systems, it is important to formally certify system properties (e.g., safety, stability) under the learned controller. However, as existing methods typically apply formal verification \emph{after} the controller has been learned, it is sometimes difficult to obtain any certificate, even after many iterations between learning and verification. To address this challenge, we propose a framework that jointly conducts reinforcement learning and formal verification by formulating and solving a novel bilevel optimization problem, which is differentiable by the gradients from the value function and certificates. Experiments on a variety of examples demonstrate the significant advantages of our framework over the model-based stochastic value gradient (SVG) method and the model-free proximal policy optimization (PPO) method in finding feasible controllers with barrier functions and Lyapunov functions that ensure system safety and stability.