LyZNet: A Lightweight Python Tool for Learning and Verifying Neural Lyapunov Functions and Regions of Attraction

本文介绍了一个轻量级的Python框架LyZNet，用于神经李雅普诺夫函数的综合学习和验证，以进行稳定性分析。该工具使用基于物理的神经网络（PINN）学习神经李雅普诺夫函数，以解决Zubov方程，并使用可满足性模理论（SMT）求解器进行验证。该工具与文献中其他工具的不同之处在于，它能够提供接近吸引域的验证区域。这是通过将Zubov的偏微分方程（PDE）编码到PINN方法中实现的。通过接受底层优化问题的非凸性质，我们证明了在凸优化（如半定编程）无法捕捉吸引域的情况下，我们的神经网络框架更加成功。该工具还提供了将耦合非线性系统分解为低维子系统网络以进行组合验证的自动化功能。我们使用几个数值示例说明了该工具的使用和有效性，包括非平凡的低维非线性系统和高维系统。该工具的存储库可以在https://git.uwaterloo.ca/hybrid-systems-lab/lyznet找到。

LyZNet的目标是提供一种轻量级Python框架，用于整合神经李雅普诺夫函数的学习和验证，以进行稳定性分析。

LyZNet使用物理信息神经网络（PINN）来解决Zubov方程并进行验证，以提供接近吸引域的验证区域。

该工具具有自动分解耦合非线性系统的功能，以进行组合验证。LyZNet通过将Zubov的偏微分方程（PDE）编码到PINN方法中来实现此功能。该工具还可以在低维子系统网络中对非平凡低维非线性系统和高维系统进行验证。该工具的存储库可以在https://git.uwaterloo.ca/hybrid-systems-lab/lyznet中找到。

最近在这个领域中，还有一些相关研究，例如“Deep Lyapunov Neural Networks”和“Verification of Nonlinear Hybrid Systems via Barrier Certificates”。