通过安全区域线性近似验证飞机避撞神经网络
系统与控制
2019-03-05 v1 计算机科学中的逻辑
摘要
下一代飞机避撞系统将问题构建为马尔可夫决策过程，并使用动态规划来优化告警逻辑。所得系统使用大型查找表来根据给定给飞行员的建议，但这些表可能变得非常庞大。为使系统能在受限硬件上运行，先前工作研究了使用深度神经网络压缩该表。然而，确保神经网络可靠地发出安全建议对于认证至关重要。本工作定义了可安全提供各建议的线性化区域，使得神经网络验证工具 Reluplex 能够检查是否曾发出不安全建议。我们生成了一个概念性避撞策略并用于训练神经网络表示。对这些神经网络检查不安全建议，结果发现了数千个不安全反例。
引用
@article{arxiv.1903.00762,
title = {Verifying Aircraft Collision Avoidance Neural Networks Through Linear Approximations of Safe Regions},
author = {Kyle D. Julian and Shivam Sharma and Jean-Baptiste Jeannin and Mykel J. Kochenderfer},
journal= {arXiv preprint arXiv:1903.00762},
year = {2019}
}