⚡ electrical engineering

Robust Verification of Concurrent Stochastic Games

本文引入了鲁棒并发随机博弈（特别是区间并发随机博弈），以处理转移概率中的认识不确定性，为零和及非零和目标的最坏情况鲁棒验证提供了一个理论框架和高效算法，这些内容已在 PRISM-games 模型检测器中实现，并在大型基准测试上得到了验证。

原作者： Angel Y. He, David Parker

发布于 2026-01-22

📖 1 分钟阅读☕ 轻松阅读

原作者： Angel Y. He, David Parker

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

大局观：迷雾世界中的规划

想象你是一支无人机编队的队长。你需要协调你的无人机安全地交付包裹。在一个完美的世界里，你会确切知道风向如何吹拂、电池如何消耗，以及其他无人机会做出什么反应。你可以计算出一个完美的计划。

但在现实世界中，情况是混乱的。你不知道确切的风速（那只是一个猜测），你的传感器存在噪声，而且你不知道其他无人机是在遵循你的计划，还是在试图干扰你的信号。这就是不确定性。

这篇论文解决了一个问题：当你不了解游戏的精确规则时，如何证明你的系统是安全的？

旧方法：“完美地图”问题

此前，计算机科学家使用一种称为**并发随机博弈（Concurrent Stochastic Game, CSG）**的模型来检查这些系统是否正常工作。可以将 CSG 想象成一个多个玩家同时移动的棋盘游戏。

问题在于： 要玩这个棋盘游戏，你需要一张能告诉你落在每个方格上的确切概率的地图。
缺陷： 在现实生活中，我们很少拥有确切的概率。我们拥有的是估计值。如果你基于一张略有偏差的地图来构建安全计划，那么当现实世界（即“迷雾”）袭来时，你的计划可能会失败。

新方案：“最坏情况”地图

作者引入了一种新的模型，称为鲁棒并发随机博弈（Robust Concurrent Stochastic Games, RCSGs），特别是一种被称为**区间 CSG（Interval CSGs, ICSGs）**的类型。

类比：区间地图
新模型不再说“下雨的概率是 50%”，而是说“下雨的概率在 40% 到 60% 之间”。

这创造了一个可能性的“云团”，而不是一个单一的点。
系统不仅检查计划在平均天气下是否有效，还会检查即使天气落在 40%-60% 范围内的绝对最坏情况时，计划是否依然有效。

这被称为鲁棒验证（Robust Verification）。它在问：“即使‘自然’（环境）竭尽全力想要破坏我们，我们能否保证安全？”

角色：智能体、对手与“自然”

在这些博弈中，通常有两种类型的玩家：

智能体（Agents）： 试图实现目标的无人机或机器人。
自然（Nature）： 环境（风力、噪声、数据错误）。

在旧模型中，“自然”只是一个随机的硬币投掷。在这个新模型中，自然是一个对手。

零和博弈（团队 vs. 团队）： 想象一场国际象棋比赛。一个玩家想要赢；另一个玩家想要阻止他。在这里，“自然”会与对手联手，尽可能让游戏对第一个玩家变得更加艰难。
非零和博弈（合作 vs. 混乱）： 想象两架无人机正在共同尝试交付包裹。它们想要实现其总和的最大化。在这里，“自然”表现得像一个淘气的恶作剧小精灵，试图最小化它们的总成功率，即便这会对两者都造成伤害。

他们是如何解决的：“影子博弈”

作者面临着一个巨大的数学挑战：当玩家同时行动且环境不可预测时，如何计算“最坏情况”的结果？

技巧：影子博弈
他们发明了一种巧妙的方法，将这个混乱、不确定的问题转化为一个标准的、可求解的棋盘游戏。

他们在游戏盘上增加了一个第三个玩家：自然。
在这个“影子博弈”中，自然可以在智能体选择行动之后进行移动。自然会观察所有可能的结果，并选择那个对智能体伤害最大的结果。
通过这种方式，他们将一个复杂的“不确定”问题转化为了一个标准的“多玩家博弈”，现有的计算机工具（如 PRISM-games 检查器）已经可以解决此类问题。

结果：

对于竞争性博弈（零和博弈）： 他们将问题转化为了一个 2 玩家博弈（智能体 vs. 对手 + 自然组成的团队）。它的运行速度几乎与旧方法一样快。
对于合作性博弈（非零和博弈）： 它变成了一个 3 玩家博弈。这更难且需要更多的计算时间，但他们开发了一个过滤系统来寻找最佳的“鲁棒纳什均衡”（Robust Nash Equilibrium，即在已知可能发生最坏情况的情况下，没有人想要改变其策略的状态）。

他们测试了什么

他们将此功能集成到了一个软件工具中，并在大型复杂场景中进行了测试，例如：

机器人协作： 让机器人在移动过程中不发生碰撞。
网络流量： 管理繁忙网络中的数据流。
无线电干扰： 保护信号免受干扰。

研究发现：

它有效： 该软件即使在数据不确定的情况下也能成功计算出安全策略。
速度： 对于竞争性场景，它仅比旧方法慢了大约两倍（而旧方法对计算机来说已经非常快了）。对于合作性场景，它虽然较慢，但仍能处理大型系统。
“迷雾”因素： 他们发现，拥有一点点不确定性（一小片“迷雾”）有时会让计算更快，因为系统会更快地收敛到解决方案。然而，过多的不确定性会导致“最坏情况”过于保守（非常安全，但也可能过于谨慎）。

总结

这篇论文为我们在信息不完全的情况下，如何检查自主系统（如自动驾驶汽车或无人机）的安全性提供了一种新方法。与其猜测确切的概率，不如假设环境会在已知范围内尽可能地刁难我们。他们将这个困难的数学问题转化为了计算机可以解决的标准博弈，从而确保我们未来的机器人不会仅仅因为风向比预期吹得稍微不同了一点就发生碰撞。

技术摘要：并发随机博弈的鲁棒验证

1. 问题陈述

运行在多智能体环境（如无人机协同、机器人探索）中的自主系统通常需要处理不确定性下的同步策略决策。虽然**并发随机博弈（Concurrent Stochastic Games, CSGs）为建模此类系统提供了强大的框架，但标准的验证技术假设转移概率是精确已知的。在现实中，由于建模不准确、噪声、抽象或数据有限（这在强化学习中很常见），这些概率往往受到认识不确定性（epistemic uncertainty）**的影响。

标准的 CSG 验证如果底层模型稍有偏差，其结果可能会变得不可靠。虽然鲁棒马尔可夫决策过程（Robust Markov Decision Processes, RMDPs）通过考虑可能的转移概率集合解决了单智能体系统中的这一问题，但针对多智能体并发设置的类似框架仍处于发展不足的状态。挑战在于如何将鲁棒性扩展到玩家同时行动的并发博弈中，且“自然”（负责解决不确定性）需与多个策略型智能体进行交互。

2. 方法论

本文引入了鲁棒并发随机博弈（Robust Concurrent Stochastic Games, RCSGs），并重点研究了一个易于处理的子类——区间 CSG（Interval CSGs, ICSGs），其中转移概率被限制在区间内。该方法涉及理论基础、博弈论归约以及算法实现。

2.1 理论框架

作者定义了在关于转移不确定性的最坏情况假设下，针对零和和非零和设置的鲁棒解概念：

零和博弈： 该框架适配了极小极大（minimax）概念。如果一个博弈的价值在玩家与“自然”（解决不确定性的对手）行动顺序不同时仍保持一致，则称该博弈是鲁棒确定的。论文证明，对于有限分支的 ICSGs，**玩家优先（player-first）和自然优先（nature-first）**语义会产生相同的鲁棒值。
非零和博弈： 论文引入了鲁棒纳什均衡（Robust Nash Equilibria, RNE）和鲁棒社会福利最优纳什均衡（Robust Social-Welfare Optimal NE, RSWNE）。RNE 是指在任何不确定性解析下都能保持为纳什均衡的策略组合。作者专注于研究亚博弈完美 $\epsilon$ -RNE 以确保其存在性。

2.2 向标准博弈的归约

核心贡献之一是通过**对抗性扩展（Adversarial Expansion）**将鲁棒验证问题归约为标准（非鲁棒）CSGs：

零和归约： 一个 ICSG 可归约为一个 2 玩家 CSG ( $G_A$ )，通过添加第三个“自然”玩家，该玩家针对玩家 1 进行对抗。由于玩家 2 和“自然”共享最小化玩家 1 收益的目标，因此他们形成了一个联盟。原始 ICSG 的鲁棒值等于这个扩展后的 2 玩家 CSG 的值。
非零和归约： 该归约创建了一个 3 玩家 CSG ( $G_A$ $G_{A}$ )，其中玩家 3（自然）通过最小化玩家 1 和玩家 2 的社会福利（效用之和）来对抗他们。
- 挑战： 扩展后的 3 玩家博弈中的纳什均衡并不自动意味着原始博弈中的鲁棒 NE，因为“自然”对效用总和的最小化并不一定意味着对每个个体效用的最小化。
- 解决方案： 作者提出了一个过滤步骤。在计算 $G_A$ 的均衡后，通过使用偏差 IMDPs（区间 MDPs）检查策略组合是否满足 RNE 条件来进行过滤。这确保了该策略组合对于每个玩家的最坏情况选择都是鲁棒的。

2.3 算法

论文开发了用于求解这些归约后博弈的高效算法：

无限时界： 使用鲁棒值迭代（Robust Value Iteration, RVI）。对于每个状态和联合动作，首先求解一个内部优化问题（寻找区间内最坏情况的转移分布），随后进行线性规划（LP）或双矩阵博弈求解。
有限时界： 使用鲁棒后向归纳（Robust Backward Induction, RBI）。
实现： 这些算法在 PRISM-games 模型检测器中实现。该方法通过在线求解内部问题和正规形式博弈（NFGs），避免了显式构建完整的扩展状态空间。

3. 核心贡献

模型定义： 引入了 RCSGs 和 ICSGs，用于模拟具有区间边界转移不确定性的多智能体系统。
理论基础：
- 证明了零和 ICSGs 中玩家优先与自然优先语义之间的值等价性。
- 建立了鲁棒纳什均衡和 RSWNE 的概念。
- 论证了鲁棒验证可以归约为求解标准 CSGs（零和为 2 玩家，非零和为带过滤的 3 玩家）。
算法实现： 开发了针对有限和无限时界的易处理算法，将鲁棒动态规划与标准 CSG 求解技术（值迭代、Lemke-Howson 算法）相结合。
实证评估： 在 PRISM-games 中实现并使用大型基准测试（机器人协同、Aloha、干扰无线电系统）进行了评估。

4. 实验结果

作者使用带有扰动转移概率（ $\pm \epsilon$ ）的基准测试，将该方法与标准（非鲁棒）CSGs 进行了对比评估。

零和性能： ICSGs 的验证时间与标准 CSGs 相当，通常在 2 倍因子以内。该方法成功处理了拥有超过 200 万个状态和 1000 万个转移的模型。在某些情况下（如 Aloha），由于所需的迭代次数较少，ICSG 的验证速度反而更快。
非零和性能： 由于 3 玩家归约和过滤步骤的复杂性，验证时间较高。该方法能有效扩展至包含高达 0.4 百万个状态和 1.3 百万个转移的模型。
不确定性 ( $\epsilon$ ) 的影响：
- 验证时间随 $\epsilon$ 的变化呈现非单调性；由于单次迭代成本与收敛速度之间的权衡，中间值的处理往往比极小或极大值的处理更慢。
- 增加 $\epsilon$ 会产生更保守（更低）的值，从而有效地为验证结果提供置信区间。

5. 重要性与主张

本文声称填补了形式化验证中的一个关键空白，即提供了一个用于推理多智能体并发系统中认识不确定性的原则性框架。

实用性： 作者证明了鲁棒验证对于大规模系统是可行的，而非仅仅是理论构想。零和情况下的扩展性与标准验证相当，使其能够立即应用于安全至上的对抗性场景。
洞察力： 非零和结果强调了鲁棒多智能体推理的内在复杂性，特别是最小化社会福利与个体鲁棒性之间的区别，这使得提出的过滤机制变得必要。
基础性： 通过将 RCSGs 归约为标准 CSGs，这项工作利用了现有的工具支持（PRISM-games）和理论成果，为自主系统的鲁棒分析提供了一条可扩展的路径。

作者总结道，尽管非零和情况引入了更高的计算需求，但该框架成功实现了对抵御模型误差的策略合成，这是在不确定的现实环境中部署自主系统的关键要求。