Strategy synthesis for zero-sum neuro-symbolic concurrent stochastic games

Neuro-symbolic approaches to artificial intelligence, which combine neural networks with classical symbolic techniques, are growing in prominence, necessitating formal approaches to reason about their correctness. We propose a novel modelling formalism called neurosymbolic concurrent stochastic games (NS-CSGs), which comprise two probabilistic finitestate agents interacting in a shared continuous-state environment. Each agent observes the environment using a neural perception mechanism, which converts inputs such as images into symbolic percepts, and makes decisions symbolically. We focus on the class of NS-CSGs with Borel state spaces and prove the existence and measurability of the value function for zero-sum discounted cumulative rewards under piecewise-constant restrictions. To compute values and synthesise strategies, we first introduce a Borel measurable piecewiseconstant (B-PWC) representation of value functions and propose a B-PWC value iteration. Second, we introduce two novel representations for the value functions and strategies, and propose a minimax-action-free policy iteration based on alternating player choices. (c) 2024 The Author(s). Published by Elsevier Inc. This is an open access article under the CC BY license (http://creativecommons .org /licenses /by /4 .0/).