arXiv:2502.02014v1 类型: cross 摘要: 尽管在基于学习的方法上取得了进展，但为非线性动态系统找到有效的李雅普诺夫函数仍然具有挑战性。当前的神经网络方法面临两大主要问题：可扩展验证的挑战和有限的可解释性。为了解决这些问题，我们提出了一种端到端框架，使用变换器构建分析李雅普诺夫函数（局部），这简化了形式验证，增强了可解释性，并为控制工程师提供了有价值的见解。我们的框架由一个基于变换器的训练器组成，该训练器生成候选李雅普诺夫函数，以及一个验证器，通过风险寻求的策略梯度来验证候选表达式并优化模型。与Alfarano等人（2024）不同，后者利用了预训练并寻找低维系统中的全局李雅普诺夫函数，我们的模型通过强化学习（RL）从头开始训练，并成功地找到了高维和非多项式系统的局部李雅普诺夫函数。由于候选者的分析性质，我们在训练过程中采用了高效的优化方法进行矛盾验证，并最终使用形式验证工具进行验证。我们在具有多达十个维度的多种非线性动态系统中展示了我们方法的有效性，并证明它可以发现控制文献中未曾发现的李雅普诺夫函数。