Notes:
Also available from https://arxiv.org/abs/2202.06255

Abstract.
Neurosymbolic 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 (NSCSGs), which comprise two probabilistic finitestate agents interacting in a shared continuousstate 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 NSCSGs with Borel state spaces and prove the existence and measurability of the value function for zerosum discounted cumulative rewards under piecewiseconstant restrictions on the components of this class of models. To compute values and synthesise strategies, we present, for the first time, practical value iteration (VI) and policy iteration (PI) algorithms to solve this new subclass of continuousstate CSGs. These require a finite decomposition of the environment induced by the neural perception mechanisms of the agents and rely on finite abstract representations of value functions and strategies closed under VI or PI. First, we introduce a Borel measurable piecewiseconstant (BPWC) representation of value functions, extend minimax backups to this representation and propose a value iteration algorithm called BPWC VI. Second, we introduce two novel representations for the value functions and strategies, constantpiecewiselinear (CONPWL) and constantpiecewiseconstant (CONPWC) respectively, and propose Minimaxactionfree PI by extending a recent PI method based on alternating player choices for finite state spaces to Borel state spaces, which does not require normalform games to be solved.
