战略战斗游戏中基于模糊XAI的形式化验证

由于涉及人类对人工智能的信任、正确性、审计、知识转移和监管等原因，可解释人工智能目前是该领域的前沿课题。利用强化学习（RL）开发的人工智能尤其引人关注，因为从环境中学到的东西并不透明。强化学习人工智能系统已被证明是 "脆性"的，无法在安全的条件下运行，因此，无论输入值如何，显示正确性的方法都是人们关注的焦点。显示正确性的一种方法是使用形式化方法（即形式化验证）验证系统。这些方法很有价值，但成本高昂且难以实现，因此大多数人倾向于采用其他方法进行验证，这些方法可能不那么严格，但更容易实现。在这项工作中，我们展示了针对战略战斗游戏《星际争霸 2》的各方面开发 RL 人工智能系统的方法，该系统性能良好、可解释并可进行形式验证。该系统在示例场景中表现出色，同时还能向人类操作员或设计者解释其行为。此外，该系统还符合有关其行为的正式安全规范。

引言

近年来，强化学习（RL）中的人工智能（AI）应用因其对以往棘手问题的广泛适用性而备受关注[1,2]。其中，DeepMind 的 AlphaGo 系统[3] 的成功点燃了该领域研究和关注的热情，特别是引入了将 RL 与深度神经网络 (DNN) 相结合的新技术，即深度强化学习 (DRL)。然而，尽管在 RL 和 DRL 的总体领域内取得的进步不断提高了这些方法的可扩展性和性能，但验证和可解释性工作却没有得到同等的关注。人们一直在努力采用性能卓越的 DRL 解决方案，并在事后提高可解释性和可信度。这方面的一个例子是 DARPA 的 XAI 计划，该计划旨在研究和确定人工智能中可解释性的重要性和使用情况[4]。他们得出的结论是，许多 DRL 解决方案都很脆弱、无法验证，而且对人类设计者/操作者来说也不透明，而人类设计者/操作者可能想要审核、验证或从智能体学到的知识中提取知识。

模糊推理系统（FIS）是一种利用模糊逻辑和推理规则将输入映射到输出的函数近似器[5]，它具有一些适合 XAI 的特性，但与 DNN 相比还有其他潜在的缺点，即可扩展性。基于模糊逻辑的系统因其近似能力[6]、易于利用专家知识实现[7]、对输入噪声的鲁棒性[8]、对人类的可解释性和透明度[9]以及可正式验证的能力[10]，长期以来一直被用于控制系统开发。然而，与输入数量相关的可扩展性问题限制了其潜在应用。为了缓解可扩展性问题，同时保留可解释性和近似能力，2015 年提出了模糊树[11]，将多个 FIS 组合成网络或树状结构。

遗传算法是一类无梯度搜索算法，它通过变异和重组在若干代内进化解决方案，并根据适应度函数中的一个或多个指标评估其适应度。长期以来，GA 在许多领域都发挥了巨大作用，在与 FIS 参数优化相关的大量工作中也是如此[12]。将模糊树与遗传算法相结合，产生了遗传模糊树（GFTs）[11]，这是一种强大的组合，使用了一种可解释、可正式验证的函数近似器和无梯度优化器，并已应用于监督[13]和强化学习领域[14]的多个复杂案例。Thales 的 GFT 软件工具包包括一个模糊逻辑引擎 Psion 和一个最先进的基于遗传算法的优化工具 EVE[15] 。它的优势在于易于使用，可以找到壁时间较短的解决方案，而且由于无梯度优化的特性，适用范围很广。阿尔法系统[14]可能是之前最著名的应用案例，它是一种超人类人工智能，可在高保真模拟中与人类飞行员专家进行超视距空对空交战[14]。

GFT 的另一个优点是可以使用形式化方法进行验证。形式化方法通常被定义为 "用于系统开发、规范和验证的数学上严格的技术"。许多方法和技术都属于形式方法的范畴，包括布尔可满足性问题（SAT）[16]、可满足性模态理论（SMT）、模型检查、定理证明、可达性分析等。形式化验证是利用形式化方法来验证系统的正确性。一般来说，验证涉及对系统正确性的信心，而形式验证则将传统验证方法（如蒙特卡洛评估）扩展到正确性的最终证明。在人工智能和人工智能领域，形式验证的应用一直进展缓慢，这主要是由于随着 DNN 规模的不断扩大，证明 DNN 属性的难度也在不断增加。

在这项工作中，我们创建了一个使用 GFT 结构的智能体，然后使用强化学习对其进行训练，使其能够游玩《星际争霸 2》中的特定场景。请注意，本研究并不分析整场标准的《星际争霸 2》比赛。相反，本研究的重点将放在具体的控制应用上，同时关注可解释性和形式可验证性，当然也可以通过使用 GFT 方法来研究整个标准的《星际争霸 2》游戏。这项研究的目的并不是要证明基于模糊逻辑的人工智能方法与其他任何方法之间的性能差距，而是要证明如何以保持可解释性和形式可验证性的方式创建这些系统。这些能力是任务/安全关键型应用非常需要的，而且往往是必需的。之所以使用星际争霸 2，是因为它是现代 RL 研究中常用的环境，允许创建可公开共享的任务/安全关键用例，并允许扩展这项工作，以便与其他高性能 RL 方法进行比较。

GFT 采用结构初始化，在适当情况下给定初始参数值，然后通过游戏中的互动在训练集中进行训练。GFT 的结构可以通过提取激活的规则和成员函数来解释输出动作。然后创建系统行为规范，并使用形式化方法[17] 对系统进行验证。在违反规范的情况下，会返回反例，显示违反规范的地方，然后进行修正。然后对修正后的系统进行验证，以确保其不违反规范，从而显示出所制定的行为规范的明确正确性。

本研究开发了四种规范，这绝不是一个详尽的潜在集合。这项工作将展示学习能力，以解决一类特别困难的问题，展示潜在的可解释性可能性，并证明遵守了一系列相关规范。本研究的主要目的是展示一个基于模糊逻辑的人工智能系统实例，该系统可以在任务/安全关键场景中正式验证是否符合安全规范。

本文其余部分的结构如下。第 2 节详细介绍了针对 SC2 中的特定场景创建、训练和验证 GFT 的方法。第 3 节展示了结果，包括 RL 训练、根据规范（和生成的反例）进行的验证，以及为确保符合规范而进行修改后的结果。第 4 节深入讨论了这些结果，并就扩展和未来工作提出了想法。最后，第 5 节简要总结了本研究的工作、结果和影响。