Analytical Lyapunov Function Discovery: An RL-based Generative Approach

TL;DR

This paper introduces a novel reinforcement learning-based transformer framework for discovering local analytical Lyapunov functions in high-dimensional nonlinear systems, improving verification and interpretability.

Contribution

It presents a new end-to-end RL approach using transformers to generate and verify local Lyapunov functions, capable of handling high-dimensional and non-polynomial systems from scratch.

Findings

Successfully finds Lyapunov functions for systems up to ten dimensions.

Outperforms previous methods by handling high-dimensional, non-polynomial systems.

Provides more interpretable Lyapunov functions with easier verification.

Abstract

Despite advances in learning-based methods, finding valid Lyapunov functions for nonlinear dynamical systems remains challenging. Current neural network approaches face two main issues: challenges in scalable verification and limited interpretability. To address these, we propose an end-to-end framework using transformers to construct analytical Lyapunov functions (local), which simplifies formal verification, enhances interpretability, and provides valuable insights for control engineers. Our framework consists of a transformer-based trainer that generates candidate Lyapunov functions and a falsifier that verifies candidate expressions and refines the model via risk-seeking policy gradient. Unlike Alfarano et al. (2024), which utilizes pre-training and seeks global Lyapunov functions for low-dimensional systems, our model is trained from scratch via reinforcement learning (RL) and succeeds in finding local Lyapunov functions for high-dimensional and non-polynomial systems. Given the analytical nature of the candidates, we employ efficient optimization methods for falsification during training and formal verification tools for the final verification. We demonstrate the efficiency of our approach on a range of nonlinear dynamical systems with up to ten dimensions and show that it can discover Lyapunov functions not previously identified in the control literature. Full implementation is available on \href{https://github.com/JieFeng-cse/Analytical-Lyapunov-Function-Discovery}{Github}