李雅普诺夫神经网络的形式化综合
系统与控制
2021-02-09 v2 机器学习
计算机科学中的逻辑
系统与控制
摘要
我们提出一种自动且形式可靠的李雅普诺夫函数综合方法，用于自治非线性系统的渐近稳定性。传统方法或是解析的且需要人工投入，或是数值的但缺乏形式可靠性。介于两者之间的李雅普诺夫函数符号计算方法提供形式保证，但通常因依赖用户提供合适的函数模板而只是半自动的。我们提出一种完全自动——利用机器学习——寻找李雅普诺夫函数，同时利用可满足性模理论（SMT）提供形式保证的方法。我们采用反例引导方法，其中数值学习器与符号验证器交互以构造可证明正确的李雅普诺夫神经网络（LNNs）。学习器训练一个在样本集上满足渐近稳定性李雅普诺夫判据的神经网络；验证器通过 SMT 求解证明判据在整个域上满足，或将反例扩充至样本集。我们的方法支持具有多项式激活函数及多种深度与宽度的神经网络，展现出广泛的学习能力。我们在若干非平凡基准上演示了该方法，并与基于数值优化的方法、基于符号模板的方法以及同类基于 LNN 的方法进行了有利比较。我们的方法比替代方案更快地综合李雅普诺夫函数且覆盖更宽的空间域，同时提供更强或同等的保证。
引用
@article{arxiv.2003.08910,
title = {Formal Synthesis of Lyapunov Neural Networks},
author = {Alessandro Abate and Daniele Ahmed and Mirco Giacobbe and Andrea Peruffo},
journal= {arXiv preprint arXiv:2003.08910},
year = {2021}
}