As deep neural networks (DNNs) are becoming the prominent solution for many computational problems, the aviation industry seeks to explore their potential in alleviating pilot workload and in improving operational safety. However, the use of DNNs in this type of safety-critical applications requires a thorough certification process. This need can be addressed through formal verification, which provides rigorous assurances -- e.g.,~by proving the absence of certain mispredictions. In this case-study paper, we demonstrate this process using an image-classifier DNN currently under development at Airbus and intended for use during the aircraft taxiing phase. We use formal methods to assess this DNN's robustness to three common image perturbation types: noise, brightness and contrast, and some of their combinations. This process entails multiple invocations of the underlying verifier, which might be computationally expensive; and we therefore propose a method that leverages the monotonicity of these robustness properties, as well as the results of past verification queries, in order to reduce the overall number of verification queries required by nearly 60%. Our results provide an indication of the level of robustness achieved by the DNN classifier under study, and indicate that it is considerably more vulnerable to noise than to brightness or contrast perturbations.

翻译：随着深度神经网络（DNN）成为解决众多计算问题的主流方案，航空业正积极探索其在减轻飞行员工作负荷与提升运行安全方面的潜力。然而，在这类安全关键应用中使用DNN需要一个彻底的认证过程。这一需求可以通过形式化验证来满足，它能提供严格的保证——例如，通过证明不存在某些特定的误判。在这篇案例研究论文中，我们使用一个由空客公司正在开发、拟用于飞机滑行阶段的图像分类器DNN来演示这一过程。我们采用形式化方法评估该DNN对三种常见图像扰动类型（噪声、亮度与对比度）及其部分组合的鲁棒性。该过程涉及对底层验证器的多次调用，计算开销可能很大；因此，我们提出一种方法，利用这些鲁棒性属性的单调性以及过往验证查询的结果，将所需的验证查询总数减少近60%。我们的结果揭示了所研究DNN分类器达到的鲁棒性水平，并表明其对噪声扰动的脆弱性显著高于对亮度或对比度扰动的脆弱性。