论文标题
ACAS XU的神经网络压缩早期原型不安全：通过量化状态偏置性验证
Neural Network Compression of ACAS Xu Early Prototype is Unsafe: Closed-Loop Verification through Quantized State Backreachability
论文作者
论文摘要
ACAS XU是一种为无人飞机设计的空对空碰撞系统，该系统发行了水平转弯咨询，以避免侵入飞机。由于在设计中使用了大型查找表，因此提出了该策略的神经网络压缩。该系统的分析刺激了关于神经网络验证的形式方法社区中的大量研究。尽管已经开发出许多强大的方法，但大多数工作都集中在网络的开环特性上，而不是系统的要点 - 避免碰撞 - 需要闭环分析。 在这项工作中，我们开发了一种使用状态量化和逆转性来验证系统闭环近似的技术。我们使用有利的假设进行分析 - 完美的传感器信息，即时关注咨询，理想的飞机操纵以及仅直飞的入侵者。当该方法无法证明该系统是安全的时，我们会完善量化参数，直到生成原始（非量化）系统也有碰撞的反例之前。
ACAS Xu is an air-to-air collision avoidance system designed for unmanned aircraft that issues horizontal turn advisories to avoid an intruder aircraft. Due the use of a large lookup table in the design, a neural network compression of the policy was proposed. Analysis of this system has spurred a significant body of research in the formal methods community on neural network verification. While many powerful methods have been developed, most work focuses on open-loop properties of the networks, rather than the main point of the system -- collision avoidance -- which requires closed-loop analysis. In this work, we develop a technique to verify a closed-loop approximation of the system using state quantization and backreachability. We use favorable assumptions for the analysis -- perfect sensor information, instant following of advisories, ideal aircraft maneuvers and an intruder that only flies straight. When the method fails to prove the system is safe, we refine the quantization parameters until generating counterexamples where the original (non-quantized) system also has collisions.
