Page 22 - Read Online

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

based AI approaches and any other methodology, but rather to demonstrate how these systems can be created
in a way that maintains explainability and formal verifiability. These capabilities are highly desired, and often
required,formission/safety-criticalapplications. Starcraft2isusedbecauseitisacommonlyusedenvironment
in modern RL research, it allows for creation of publicly-shareable mission/safety-critical use-cases, and allows
for extension of this work for comparisons with other highly performant RL methodologies.

The GFT is initialized with a structure, given initial parameter values where applicable, and then trained by
interaction in the game across a training set of episodes. The structure of the GFT is such that output actions
can be explained by extracting the activated rules and membership functions. Specifications about the sys-
tem’s behavior are then created and verified against the system using Formal Methods [17] . In cases where the
specifications are violated, counterexamples are returned showing where the violations occur, and then cor-
rections are performed. The corrected systems are then verified to not violate specifications showing definitive
correctness with respect to the developed behavioral specifications.

Four specifications have been developed for this study, which is by no means an exhaustive potential set. This
work will demonstrate the learning capability to solve a particularly difficult sort of engagement, demonstrate
the potential explainability possibilities, and prove adherence to a set of relevant specifications. The primary
objective for this study is to showcase an example of a fuzzy logic based AI system which can be formally
verified to adhere to safety specifications within a mission/safety-critical scenario.

The structure of the remainder of the paper is as follows. Section 2 details the methods used to create, train,
and verify a GFT for specific scenarios in SC2. Section 3 shows the results including RL training, verification
against specifications (and generated counterexamples), and results after modification to ensure specification
adherence. Section 4 discusses the results in depth and offers thoughts on extensions and future work. Finally,
Section 5 gives a concise conclusion on the work, results, and impact of this study.

2. METHODS
This section describes both the general background info and setup of a GFT solution for training in a RL
context followed by the specific implementation for the SC2 use case.

2.1. General GFT workflow
The typical workflow for creating a GFT AI solution involves creating a GFT-based agent with a tree structure
that is purposefully designed such that it is explainable and formally verifiable. The performance of the agent
is evaluated through a number of different scenarios for training, testing, and validation. The system is then
formally verified against specifications about its behavior. Explainability aspects are used both as an auditing
tool when evaluating counterexamples from the formal verification process, and also as a knowledge transfer
device to allow human observation and understanding of what the agent learned during the RL process.

GFTs are most often created using a combination of initial expert knowledge and machine learning using
gradient-free optimization. Thales’s GFT toolkit is a commercial software package that includes both a Fuzzy
Inference System (FIS) engine named Psion and a Genetic Algorithm optimization engine, EVE, which com-
bined represent the best software implementation of Genetic Fuzzy Trees available today [15] . An example of a
notional GFT structure is shown in Figure 1.

TheGFT is thentrainedusingEVEinwhatevercontexttheproblemisframed (supervised, reinforcment)until
termination criteria are met. These termination criteria can include performance metrics, time, number of
generations/epochs, stagnation measures, etc. Once this round of training is complete, verification can occur
on the GFT (fixed parameters) along with SME/developer auditing and manual changes. Counterexamples