🤖 machine learning

Value Functions as Supermartingale Certificates

本文建立了一种理论联系，表明满足 $\omega$ -正则属性的策略其价值函数编码了 Streett 超鞅证书，从而架起了形式化验证与强化学习之间的桥梁，以实现在有限、可数无限以及连续状态空间上的原则性证书合成。

原作者： Alessandro Abate, Daniel Contro, Mirco Giacobbe, Agustín Martínez-Suñé, Diptarko Roy

发布于 2026-06-01

📖 1 分钟阅读☕ 轻松阅读

原作者： Alessandro Abate, Daniel Contro, Mirco Giacobbe, Agustín Martínez-Suñé, Diptarko Roy

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

想象一下你正在教一个机器人如何在迷宫中导航。你想让它遵循一套复杂的规则，比如“一直走直到找到宝藏，然后永远留在安全区，并且绝不踏入岩浆”。在计算机科学的世界里，这被称为满足一个“ $\omega$ -正则”（omega-regular）属性（这是一个高级说法，指适用于无限旅程的规则）。

长期以来，有两种处理这种问题的方法：

“数学证明”法（验证/Verification）： 数学家使用一种叫做**超鞅证书（Supermartingale Certificate）**的东西。你可以把它想象成一个“安全性评分表”。如果你能画出一张地图，其分数随着机器人的移动而始终下降（或保持不变），且仅在机器人处于安全状态时达到零，那么你就拥有了一个数学证明，证明无论骰子点数如何变化（随机性），机器人永远不会失败。问题在于，为复杂的迷宫手工绘制这样一张地图极其困难，且难以扩展到大规模场景。
“试错”法（强化学习/Reinforcement Learning）： 这是机器人通过实践进行学习的过程。它尝试各种动作，根据好的移动获取奖励，并学习一个价值函数（Value Function）。你可以把价值函数想象成一张“幸福地图”，它告诉机器人从任何位置出发，预期未来能获得多少回报。虽然这在寻找最优路径方面效果很好，但它通常缺乏形式化的保证，即无法确保机器人一定会成功，尤其是在复杂、无限或连续的世界中。

重大突破

这篇论文弥合了这两个世界之间的鸿经过。作者们发现了一个令人惊讶的秘密：如果机器人的“幸福地图”（价值函数）是使用一种非常特定的奖励系统构建的，那么这张图本身就是一份有效的“安全性评分表”（超鞅证书）。

他们是如何做到的，以下是使用简单类比进行的说明：

两种奖励配方

作者提出了两种不同的给机器人提供奖励的方法，使得其生成的“幸福地图”能自动成为一份有效的安全证明。

配方 1：“安全区”奖励

运作方式： 你告诉机器人：“每当你踏入‘安全区’（或一个你能保证永远保持安全的区域）时，你就获得一分。”
神奇之处： 如果机器人确实在遵守规则，它的“幸福地图”会在安全区之外自然地处于高位，并随着它接近安全区而降低。一旦进入安全区，地图就会保持平稳。
难点： 要使用这种方法，你需要预先知道哪些区域是机器人会永远停留的“安全区”。在复杂的系统中，这很难提前得知。

配方 2：“惩罚与奖赏”奖励

运作方式： 你告诉机器人：“每当你处于‘危险区’（等待达成目标阶段）时，你会受到微小的惩罚（负分）；而当你最终到达‘目标点’时，你会获得一大笔奖赏。”
神奇之处： 当机器人在危险区移动时，由于它正接近大奖并正在摆脱惩罚，其“幸福地图”会逐渐上升。一旦到达目标点，地图就会趋于稳定。
难点： 这不需要预先知道“安全区”，只需要知道规则（规范）。但是，它需要一个稍微复杂一点的数学设置（一种特殊的折扣因子）来使数值计算成立。

他们证明了什么

作者从数学上证明了，如果你使用上述任一奖励配方，并且机器人确实成功遵循了规则，那么生成的“幸福地图”就是一个有效的超鞅证书。

这意味着：

你不需要手动绘制安全地图。
你可以使用标准的强化学习工具来训练机器人。
一旦训练完成，你可以查看机器人的“幸福地图”，将其在数学上进行翻转，就能立即获得一份正式的、数学上的证明，证明机器人几乎 100% 会成功。

实验

他们在“湿滑迷宫”（机器人可能会因意外而向错误方向滑动）的计算机模拟中测试了这一点。

他们训练机器人遵循各种复杂的规则（例如“找到 $b$ 且永远不要碰到 $h$ ”）。
他们计算了成功机器人的“幸福地图”。
他们根据安全规则检查了该地图。
结果： 这些地图完美通过了测试。成功的机器人拥有有效的证书；而失败的机器人则没有。

为什么这很重要（根据论文所述）

这为**认证强化学习（Certified Reinforcement Learning）**开辟了一条全新的、有原则性的路径。与其仅仅“希望”一个学习到的策略有效，或者费力地编写复杂的证明，我们现在可以：

使用标准 AI 方法训练策略。
评估其价值函数。
检查该函数是否满足“安全性评分表”的规则。

如果满足，我们就拥有了该策略有效的正式保证。这表明，即使是在人类无法手动分析的复杂、连续或无限的环境中，我们也可以利用数据驱动的方法（如神经网络）来构建这些安全证明。

技术摘要：作为超鞅证书的价值函数

问题陈述

在一般状态空间（有限、可数无限及连续空间）上针对 $\omega$ -正则属性（包括线性时序逻辑，LTL）进行随机系统验证，通常依赖于超鞅证书（supermartingale certificates）。这些证书是满足特定证明规则的实值函数，用作几乎处处满足规范的数学保证。然而，合成这些证书具有挑战性；现有方法通常依赖于约束优化，这在面对大规模或连续状态空间时扩展性较差。

相反，**强化学习（RL）*已被广泛应用于为 $\omega$ -正则任务合成策略。虽然 RL 方法可以最大化满足概率，但它们通常缺乏形式化保证，即无法证明一个已训练*（非最优）的策略在特定概率下满足规范，尤其是在超出有限状态和动作空间的场景下。超鞅验证的理论机制与 RL 策略评估的实际机制之间存在脱节。

方法论

本文建立了折扣强化学习设置中策略的价值函数与 Streett 超鞅证书之间的全新理论联系。其核心假设是：在特定的奖励设计下，几乎处处满足 LTL 规范的策略 $\pi$ 的价值函数 $V^\pi$ 编码了一个有效的 Streett 超鞅。

作者提出了两种不同的奖励设计来实现这一目标：

奖励设计 1（吸收集知识）：
- 要求： 需要了解由策略诱导的吸收集（具体为 Streett 对集合并集的最大吸收子集）。
- 机制： 当过程进入目标集 $B$ 或进入一个既无法再次访问 $A$ 也无法再次访问 $B$ 的吸收集时，奖励设为 1。
- 理论基础： 价值函数 $V^\pi$ 代表这些奖励的期望折扣总和。通过定义证书 $W(s) = C - V^\pi(s)$ （其中 $C$ 是与折扣因子相关的常数），作者证明了 $W$ 满足 Streett 超鞅条件：在 $A \setminus B$ 中，由于对首次到达时间的一致界限，其期望值严格下降；而在其他地方则保持非增特性。
奖励设计 2（仅需规范知识）：
- 要求： 仅需了解规范（Streett 对 $(A, B)$ ），无需了解策略的具体吸收集。
- 机制： 该设计采用状态相关折扣因子 $\Gamma(s)$ 以及为访问 $B$ 分配正奖励、为访问 $A \setminus B$ 分配负奖励的奖励函数。
- 理论基础： 折扣因子在奖励非零时设为 $\gamma < 1$ ，否则为 1。在“正复现界限”（Positive Recurrence Bound，限制在到达 $B$ 之前停留在 $A$ 中的预期步数）假设下，价值函数同样编码了一个超鞅。通过调整正负奖励的比例，确保证书保持非负且在必要处严格递减。

两种方法都被证明适用于有限、可数无限及连续状态空间。证明过程依赖于将价值函数与首次到达时间及价值的一步期望变化量联系起来的引理。

核心贡献

理论桥梁： 本文证明了在适当的奖励设计下，满足 LTL 规范的策略的价值函数是一个有效的 Streett 超鞅证书（定理 1 和定理 2）。
两种奖励方案： 作者提供了两种构建这些奖励的方法：一种利用策略特定的吸收集（定理 1），另一种仅依赖于规范结构结合状态相关折扣（定理 2）。
通用性： 结果不仅限于有限 MDP；它们适用于一般状态空间，填补了现有基于 RL 的验证在处理无限或连续空间时缺乏形式化保证的空白。
实验验证： 作者在网格世界（Grid-world）环境下，利用有限马尔可夫决策过程（MDP）对理论进行了实验验证。他们针对涵盖 Manna-Pnueli 层级的各种 LTL 规范合成了证书，验证了超鞅证明规则，并通过 PRISM 模型检测器交叉检查了满足概率。

结果

实验验证： 在网格世界实验中，所提出的奖励设计成功地为满足规范（满足概率为 1.0）的策略合成了有效的证书。对于不满足规范的策略，证明规则失效（无效证书），且 PRISM 确认其满足概率严格小于 1。
一致性： 实验结果与理论保证完美契合，证明了该价值函数方法能够正确识别满足与不满足规范的策略。
实验局限性： 目前的实验受限于通过线性系统精确计算价值函数的有限 MDP。论文指出，未来工作将研究如何使用参数化近似（如神经网络）将此扩展到无限/连续空间。

意义与主张

本文声称开辟了一条**“通过 RL 进行证书合成的有原则路径”。通过将寻找超鞅证书的问题（传统上是一个约束优化问题）重新定义为策略评估后接证书检查**的问题，作者提出了一条将验证扩展到大规模和连续状态空间的途径。

作者强调，虽然定理为价值函数成为证书提供了充分条件，但只要证明规则成立，证书本身就是有效的，无论是否独立验证了定理的假设（如一致的首次到达时间界限）。这允许了一个实际的工作流：训练策略，估计其价值函数，然后直接验证超鞅条件。

本文将此项工作定位为迈向**认证强化学习（Certified Reinforcement Learning）**的基础性步骤，旨在使经过训练的策略能够针对 $\omega$ -正则属性进行形式化验证，从而超越有限状态空间，弥合 RL 的可扩展性与形式化验证的严谨性之间的鸿沟。