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