ACAS Xu早期原型神经网络压缩不安全：基于量化状态反向可达性的闭环验证
数值分析
2022-06-28 v3 人工智能
计算机科学中的逻辑
数值分析
摘要
ACAS Xu是一种为无人机设计的空对空碰撞避免系统，通过发出水平转弯建议以避开入侵飞机。由于设计中使用了大型查找表，有人提出了该策略的神经网络压缩方案。对该系统的分析在形式化方法学界激发了大量关于神经网络验证的研究。尽管已开发出许多强大的方法，但大多数工作关注网络的开环性质，而非系统的核心目标——碰撞避免——这需要闭环分析。在本工作中，我们开发了一种利用状态量化和反向可达性来验证系统闭环近似的技术。我们采用有利于分析的理想假设——完美的传感器信息、对建议的即时遵从、理想的飞机机动以及仅直线飞行的入侵者。当该方法无法证明系统安全时，我们细化量化参数，直至生成原始（非量化）系统同样发生撞击的反例。
引用
@article{arxiv.2201.06626,
title = {Neural Network Compression of ACAS Xu Early Prototype is Unsafe: Closed-Loop Verification through Quantized State Backreachability},
author = {Stanley Bak and Hoang-Dung Tran},
journal= {arXiv preprint arXiv:2201.06626},
year = {2022}
}