用强化学习生成可解析的李雅普诺夫函数，解决高维非线性系统稳定性验证难题。
Analytical Lyapunov Function Discovery: An RL-based Generative Approach
- 基于Transformer的强化学习框架，从零训练生成局部解析李雅普诺夫函数。
- 在十维非多项式系统上成功发现文献未报道的新李雅普诺夫函数。
- 兼具可解释性与高效验证能力，适合控制工程与形式化验证研究者。
尽管基于学习的方法有所进展，为非线性动力系统寻找有效的李雅普诺夫函数仍具挑战性。现有神经网络方法面临可扩展验证困难和可解释性差的问题。为此，我们提出一个端到端框架，利用Transformer构建局部解析李雅普诺夫函数，简化形式化验证、提升可解释性，并为控制工程师提供重要洞见。该框架包含一个基于Transformer的训练器生成候选函数，以及一个验证器通过风险导向的策略梯度对模型进行迭代优化。与Alfarano等（2024）预训练并寻求低维系统全局李雅普诺夫函数不同，我们的模型从零开始通过强化学习训练，成功在高维及非多项式系统中发现局部李雅普诺夫函数。由于候选函数具有解析形式，训练中采用高效优化方法进行伪证，最终使用形式化验证工具完成确认。我们在多达十维的非线性动力系统上验证了方法的有效性，发现文献中尚未报道的李雅普诺夫函数。完整实现已开源于Github。
原文摘要 · Abstract (English)
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}
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。