Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates

TL;DR

This paper introduces a novel method for training and verifying Neural Lyapunov Barrier certificates to ensure safety and goal achievement of deep reinforcement learning controllers in complex systems, with formal guarantees.

Contribution

It proposes a new technique for composing and filtering certificates, simplifying verification of complex systems, and integrates neural network verification engines for formal safety guarantees.

Findings

Successfully verified safety and liveness for a DRL-controlled spacecraft

Introduced certificate composition to simplify complex system verification

Enhanced certificate filtering to streamline the verification process

Abstract

Deep reinforcement learning (DRL) is a powerful machine learning paradigm for generating agents that control autonomous systems. However, the ``black box'' nature of DRL agents limits their deployment in real-world safety-critical applications. A promising approach for providing strong guarantees on an agent's behavior is to use Neural Lyapunov Barrier (NLB) certificates, which are learned functions over the system whose properties indirectly imply that an agent behaves as desired. However, NLB-based certificates are typically difficult to learn and even more difficult to verify, especially for complex systems. In this work, we present a novel method for training and verifying NLB-based certificates for discrete-time systems. Specifically, we introduce a technique for certificate composition, which simplifies the verification of highly-complex systems by strategically designing a sequence of certificates. When jointly verified with neural network verification engines, these certificates provide a formal guarantee that a DRL agent both achieves its goals and avoids unsafe behavior. Furthermore, we introduce a technique for certificate filtering, which significantly simplifies the process of producing formally verified certificates. We demonstrate the merits of our approach with a case study on providing safety and liveness guarantees for a DRL-controlled spacecraft.