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 neuro-symbolic concurrent stochastic games (NS-CSGs), which comprise two probabilistic finite-state 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 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 continuous-state 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 piecewise-constant (B-PWC) representation of value functions, extend minimax backups to this representation and propose a value iteration algorithm called B-PWC VI. Second, we introduce two novel representations for the value functions and strategies, constant-piecewise-linear (CON-PWL) and constant-piecewise-constant (CON-PWC) respectively, and propose Minimax-action-free PI by extending a recent PI method based on alternating player choices for finite state spaces to Borel state spaces, which does not require normal-form games to be solved.

翻译：神经符号人工智能方法融合神经网络与经典符号技术，其重要性日益凸显，亟需形式化方法验证其正确性。我们提出一种新颖的建模形式——神经符号并发随机博弈（NS-CSG），该模型包含两个概率有限状态智能体在共享连续状态环境中的交互。每个智能体通过神经感知机制将图像等输入转换为符号感知结果，并基于符号进行决策决策。针对具有Borel状态空间的NS-CSG类别，我们证明了在分段常数约束下，零和折扣累积回报值函数的存在性与可测性。为计算值函数并合成策略，我们首次提出实用值迭代（VI）和策略迭代（PI）算法，用于求解这种新型连续状态CSG子类。这些算法通过智能体神经感知机制诱导的环境有限分解，依赖满足VI或PI封闭性的值函数与策略的有限抽象表示。首先，引入Borel可测分段常数（B-PWC）值函数表示，将极小化极大备份扩展至该表示，并提出称为B-PWC VI的值迭代算法。其次，分别提出常数分段线性（CON-PWL）与常数分段常数（CON-PWC）两种新型值函数与策略表示，通过将有限状态空间中基于交替玩家选择的PI方法扩展至Borel状态空间，提出无需求解正规形式博弈的极小化极大无动作PI。