NNLander-VeriF：一种用于基于视觉的自主飞机着陆的神经网络形式化验证框架

本文考虑对基于神经网络（NN）的自主着陆系统进行形式化验证的问题。在此类系统中，NN 控制器处理来自摄像机的图像以在飞机接近跑道时对其进行引导。基于视觉的闭环系统的安全性与活性验证面临的一个核心挑战是，缺乏能够刻画系统状态（如飞机位置）与基于视觉的 NN 控制器所处理图像之间关系的数学模型。另一挑战是最先进 NN 模型检测器的能力有限。此类模型检测器仅能推理神经网络的简单输入输出鲁棒性性质。该局限在 NN 模型检测器能力与下述需求之间造成了鸿沟：在考虑飞机动力学、感知组件与 NN 控制器的情况下验证闭环系统。为此，本文提出 NNLander-VeriF，一个用于验证基于视觉的自主着陆 NN 控制器的框架。NNLander-VeriF 通过利用透视摄像机的几何模型获得一个捕捉飞机状态与 NN 控制器输入之间关系的数学模型，从而应对上述挑战。通过将此模型转换为一个 NN（带手动指定权重）并与 NN 控制器组合，可用一个增广 NN 捕捉飞机状态与控制动作之间的关系。这样的增广 NN 模型可将闭环验证自然编码为若干 NN 鲁棒性查询，而最先进的 NN 模型检测器可处理这些查询。最后，我们评估了所提框架以形式化验证一个已训练 NN 的性质，并展示了其效率。