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 probabilistic finite-state agents interacting in a shared continuous-state environment observed through perception mechanisms implemented as neural networks (NNs). 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, implementable value iteration (VI) and policy iteration (PI) algorithms to solve a class of continuous-state CSGs. These require a finite representation of the pre-image of the environment's NN perception mechanism 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 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. We illustrate our approach with a dynamic vehicle parking example by generating approximately optimal strategies using a prototype implementation of the B-PWC VI algorithm.

翻译：神经符号人工智能方法将神经网络与经典符号技术相结合，其重要性日益凸显，因此需要形式化方法对其正确性进行推理。我们提出了一种新颖的形式化建模框架——神经符号并发随机博弈（NS-CSG），该框架包含概率有限状态智能体，它们在一个共享的连续状态环境中交互，并通过作为神经网络（NN）实现的感知机制进行观测。我们重点关注具有Borel状态空间的NS-CSG类别，并证明了在该类别模型的分段常数限制下，零和折扣累积奖励的值函数的存在性与可测性。为了计算值函数并综合策略，我们首次提出了可实现的数值迭代（VI）和策略迭代（PI）算法，用于求解一类连续状态CSG。这些算法需要对环境神经网络感知机制的原像进行有限表示，并依赖于在VI或PI下封闭的值函数与策略的有限抽象表示。首先，我们引入了值函数的一种Borel可测分段常数（B-PWC）表示，将该表示扩展至极小极大备份，并提出了B-PWC VI算法。其次，我们分别引入了值函数与策略的两种新型表示——常数分段线性（CON-PWL）和常数分段常数（CON-PWC），并通过将一种基于交替玩家选择的有限状态空间最新PI方法扩展到Borel状态空间，提出了无需极小极大行动的PI算法，该算法无需求解正规型博弈。我们通过一个动态车辆停放示例，利用B-PWC VI算法的原型实现生成近似最优策略，展示了该方法的有效性。