💻 computer science

Weakly Non-Negative Supermartingales for Omega-Regular Verification

本文引入了惰性 Streett 超鞅及其字典序扩展，以利用弱非负多项式模板实现概率程序中几乎处处 $\omega$ -正则属性的可靠自动化验证，从而扩大了搜索空间，并显著提高了相对于传统强非负方法在验证成功率方面的表现。

原作者： Toru Takisaka, Hongjie Qing, Libo Zhang

发布于 2026-07-21

📖 1 分钟阅读☕ 轻松阅读

原作者： Toru Takisaka, Hongjie Qing, Libo Zhang

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

想象一下，你是一名试图在一个计算机程序内部破解谜题的侦探。但这不是一个普通的程序，而是一个“概率性”程序，这意味着它通过掷骰子来做决定。有时它向左走，有时向右走，有时甚至可能会陷入无限循环而永远无法停止。你的任务是证明，无论骰子如何滚动，程序最终都会完成它的工作或遵循一套特定的规则。为了做到这一点，数学家们使用了一个巧妙的工具，叫做“鞅”（martingale）。你可以把“鞅”想象成一个神奇的计分卡。如果你能找到一个随着程序运行而持续下降（或保持受控状态）的计分卡，你就知道这个程序是安全的，并且最终会停止。

长期以来，这些计分卡都有一个严格的规则：它们在任何地方都必须是正数，就像一个永远不会欠债的银行账户一样。这使得寻找计分卡变得非常困难，就像是在一大堆钥匙中寻找一把特定的钥匙，而且你只能看那些闪亮的金钥匙。研究人员在这篇论文中提出了一个简单的问题：“如果我们允许计分卡在短时间内出现负数，只要它在实际运行时表现良好，会怎么样呢？”他们发现，如果谨慎地放宽这一规则，就能更容易地找到计实现计分卡，从而证明复杂的程序是安全的。

这篇论文的核心思想：用于掷骰子程序的“懒惰”计分卡

这篇论文介绍了一种构建这些神奇计分卡的新型、更灵活的方法，作者称之为**“懒惰斯特里特超鞅”（Lazy Streett Supermartingales）**。要理解为什么这很重要，让我们先看看他们正在解决的问题。

在计算机验证的世界里，我们经常处理带有循环的程序。我们想知道：“这个循环会停止吗？”或者“这个程序会永远做正确的事情吗？”为了回答这个问题，我们使用一个证书——一个数学函数，它充当监视器。如果监视器看到程序的值在稳步下降，它就知道程序正朝着终点线前进。

然而，这里有一个陷阱：几十年来，这些监视器必须是严格非负的。想象一下一名登山者试图证明自己会到达山脚。旧规则说：“只有当你处于海平面以上时，你才能计算你的步数。”如果登山者在某一秒钟跌到了海平面以下，整个证明就会失效，即使他显然正在向下移动。这使得为许多程序寻找证明变得非常困难，因为完美的计分卡可能会在某些理论场景下跌破零点，即使程序本身并不会真的卡在那里。

作者意识到这个严格的规则太挑剔了。他们提出了一种新的计分卡类型，它是弱非负的。这就像是告诉登山者：“如果你暂时跌到海平面以下也没关系，只要你不会一直待在那里，并且只要你在那里时表现得足够‘规矩’即可。”

但问题的关键在于：在一个掷骰子的世界里（概率程序），所谓的“规矩”比听起来要难得多。论文指出了一个著名的陷阱：如果你只是在不加思考的情况下放宽规则，你可能会无意中创造出一个“虚假”的证明。你可能会拥有一个看起来在下降的计分卡，但程序实际上却在无限运行，因为骰子的点数通过某种方式合谋，让计分卡保持在负值状态，从而欺骗了数学逻辑。

为了修复这个问题，作者发明了一套非常具体的条件，称为**“相对良态性”（relative well-behavedness）**。你可以把它想象成一个针对骰子的安全网。它确保程序中的随机数生成器（即骰子）不会产生向无穷远处延伸的“狂野”尾部。只要骰子的点数是有界的或以可预测的方式运行（这在几乎所有现实世界的随机过程中都是成立的），这个安全网就能保证“懒惰”计分卡不会被欺骗。如果没有这个特定的条件，在使用现代软件中常见的复杂多项式方程时，这个证明将会失效。有了它，证明才会坚如磐石。

解决方案：“懒惰”与“斯特里特”

论文结合了两个强大的概念来解决问题：

懒惰（Lazy）： 这意味着计分卡不需要在任何地方都是完美的。它只需要在程序处于“危险区域”（即我们试图证明会结束的循环部分）时是严格正数的。如果程序处于安全区域，计分卡可以是负数，只要它有一条规则说明：“如果我是负数，我就保持为负。”这可以防止程序利用负分来通过作弊手段进入无限循环。
斯特里特（Streett）： 这是一个用于处理复杂、长期行为（称为 $\omega$ -正则属性）的规则类型的花哨名称。我们不仅仅是问“它会停止吗？”，我们还可以问“它会永远检查交通灯吗？”或者“它最终会去邮局吗？”“斯特里特”部分允许计分卡处理这些复杂的、多步骤的承诺。

作者将这种新工具称为**“懒惰斯特里特超鞅”。他们从数学上证明了，如果你使用这些工具处理多项式方程（这是编程中常用的一种数学类型），并且如果程序中的随机数生成器是“相对良态”**的（意味着它们没有狂野且无界的尾部），那么这个证明就是可靠的。

为什么这很重要：研究结果

研究人员不仅写出了理论，还建立了一个测试工具。他们使用了 170 个不同的计算机程序（基准测试），这些程序已知是非常棘手的。他们用他们的新“懒惰”方法与旧的“严格”方法进行了对比测试。

结果令人印象深刻。要求计分卡永远不能为负值的旧方法仅成功验证了 170 个程序中的 88 个。而新的“懒惰”方法（它允许在受控条件下跌破零点，并配备了“相对良态”的安全网）成功验证了 128 个程序。这大约增加了 20 到 23.5 个百分点。

简单来说，通过稍微放宽规则，并聪明地处理如何放宽规则——特别是通过确保随机骰子点数是“相对良态”的——作者找到了证明更多程序是安全的方法。他们表明，我们不需要抛弃所有的“负数”可能性；我们只需要更好地理解它们。这使得计算机能够更轻松地自动检查我们的软件是否可靠，特别是当软件涉及随机性（如人工智能或模拟）时。

论文总结道，这种方法不仅仅是一个理论上的奇思妙想，而是一个实用的升级。它为验证更复杂的系统打开了大门，而不再受限于“每一个数学步骤都必须是正数”这一僵化要求。它提醒我们，有时为了寻找真相，你必须愿意去观察阴影，而不只是光亮。

技术摘要：用于 $\omega$ -正则验证的弱非负超鞅

1. 问题陈述

基于鞅的方法是概率程序验证的核心，特别是用于证明几乎处处终止（almost-sure termination）以及几乎处处满足 $\omega$ -正则属性（ $\omega$ -regular properties）。这些方法在算法适用性上的一个显著瓶颈是要求超鞅证书具有强全局非负性（strong global non-negativity）。虽然将搜索空间限制在可处理的类别（例如线性或多项式模板）内对于自动化合成是必要的，但严格的非负性约束往往会排除掉那些位于搜索空间之外的简单且有效的证书。

放宽非负性要求（允许“弱非负”函数）扩大了搜索空间，但也引入了一个关键挑战：在概率设置下，朴素的放宽是不完备/不稳健的（unsound）。与非概率情况不同，一个虽然在期望上递减但在某些情况下可能取任意负值的函数，可能会导致无法证明几乎处处终止或 $\omega$ -正则属性的满足。先前的工作仅在受限条件下建立了弱非负词典序排名超鞅（lexicographic ranking supermartingales, RSMs）的完备性：即仅限于线性模板、线性算术更新以及特定的“良好行为”（well-behaved）采样分布。这些限制阻碍了将弱非负性应用于一般多项式概率程序和更广泛的 $\omega$ -正则规范。

2. 方法论与技术方法

本文引入了**延迟 Streett 超鞅（Lazy Streett Supermartingales, Lazy SSMs）**及其词典序扩展——延迟词典序 SSM（Lazy LexSSMs），以解决上述局限性。该方法建立在三个核心技术支柱之上：

A. 相对良好行为的分布（Relatively Well-Behaved Distributions）

作者发现，现有的针对线性模板定制的“良好行为”条件对于多项式模板过于严格。具体而言，在多项式函数下，即使是区间上的均匀分布也会失效，因为多项式函数的“均值亏损”（mean shortfall）可能保持不变，而其为负值的概率却趋于零。

为了克服这一点，本文引入了相对良好行为性。这一新条件建立了一种权衡：如果一个多项式函数为负值的概率趋于零，那么其均值亏损必须相对于该函数的均值值趋于零。作者证明，所有有界支撑（bounded-support）的分布对于多项式模板都满足这一相对条件。这种泛化对于将完备性证明从线性扩展到多项式设置至关重要。

B. 通过分数幂变换进行的完备性证明

Lazy SSM 的完备性证明采用了一种不同于以往线性证明的新策略。作者并未直接分析多维词典序对象，而是：

隔离出一维 Lazy SSM 的完备性证明。
利用超鞅的分数幂变换 $(\eta^+)^\theta$ ，其中 $\theta \in (0,1)$ 。
利用相对良好行为性条件和 Jensen 不等式，证明该变换后的函数满足**强非负 Streett 超鞅（SSM）**的条件。
这种变换使得原始弱非负函数的排名条件能够转化为有效的、非负变换函数的排名条件，从而证明几乎处处的满足。

C. 组合式词典序提升（Compositional Lexicographic Lifting）

本文提供了一个关于词典序证书的组合说明。它证明了词典序 SSM 等价于一组共同证明目标属性的一系列一维 SSM。

分解： 一个 $\omega$ -正则 Streett 条件 $(S_{Fin}, S_{Inf})$ 被分解为一系列 Streett 对 $(S^{(i)}_{Fin}, S^{(i)}_{Inf})$ 。
等价性： 作者证明，每一个见证特定分解后的 Streett 对的一维 Lazy SSM 序列，等价于单个词典序 Lazy SSM。
益处： 这种方法简化了多维鞅的完备性证明，将其简化为一维情况的一个推论，避免了对非标准词典序的复杂分析。

D. 程序 MDP（Program MDPs）

该形式化定义在程序 MDP 上，这是马尔可夫决策过程（MDP）的一个子类，它抽象了概率控制流图（pCFG）的具体属性。这种抽象显式地公理化了诸如独立更新和有限多样性随机化等属性，明确了完备性结果的范围，并允许可测量的（非线性）程序更新。

3. 核心贡献

延迟 Streett 超鞅（Lazy SSMs）： 一种结合了“延迟”（弱非负）RSM 和 Streett 超鞅的新型鞅概念。这使得通过弱非负性来证明一般 $\omega$ -正则属性（不仅是终止性）的几乎处处满足成为可能。
有界支撑下的多项式完备性： 本文证明了在相对良好行为性假设下，多项式 Lazy SSM 的完备性。至关重要的是，作者证明了所有有界支撑分布都满足此条件，相比于此前要求“良好行为”分布和线性算术的先前工作，显著扩大了适用概率程序的类别。
组合式词典序框架： 一种新的证明策略，通过一系列一维证书将一维 SSM 的完备性提升到词典序变体，简化了理论分析。
自动化合成算法： 一种用于合成多项式 Lazy LexSSM 的算法，它通过增量构建证书序列，并通过“STAB”（负值稳定性）和“WORST”（最坏情况不影响）选项处理不同程序位置处条件的不可比性。

4. 实验结果

作者在 170 个包含 $\omega$ -正则规范的多项式概率程序合成基准测试（源自 LTL-VerP 基准测试）上评估了其方法。实验对比了三种变体：

STR： 强非负 LexSSM（基准线）。
WORST： 带有 “WORST” 选项的 Lazy LexSSM。
STAB： 带有 “STAB” 选项的 Lazy LexSSM。

结果：

基准线 (STR) 成功验证了 88 个实例 (51.7%)。
WORST 变体验证了 128 个实例 (75.2%)。
STAB 变体验证了 122 个实例 (71.7%)。
WORST 与 STAB 的并集成功验证了 134 个实例 (78.8%)。

这比强非负基准线在验证成功率上提升了 20.0–23.5 个百分点。结果表明，放宽非负性要求显著提高了基于模板合成的 $\omega$ -正则验证的算法适用性。

5. 重要性与主张

本文声称显著扩展了弱非负鞅方法的适用范围。通过从线性模板转向多项式模板，以及从可达性（终止性）转向一般的 $\omega$ -正则属性，作者将弱非负性的效用扩展到了更广泛的概率程序中。

其重要性在于：

在实际假设下的完备性： 向“相对良好行为性”的转变允许使用常见的有界支撑分布（如均匀分布）配合多项式模板，而此前这些分布因更严格的条件而被排除在外。
理论统一： 本文统一了延迟 RSM 和 Streett 超鞅的概念，提供了一个简化的框架，用于验证复杂的 $\omega$ -正则属性。
实际影响： 实验结果证实，理论上的约束放宽直接转化为更高的自动化验证工具成功率，使得复杂概率程序的验证变得更加可行。

作者对局限性保持了谦逊的态度，指出由于不同位置处鞅条件的不可比性，目前的合成算法在已知并非完备或多项式时间的，这是继承自底层延迟 RSM 合成问题的局限性。