面向动力学模型的神经障碍证书的自动化与形式化综合
系统与控制
2020-10-20 v2 机器学习
计算机科学中的逻辑
系统与控制
摘要
我们引入一种基于反例的自动化、形式化方法来综合障碍证书（BC），用于连续与混合动力学模型的安全性验证。该方法由一个归纳框架支撑：其结构为学习者与可靠验证器之间的顺序循环，其中学习者操纵以神经网络形式构造的候选 BC，验证器则要么证明候选的有效性，要么生成反例以进一步引导学习者。我们在多项式与非多项式动力学模型上将该方法与最先进技术进行比较：结果表明，我们综合可靠 BC 的速度最高快两个数量级，尤其验证引擎的加速极为显著（最高快五个数量级），同时学习部分所需数据集大幅减小（最高小三个数量级）。除超越现有最优水平外，我们进一步在混合动力学模型与更高维模型上挑战新方法的极限，并展示了我们算法与代码库的数值鲁棒性。
引用
@article{arxiv.2007.03251,
title = {Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models},
author = {Andrea Peruffo and Daniele Ahmed and Alessandro Abate},
journal= {arXiv preprint arXiv:2007.03251},
year = {2020}
}