🤖 AI

Automated Approach for Solving Infinite-state Polynomial Reachability Games

本文提出了一种可靠、半完备且次指数级的自动化算法，该算法利用排序证书来解决无限状态多项式可达性博弈，并成功在诸如“灰姑娘与继母”博弈等以往方法失效的复杂场景中计算出可达玩家的获胜策略。

原作者： Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Maximilian Seeliger, {\DJ}or{\dj}e Žikelić

发布于 2026-05-12

📖 1 分钟阅读☕ 轻松阅读

原作者： Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Maximilian Seeliger, {\DJ}or{\dj}e Žikelić

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

想象一场在巨大且无限的棋盘上进行的游戏，其中的棋子并非仅仅是黑白方格，而是像温度、速度或水位这样的复杂数学值。本文介绍了一种解决这些“无限状态”游戏的新方法，特别聚焦于两名玩家之间的博弈：REACH（攻击者）与SAFE（防御者）。

以下是作者所做工作的简要拆解，并辅以日常类比。

游戏：一场永无止境的拔河

在这些游戏中，棋盘由实数定义（例如温度计读数或银行账户余额）。

REACH 的目标：将游戏推向特定的“目标区域”（例如，水桶溢出、机器人到达目的地）。
SAFE 的目标：永远将游戏保持在远离该目标区域的状态。

通常，如果棋盘是无限的，用计算机找出谁将获胜是不可能的。这就像试图数清沙滩上的每一粒沙子，以判断是否足以建造一座城堡；任务过于庞大。

核心思想：“进度计”（排序证书）

作者发明了一种新工具，称为排序证书。你可以将其想象为附着在游戏每一个可能状态上的魔法进度计或电池电量。

其工作原理如下：

电量规则：进度计必须始终显示正数（或零）。
耗电规则：每次移动时，电池电量必须至少减少一点点。
获胜者：如果电池电量归零（或变为负数），游戏结束，REACH 获胜，因为他们到达了目标。

关键点：

如果是SAFE 的回合，无论 SAFE 选择哪种移动，进度计都必须下降。SAFE 无法找到一种方法来保持电池电量不降。
如果是REACH 的回合，REACH 只需要找到一种能消耗电池电量的移动即可。

如果你能绘制出一张地图，其中每一次移动都会消耗电池电量，你就证明了无论 SAFE 如何努力阻止，REACH 最终都会获胜。这就是“排序证书”。

问题：“无限选择”陷阱

作者发现了这一想法中的一个缺陷。想象 SAFE 拥有一种超能力：他们可以从无限数量的移动中进行选择。

类比：想象 SAFE 可以选择将电池电量降低 0.1，或 0.01，或 0.0000001。如果 SAFE 不断选择越来越小的降幅，即使电量在下降，电池也可能永远不会真正归零。在这种特定的“无限选择”场景下，电池电量计的技巧无法证明胜利。

然而，作者证明，如果 SAFE 在每一步的选择被限制为有限数量（就像普通棋盘游戏一样），电池电量计的技巧就能完美运作，并构成一个完整的证明。

解决方案：自动化机器人求解器

本文提出了一种全自动计算机程序，执行以下操作：

猜测形状：它假设“电池电量计”是一个多项式方程（一种涉及变量如 $x$ 、 $y$ 、 $x^2$ 等的复杂数学公式）。
填补空白：它使用计算机求解器来找出使该公式作为有效电池电量计运作的确切数值。
输出策略：如果找到了这些数值，它会为你提供 REACH 的确切获胜移动，以及证明它们有效的数学证明（即证书）。

这有何特别之处？
以前的方法就像试图通过逐一检查每一块拼图来解谜题，要么耗时无穷，要么在复杂谜题上失败。这种新方法更快（次指数时间），并且能够处理比以前的工具（仅限于简单的线性数学）更复杂的数学（多项式）。

现实世界测试：灰姑娘与继母游戏

为了证明其方法有效，作者在一个名为灰姑娘与继母游戏的著名谜题上进行了测试。

设定：继母（REACH）向 5 个水桶中倒水。灰姑娘（SAFE）倒空两个水桶。如果任何水桶溢出，继母获胜。
挑战：多年来，计算机只能在水桶非常小的情况下解决此问题。如果水桶几乎满了（但还没满），计算机就会陷入停滞。
结果：作者的新工具解决了任何尺寸水桶的游戏，甚至是那些任意接近溢出的水桶。它找到了继母的获胜策略，而其他计算机工具此前无法做到这一点。

总结

本文引入了一种新的“电池电量计”证明规则，以表明攻击者可以赢得复杂的无限游戏。他们构建了一个机器人，利用高级数学自动设计这种电池电量计。该机器人是首个成功解决此前计算机无法破解的困难无限状态游戏的工具，特别是经典的“灰姑娘与继母”水桶谜题。

技术摘要：求解无限状态多项式可达性游戏的自动化方法

问题陈述

本文解决了无限状态可达性游戏的求解问题。这类游戏是在图上进行的两人轮流博弈，其中节点被划分为REACH玩家（其目标是将游戏强制推进到特定的目标状态集）和SAFE玩家（其目标是无限期地避免目标状态集）。

虽然有限图上的可达性游戏已被充分理解且可在多项式时间内求解，但无限状态变体通常是不可判定的（根据 Rice 定理），即使是在一个玩家仅有一个动作的受限情况下也是如此。现有方法通常依赖于将问题归约到逻辑可满足性（例如约束霍恩子句）或不动点计算，但这些方法在处理多项式约束、提供完备性保证或实现高效运行时面临局限。本文解决的具体挑战是：确定在由实值变量和多项式约束定义的游戏里，REACH 玩家是否存在获胜策略，并计算该策略。

方法论

1. 排序证书

核心理论贡献是引入了用于可达性游戏的排序证书。受用于证明程序终止的排序函数的启发，排序证书是一个将游戏状态映射到实值的函数 $f: S \to \mathbb{R}$ 。为了作为 REACH 玩家获胜策略的见证， $f$ 必须满足三个条件：

起始非负性： $f(s_{init}) \ge 0$ 。
安全进展（SAFE 回合）：如果当前状态 $s$ 属于 SAFE 且 $f(s) \ge 0$ ，那么对于所有可能的后继状态 $s'$ ，必须满足 $f(s) - 1 \ge f(s') \ge 0$ 。这确保 SAFE 无法阻止数值下降。
可达性进展（REACH 回合）：如果当前状态 $s$ 属于 REACH 且 $f(s) \ge 0$ ，则存在一个后继状态 $s'$ 使得 $f(s) - 1 \ge f(s') \ge 0$ 。这确保 REACH 可以选择一个严格减小数值的移动。

该函数的值充当向目标集进展的度量。本文证明了此类证书的存在意味着 REACH 存在无记忆获胜策略（可靠性）。虽然该证明规则对于一般的无限状态游戏并不完备（因为 SAFE 可能从无限多个值中选择以强制无界下界），但已证明如果 SAFE 在每一步仅有有限个选择，则该规则是可靠且完备的。

2. 自动化合成算法

作者提出了一种针对多项式可达性游戏的全自动算法，其中守卫、更新和目标均由实变量上的多项式不等式定义。该算法分为四个步骤：

模板设置：算法为排序证书 $f$ 和无记忆策略 $\sigma$ 固定最大次数为 $D$ 的符号多项式模板。
约束收集：生成关于符号模板变量的约束系统。这些约束编码了排序证书定义的条件（C1–C3），用符号模板替换函数。
量词消去：约束包含全称量词（例如“对于所有 $x$ "）。算法应用基于Putinar 定理（针对一般多项式）或Farkas 引理（针对线性多项式）的转换，将这些约束转化为纯存在量词的多项式约束系统。
求解：使用现成的 SMT 求解器（如 Z3、MathSAT5）求解生成的系统。解将给出多项式模板的具体系数，从而产生有效的排序证书及相应的获胜策略。

该算法是可靠的（任何计算出的策略都是正确的）且半完备的（如果解存在于多项式证书类中且状态空间是紧致的，则保证能找到解）。对于固定的多项式次数，其运行时间相对于输入规模是次指数级的。

主要贡献

理论框架：引入排序证书作为特定子类无限状态游戏（SAFE 具有有限选择）的可靠且完备的证明规则。这将排序函数的概念从程序终止推广到了博弈论。
自动化：开发了一种全自动算法，用于合成多项式可达性游戏的获胜策略和形式正确性见证（即证书）。
复杂性与范围：该方法处理多项式算术（不同于此前仅限于线性算术的方法），并实现了次指数级复杂度（改进了先前线性算术方法的双指数复杂度）。
实验验证：实现了一个原型，成功解决了现有工具此前无法处理的具有挑战性的基准测试。

实验结果

作者在两个主要基准测试上评估了他们的方法：

灰姑娘与继母游戏：
- 经典变体：继母（REACH）将水分发到桶中，灰姑娘（SAFE）倒空两个相邻的桶。目标是使某个桶溢出。
- 结果：所提方法解决了容量高达 $2 - 10^{-10}$ 的游戏，并且关键的是，在不到 1 秒的时间内解决了符号情况 $2 - \epsilon$ （其中 $\epsilon > 0$ ）。
- 对比：最先进工具（GenSys 和 rpgsolve）在 $2 - 10^{-10}$ 案例上失败（超时或不支持），且无法处理符号 $2 - \epsilon$ 案例。这代表了该游戏中任意精度参数的首个自动化解决方案。
- 非线性变体：继母的分发受欧几里得范数（ $\ell_2$ ）而非曼哈顿范数（ $\ell_1$ ）约束的版本，引入了非线性。所提方法在不到 1 秒内解决了固定容量案例，而基线方法完全失败。
故障机器人基准：
- 一个模拟机器人混合化学品的游戏，其中对手引入故障。机器人的目标是达到特定的密度和体积。
- 结果：所提方法在 44 秒内解决了该游戏。基线 GenSys 在 5 分钟超时内未能终止。

意义与主张

本文主张，其方法通过提供一种单一方法中前所未有的独特功能组合，显著推进了求解无限状态可达性游戏的最先进水平：

适用于多项式游戏：不同于先前仅限于线性算术的可靠/半完备方法。
半完备性保证：不同于可能不终止或缺乏完备性保证的不动点方法。
效率：与双指数替代方案相比，具有次指数级运行时间。

作者强调，他们的方法是首个为任意精度参数（ $2 - \epsilon$ ）计算经典灰姑娘与继母游戏最优获胜策略的方法，这是一个此前对自动化求解器而言未解决的问题。他们承认局限性，指出该方法目前仅适用于多项式游戏并专注于可达性目标，将扩展到非多项式游戏和其他目标（例如 $\omega$ -正则或定量目标）留作未来工作方向。