神经网络控制的自主系统的形式化验证
人工智能
2018-11-01 v1 机器人学
系统与控制
摘要
本文考虑形式化验证配备神经网络（NN）控制器的自主机器人安全性问题，该控制器处理 LiDAR 图像以产生控制动作。给定由一组多面体障碍物刻画的工作空间，我们的目标是从这些初始条件出发的机器人轨迹保证避开障碍物，计算安全初始条件的集合。我们的方法是构造系统的有限状态抽象，并在该有限状态抽象上使用标准可达性分析来计算安全初始状态集合。计算有限状态抽象的第一个技术问题是数学建模将机器人位置映射到 LiDAR 图像的成像函数。为此，我们引入成像适应集的概念，作为工作空间的划分，其中成像函数保证为仿射的。我们开发了多项式时间算法将工作空间划分为成像适应集，并计算相应的仿射成像函数。给定该工作空间划分、机器人的离散时间线性动力学以及具有修正线性单元（ReLU）非线性的预训练 NN 控制器，第二个技术挑战是分析神经网络的行为。为此，我们利用可满足性模凸（SMC）编码来枚举不同 ReLU 的所有可能分段。SMC 求解器随后使用布尔可满足性求解器和凸规划求解器，将问题分解为更小的子问题。为加速该过程，我们开发了可快速剪枝可行 ReLU 分段空间的预处理算法。最后，我们使用神经网络控制器复杂度递增的数值仿真展示了所提算法的效率。
引用
@article{arxiv.1810.13072,
title = {Formal Verification of Neural Network Controlled Autonomous Systems},
author = {Xiaowu Sun and Haitham Khedr and Yasser Shoukry},
journal= {arXiv preprint arXiv:1810.13072},
year = {2018}
}