推荐！【F16模型：符号系统、模型提取、异常检测和形式化方法】《利用符号表示实现安全可靠学习》美空军2022最新107页技术报告

2022 年 11 月 3 日 专知

根据合同FA8750-19-C-0092制定本报告：利用符号表示进行安全和可靠的学习。这项研究工作的目标是开发新的工具、算法和方法，以提高自主的、可学习的网络物理系统（LE-CPSs）的安全性。这些系统由于更高的自主性以及网络组件和物理环境之间的相互作用而表现出一系列丰富的行为。这项工作总结了在符号系统测试、模型提取、异常检测、学习未知动力学和形式化方法方面的进展，以验证这些系统。这些工作被整合到控制系统分析框架中，并应用于高保真F16模型。

图1 可靠学习小组

报告总结

可靠自主性（AA）计划是由美国国防部高级研究计划局（DARPA）委托进行的，目的是推动持续可靠技术的发展，以跟上安全关键系统日益复杂和自主的步伐。该计划的目标是学习型（LE）网络物理系统（CPS）（LECPSs）；由于更高水平的自主性，以及网络组件和物理环境之间的互动，这些系统表现出丰富的行为集合。由于这些系统经常被部署在安全关键环境中，其故障可能导致金钱和人命的损失，因此其持续的保证是最重要的。

为了加速LE-CPS的采用，保证学习团队采用了一种多方面的方法，为保证几个层次的自主性提供解决方案，包括规范、设计、培训、设计时间测试和运行时间保证。图1所示的海报中总结了保证学习团队的方法。

1.1 可靠学习挑战问题

该团队将F-16飞行控制系统[75]确定为美国防部（DoD）可靠自主性计划的相关基准。这支持了该计划第二阶段挑战问题2.5 "避免地面碰撞 "和第三阶段挑战问题3.2 "避免空中碰撞"。我们开发了控制系统分析框架（CSAF），这是一个集成的工具链，以证明团队开发的技术和工具的有效性。我们使用DevOps风格的自动化来推动LE-CPS的持续集成和目标定向测试。最后，我们展示了运行时可靠（RTA）的可行性，以保护系统免受LECPS故障的影响。

1.2 控制系统分析框架

Galois开发了控制系统分析框架，这是一个用于建模、测试和正式验证LE-CPS的综合工具链。CSAF将最先进的分析工具引入数字工程框架，由DevOps风格的持续集成支持，以加速安全关键系统的数字设计。CSAF通过对学习型组件进行严格的自动测试来实现持续验证。图2说明了CSAF如何与现有的和新兴的工具相结合，在持续集成/持续部署（CI/CD）环境中提供自动化、目标定向测试、运行时间可靠验证。

图2 控制系统分析框架概述

2 引言

在过去的十年中，将机器学习技术应用于网络物理系统方面取得了巨大的进步，导致了支持学习的自主网络物理系统的发展；这些系统已经在空中、地面和深海环境中得到了初步的部署。机器学习使图像处理、决策和控制的强大和适应性方法成为可能。然而，由于这些系统的操作行为缺乏强有力的保证，以及许多训练方法需要大量的数据，这些系统的广泛采用和更广泛的接受受到了阻碍。

2.1 符号系统测试

这一工作的第一阶段探讨了如何将为传统软件系统开发的形式化验证和原则性测试技术重新用于验证、安全和改善学习型系统的训练时间。具体来说，我们将这些技术用于现实世界中复杂的异质系统（F-16模型），该系统由传统算法、自适应控制和学习型组件混合组成。我们的技术将相关领域的知识作为模型生成的一部分，在第二阶段我们进行了高覆盖率的系统级测试。这种方法为部署的机器学习模型的安全性提供了高度的保证，即使是在面对意外的环境干扰时。第一阶段的初步结果成功地证明了使用正式模型来有效地指导学习，改善训练时间，提高性能，并使数据得到更有效的利用。因此，我们预计这将大大扩展深度学习方法可以应用的系统组件的范围。

我们将上述对学习型系统的正式验证和测试与运行时保护方法的工作相结合，以确保学习型控制器（LEC）算法的正确性。我们利用先进的机器学习（ML）异常检测方法来评估LEC输出的质量。我们提供了替代的、确定性的程序，这些程序既可以用来引导LEC的不良行为，也可以提供适合形式化验证的LEC行为的替代抽象。最后，我们提供了利用我们的测试结果来提高我们重新训练的LEC的效率和稳健性的方法。

虽然通过学习来适应控制法则对实现更灵活的车辆系统很重要，但对动态变化的适应也同样重要，例如，由于部件的退化或平台的损坏。第一阶段推进了先前的工作，开发了新的系统动力学学习方法，利用基础系统物理学知识，提供更可靠和有效的结果。

2.2 可靠学习挑战问题

Galois在Aditya Zutshi博士的领导下，开始收集基准挑战问题，包括波音公司的TAXINET/X-Plane模拟器、汽车学习行动（CARLA），以及控制理论研究中使用的学术基准。F-16 AeroBench基准[76]的选择是为了使我们的工作与空域挑战问题集和正在进行的波音公司TAXINET/X-plane的感知工作相一致，使用基于感知的学习技术。第一阶段的高潮是将我们的工具和技术早期整合到一个模块化的学习型控制器测试线束中，使用F-16模型来演示F-16地面防撞系统（GCAS）机动的保证学习。作为第一阶段挑战问题2.5的一部分，我们成功演示了GCAS机动。

在第二阶段，团队继续开发控制系统分析框架和其他工具，重点是F-16空中防撞（ACA）挑战问题。在第二阶段，我们演示了单人和多人的F-16空中防撞，作为该计划挑战问题3.2的一部分。

2.3 CPS系统的训练、鲁棒性和形式验证的方法

普渡大学团队在Suresh Jagannathan博士和Ananth Grama博士的领导下，致力于保证学习型控制器的六个核心部分：

(i) 下一代高效的学习模型的训练程序。

(ii) 在强化学习（RL）控制器中使用新的训练程序。

(iii) 保证控制器性能和物理设备安全的正式方法。

(iv) 应用于CPS系统的稳健性技术。

(v) 控制器的可扩展验证；以及。

(vi) 新的规范形式和编译技术，用于高保证的多智能体自主系统。

2.4 OSU的异常检测调查

俄勒冈州立大学（OSU）团队在Tom Dietterich和Alan Fern博士的领导下，对跨越许多应用领域的两类数据的异常检测（AD）进行了调查。研究异常检测的动机是，保证机器学习系统的自主性必须能够检测到与训练系统相比，系统何时处于新的 "运行状态"。

第一个AD调查研究了深度图像分类的开放类别检测问题。这个问题涉及到开发一些方法，以确定一个经过训练的深度图像分类器在部署后遇到的输入图像，相对于训练数据中的类别而言，是否属于一个新类别。我们的工作重点是使用 "神谕技术 "来分析这个问题的深度表征和异常检测方法的互动。结果表明，改进的表征与基于这些表征的改进的异常检测信号相比，有相对的改进空间。

第二个AD调查研究了分布外动态（OODD）检测的问题。这个问题涉及到确定何时一个时间过程，例如一个部署的学习控制系统，正在经历与它被训练的动态不同的动态。这是一个在深度强化学习（DRL）文献中很少受到关注的问题，尽管它具有实际的重要性。我们的第一个贡献是设计和开发了第一套基于常用DRL领域的ODD基准和度量。我们的第二个贡献是设计、开发和评估了一个强大的基线OODD方法，它提供了非微不足道的性能，但也为基准留下了改进空间。这为OODD检测的未来进展奠定了基础。

2.5 实时学习系统动力学（物理感知学习）

由Ufuk Topcu博士领导的德克萨斯大学（UT）奥斯汀团队的工作重点是开发数据驱动的算法，用于在非常严重的数据限制下对未知动态系统进行可达性分析和控制。这项工作是由系统动态发生重大和意想不到的变化的情景所激发的。在保证学习计划中，这些工作被应用于F16模型被置于需要快速倾斜系统动力学的场景中，因为在操作条件、故障和极端的地面防撞场景中，传统方法无法提供保证。

2.6 学习程序性政策的强化学习方法

由Swarat Chaudhuri博士领导的UT Austin团队（最初在莱斯大学）开发了模仿-预测程序化强化学习（PROPEL），这是一种强化学习方法，用于学习可以用预定义符号语言表达的程序化策略（关于这项工作的论文《模仿-预测程序化强化学习》发表在2019年NeurIPS大会上）[48]。符号化策略是一个决策程序，例如 "如果（道路畅通）加速，否则减速"，可以想象它是由人类工程师编写。相对于传统的深度强化学习，其中学习的策略是不透明的神经网络，程序化的策略是可审计的，并简化了正式的正确性验证。这个政策学习问题是用镜像下降法解决的，该方法保持了一个神经和程序化政策的加法组合，使用归纳程序合成和基于梯度的优化的混合方法迭代更新这两个部分（更多内容见第3.5节）。该方法在一个模拟驾驶任务以及一系列经典控制任务上进行了评估。实证结果表明，该方法发现了人类可理解的策略，而没有明显影响性能。

该团队还开发了一种强化学习的方法，在探索过程中构建的每一个中间策略都得到了正式的验证，并在2020年的NeurIPS上展示了 "具有正式验证的探索的神经符号强化学习"（REVEL）。在算法上，REVEL学习神经策略，这些策略由确保每一个行动都是安全的盾牌来保护。该学习算法使用一种镜像下降的形式来迭代更新策略的防护罩和神经组件，同时保持安全，而不需要直接的神经网络验证。该方法在控制和机器人学的几个基准上进行了评估，这些基准类似于简化的自动驾驶应用。结果表明，REVEL可以在学习过程中保证最坏情况下的安全，而其他最先进的强化学习方法在学习过程中经常违反安全约束。

在项目的最后阶段，该团队探索了学习符号策略的机制，这些策略在被视为像素的场景中运作。在这里，一个神经网络被用来识别一个场景中有趣的实体。然后，这些实体被视为命名的变量，一个以这些变量为程序的程序被自动发现。