Page 20 - Read Online

Ernest et al. Complex Eng Syst 2023;3:4 Complex Engineering
DOI: 10.20517/ces.2022.54 Systems

Research Article Open Access

Formal verification of Fuzzy-based XAI for Strategic
Combat Game

Nicholas Ernest, Timothy Arnett, Zachariah Phillips
Thales Avionics Inc., Cincinnati, OH 45242, USA.

Correspondence to: Dr. Nicholas Ernest, Thales Avionics Inc., 4358 Glendale-Milford Rd., Cincinnati, OH 45242, USA. E-mail:
nick.ernest@us.thalesgroup.com
How to cite this article: Ernest N, Arnett T, Phillips Z. Formal verification of Fuzzy-based XAI for Strategic Combat Game. Complex
Eng Syst 2023;3:4. http://dx.doi.org/10.20517/ces.2022.54
Received: 11 Dec 2022 First Decision: 31 Jan 2023 Revised: 13 Mar 2023 Accepted: 14 Mar 2023 Published: 30 Mar 2023
Academic Editor: Hamid Reza Karimi Copy Editor: Yin Han Production Editor: Yin Han

Abstract
Explainable AI is a topic at the forefront of the field currently for reasons involving human trust in AI, correctness,
auditing, knowledge transfer, and regulation. AI that is developed with reinforcement learning (RL) is especially of
interest due to the non-transparency of what was learned from the environment. RL AI systems have been shown to
be ”brittle” with respect to the conditions it can safely operate in, and therefore ways to show correctness regardless
of input values are of key interest. One way to show correctness is to verify the system using Formal Methods, known
as Formal Verification. These methods are valuable, but costly and difficult to implement, leading most to instead
favor other methodologies for verification that may be less rigorous, but more easily implemented. In this work,
we show methods for development of an RL AI system for aspects of the strategic combat game Starcraft 2 that is
performant, explainable, and formally verifiable. The resulting system performs very well on example scenarios while
retaining explainability of its actions to a human operator or designer. In addition, it is shown to adhere to formal
safety specifications about its behavior.

Keywords: Explainable AI, reinforcement learning, formal verification, starcraft, genetic algorithm, fuzzy logic, ge-
netic fuzzy trees, formal methods

© The Author(s) 2023. Open Access This article is licensed under a Creative Commons Attribution 4.0
International License (https://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, shar-
ing, adaptation, distribution and reproduction in any medium or format, for any purpose, even commercially, as long as you
give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate
if changes were made.

www.comengsys.com