Page 21 - Read Online

Page 2 of 22 Ernest et al. Complex Eng Syst 2023;3:4 I http://dx.doi.org/10.20517/ces.2022.54

1. INTRODUCTION
Artificial intelligence (AI) applications in reinforcement learning (RL) have garnered significant attention in
recent years [1,2] due to their wide ranging applicability to previously intractable problems. In particular, the
success of DeepMind’s AlphaGo system [3] ignited a revitalization of research and attention in the area, specif-
ically with the introduction of new techniques combining RL with deep neural networks (DNN), known as
Deep Reinforcement Learning (DRL). However, while improvements within the overarching field of RL and
DRL continue to increase the scalability and performance of these approaches, verification and explainability
efforts have not received comparable attention. There have been efforts to take highly performant DRL so-
lutions and increase explainability and trustworthiness ex post facto. An example of this was DARPA’s XAI
[4]
program, introduced to study and identify the importance and usage of explainability in AI . Their conclu-
sions were that many DRL solutions were brittle, unverifiable, and opaque to human designers/operators that
may want to audit, verify, or extract knowledge from what the agent learned.

Fuzzy inference systems (FIS), function approximators that utilize Fuzzy Logic and inference rules to map
[5]
inputs to outputs , have several properties that lend themselves towards XAI, but have other potential draw-
backs compared to DNNs, namely scalability. Fuzzy Logic-based systems have long been used in control
[6]
system development due to their approximation capabilities , ease of implementation from expert knowl-
[7]
[9]
[8]
edge , robustness to input noise , explainability and transparency to humans , and ability to be formally
verified [10] . However, scalability issues with respect to the number of inputs limited the potential applications.
Fuzzy trees were introduced in 2015 [11] in order to mitigate scalability issues while also retaining explainability
and approximation capabilities by combining multiple FISs arranged in a network or tree-like structure.
Genetic Algorithms are a class of gradient-free search algorithms that evolve solutions by mutation and re-
combination over a number of generations by evaluating their fitness against one or more metrics in a fitness
function. GAs have long been used to great effect in many areas, but also in a large body of work related to
optimization of FIS parameters [12] . Combining Fuzzy Trees with Genetic Algorithms led to Genetic Fuzzy
Trees (GFTs) [11] , a powerful combination that uses an explainable and formally verifiable function approxima-
tor with a gradient-free optimizer and has been applied to several complex use cases in both supervised [13]
and reinforcement learning domains [14] . Thales’s GFT software toolkit includes both a Fuzzy Logic engine,
Psion, and a state-of-the-art Genetic Algorithm-based optimization tool, EVE [15] . Its strengths include ease
of utilization for finding low wall-time solutions and wide applicability due to the nature of gradient-free op-
timization. Perhaps the most notable prior use-case was the Alpha system [14] , a super-human AI for beyond
visual range air-to-air engagements within high-fidelity simulations against expert human pilots [14] .

Another benefit of GFTs is that they can be verified using Formal Methods. Formal Methods are often defined
as ”mathematically rigorous techniques for the development, specification, and verification of systems.” Many
methods and techniques fall under the umbrella of Formal Methods including the boolean satisfiability prob-
lem (SAT) [16] , satisfiability modulo theories (SMT), model checking, theorem proving, reachability analysis,
etc. Formal Verification is the utilization of Formal Methods towards verifying the correctness of a system.
In general, verification is about confidence in the correctness of a system, and formal verification extends
traditional verification methods (e.g., Monte Carlo evaluation) towards definitive proofs of correctness. The
adoption of formal verification has been slow in the world of AI and ML mainly due to the difficulty in proving
properties of DNNs as their scale continues to increase.

In this work, an AI agent using the GFT construct is created and then trained using reinforcement learning
to play specific scenarios within StarCraft 2. Note that this study does not analyze an entire standard Starcraft
2 match. Instead, the focus will be on specific control applications with a focus on explainability and formal
verifiability, though an entire standard game of Starcraft 2 could certainly be studied through utilization of the
GFT approach. This study is not aimed towards demonstrating a performance disparity between Fuzzy logic-