💻 computer science

Multiobjective Preexpectation Reasoning for Probabilistic Programs

本文引入了一种用于具有非确定性的概率程序中多目标策略合成的演绎式程序级框架，该框架利用一种多目标预期望转换器，将后期望映射到凸 Hoare 幂域内的可实现值集，从而在无需有限状态空间的情况下，能够稳健地处理无限状态马尔可夫决策过程。

原作者： Lena Verscht, Hannah Mertens, Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen

发布于 2026-08-14

📖 1 分钟阅读☕ 轻松阅读

原作者： Lena Verscht, Hannah Mertens, Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen

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

想象一下，你是一名正在混乱星云中航行的宇宙飞船舰长。你有两个目标：尽可能快地到达目的地，同时保护飞船的外壳不被太空碎片损坏。但问题在于：你开得越快，撞毁的可能性就越大；而你开得越稳，旅程就耗时越长。在计算机科学的世界里，这是一个经典的“规划问题”。我们编写计算机程序来做出决策，但有时这些程序必须处理两种类型的确定性：随机性（比如通过抛硬币来决定路线）和非确定性（程序必须在多个选项中做出选择，但我们还不知道它最终会选择哪一个）。

为了确保这些程序能够正确运行，科学家们使用了一种叫做“谓词转换器”（predicate transformer）的工具。你可以把它想象成一个神奇的水晶球，它能在程序运行之前观察程序，并告诉你预期的结果会是什么。如果你告诉水晶球：“我想知道安全抵达的可能性是多少”，它就会计算出能使安全性最大化的最佳策略。长期以来，这些水晶球一次只能关注一个目标。但在现实生活中，我们很少只想要一件事情；我们想要的是一种平衡。我们想要了解这种权衡：“如果我想快 10%，我会损失多少安全性？”这便是多目标优化的领域，其目标不是寻找一个单一的完美数字，而是一整张关于各种可能折衷方案的地图，被称为帕累托前沿（Pareto front）。

本文介绍了一种专门为这种多目标场景设计的升级版水晶球。作者们（一个计算机科学家团队）开发了一个名为多目标预期望转换器（简称“mop”）的数学框架。这个工具不再只给你一个数字，而是给你一个形状——一个由你可以通过混合不同策略所能达到的所有结果组成的“云团”。它的运作方式就像一本复杂的食谱：它接收一个带有不确定选择的程序，并计算出整个可能的“菜单”，准确展示哪些速度与安全的组合是可实现的，哪些是不可实现的。

论文证明了这个新工具在数学上是严谨的，这意味着即使程序可能会永远运行下去，或者拥有无限个状态，它也能准确反映程序在现实世界中的行为。他们展示了你可以利用这个工具不仅进行结果预测，还可以进行策略合成。换句话说，如果你说：“我想要一个 60% 速度和 40% 安全性的结果”，该系统可以从数学上构建出一个特定的计划（一种“混合确定化”方案）来实现这一目标。这个计划可能涉及在开始时通过抛硬币来决定是在两种不同的纯策略之间进行选择，从而有效地将选择随机化，以达到那个完美的中间地带。

研究人员在几个示例上测试了他们的方法，包括一个试图在不损坏的情况下到达目标的机器人，以及一个试图在赢得奖金的同时不输光所有钱的赌徒。在机器人的例子中，他们展示了最佳策略并不总是“始终快跑”或“始终慢行”。有时，最优的动作是旅程的大部分时间都走得慢，然后在最后阶段冲刺，或者混合这两种方式。论文表明，他们的“mop”工具可以符号化地计算这些复杂的权衡，而无需模拟机器人可能采取的每一条路径。

然而，作者也谨慎地指出，虽然他们可以找到在任何期望点附近“任意接近”的策略，但如果某个点是地图上的“尖锐转角”，且没有任何单一策略能触及该点，那么找到一个能精准命中该点的策略有时是不可能的。在这种情况下，他们能做的就是无限接近。他们还指出，目前的方法最适用于简单的程序，尚未处理递归函数或连续概率分布等复杂特性，这些都是留给未来研究的挑战。

最终，这项工作弥合了高层程序代码与不确定性下决策的复杂数学之间的鸿沟。它提供了一种同时对多个目标进行推理的方法，将“寻找平衡”这一模糊的概念转化为一门精确、可计算的科学。通过将所有可能结果的集合视为一个几何形状，作者为程序员提供了一个全新的视角，去设计那些不仅是安全或快速，而且是实现智能平衡的系统。

技术摘要：概率程序的多元目标前期望推理

问题陈述

具有非确定性的概率程序对建模规划与控制问题至关重要，其中策略（或控制器）必须解决非确定性选择以优化预期结果。虽然经典方法侧重于优化单个量（例如预期燃料水平或终止概率），但许多现实世界的场景需要同时优化多个通常相互冲突的目标（例如在最大化成功概率的同时最小化资源消耗）。

在多目标设定中，提高一个目标往往会导致另一个目标的下降。最优权衡集合由帕累托前沿（Pareto front）来刻画。现有的马尔可夫决策过程（MDP）中的多目标优化方法大多局限于有限状态模型。然而，概率程序通常会诱导出无限状态的 MDP。此外，目前缺乏一种能够进行演绎的、程序级的演算，能够在不借助显式状态枚举的情况下，同时对多个期望进行推理、合成策略并处理无限状态空间。

本文解决了以下三个核心问题：

Q1： 给定一个程序，其同时可实现的取值元组集合（即多目标前期望）是什么？是否可以通过一种可机械化实现的程序级演算来计算？
Q2： 给定一个可实现的目标权衡，如何合成一个实现该目标的程序细化（策略）？
Q3： 这些程序级构造如何与（可能是无限状态的）多目标 MDP 理论建立联系并对其进行扩展？

方法论

作者开发了一种多目标前期望变换器（记作 mop），它在程序层面运行。这种方法扩展了经典的弱最期望（wp）演算，以处理期望向量。

1. 多目标前期望变换器 (`mop`)

其核心创新是将一组后期望元组 $(f_1, \dots, f_n)$ 映射为一组同时可实现的值。

定义域： 该变换器作用于 $\mathbb{R}_{\ge 0}^n$ $R_{\geq 0}^{n}$ 的凸 Hoare 幂集（convex Hoare powerdomain）。该幂集的元素是满足以下条件的 $\mathbb{R}_{\ge 0}^n$ $R_{\geq 0}^{n}$ 子集：
- 非空性： 始终包含零向量。
- 向下封闭性： 如果一个值向量是可实现的，那么任何被其支配的向量也是可实现的。
- 凸封闭性： 通过混合策略（在确定性实现之间进行随机化）可以实现其结果的任何凸组合。
- Scott 封闭性： 捕捉“几乎可实现”的点（可实现点序列的极限），确保了在实现可能无法通过单一策略达到的无限状态系统中具有完备性。
语义： 变换器根据程序结构（skip、赋值、顺序复合、概率选择、受保护的非确定性选择以及循环）进行归纳定义。
- 对于受保护的非确定性选择，mop 在幂集中取逐点上确界（pointwise supremum），这对应于各分支的 Scott 封闭且凸封闭的并集。
- 对于循环，mop 被定义为特征函数的最小不动点（lfp），由于变换器的 $\omega$ -连续性，该不动点保证存在。

2. 通过标量化进行策略合成

为了合成实现帕累托前沿上特定点的策略（即确定化），作者采用了**标量化（scalarization）**技术：

加权和： 一个权重向量 $w$ 将多个目标组合成单个标量期望 $w \cdot f$ 。
规约： 将寻找特定权衡下的策略问题规约为寻找加权和目标的最优策略问题。现有的单目标程序化策略合成技术（例如 [Batz et al. 2024a]）可用于寻找最大化 $w \cdot f$ 的纯确定化 $C_w$ 。
混合确定化： 由于单一的确定性策略可能无法实现帕累托前沿上的所有点（特别是对于非暴露点），作者引入了混合确定化（mixed determinizations）。这些程序通过执行初始硬币投掷来在不同的纯确定化之间进行选择。研究表明，可实现点的集合是这些纯确定化结果的凸包的闭包。

3. 循环推理与终止

论文提供了使用不变式进行循环推理的规则：

上界： 通过使用超不变式（superinvariants）进行 Park 归纳得出。
下界： 在特定的终止条件下使用下不变式（subinvariants）得出：
- 恶魔式几乎确定终止 (dAST)： 每一个非确定性的解析都以概率 1 终止。
- 恶魔式确定终止 (dCT)： 所有执行都在有限步数内终止。
- $\omega$ -不变式： 一种追踪展开深度的不变式序列，适用于没有终止假设的情况，但需要无限多个证明义务。

4. 操作对应关系

作者在程序级的 mop 变换器与作为可数状态、有限动作 MDP 的概率程序操作语义之间建立了严谨的联系。

他们在用于 MDP 的凸 Hoare 幂集上定义了一个广义的 Bellman 算子。
他们证明了 mop 变换器恰好与该 Bell 算子的最小不动点一致，从而刻画了几乎可实现的预期奖励向量集合。这一对应关系在不假设有限状态空间的情况下依然成立。

核心贡献

多目标前期望变换器： 引入了 mop，这是一个在凸 Hoare 幂集上定义的良定义、单调且 $\omega$ -连续的变换器，它保守地将弱最期望扩展到了多目标设定。
基于不变式的推理： 将基于不变式的循环推理提升到多目标设定，提供了用于上界和下界的规则，包括精确性条件（dAST/dCT）。
策略合成： 开发了合成见证策略的规则。论文表明，虽然纯确定化可能不足以覆盖所有帕累托最优点，但混合确定化（在纯确定化之间进行随机化）可以实现属于可实现集之 Scott 封闭凸包内的任何点。
操作完备性： 证明了 mop 变换器与操作 MDP 语义上的广义 Bellman 算子之间存在精确对应。这推广了以往仅限于有限状态的多目标 MDP 验证结果。
案例研究： 将该机制应用于三个案例研究：
- 机器人 (Robot)： 风险与速度的权衡，展示了帕累托前沿的计算与混合策略的合成。
- 赌场 (Casino)： 具有无界奖励的赌博场景，展示了使用 $\omega$ -不变式和 dAST 进行推理。
- 队列 (Queue)： 一个自适应服务器系统，展示了该框架如何在变化的参数环境下符号化地刻画权衡。

结果与意义

论文声称 mop 为无限状态 MDP 上的多目标优化提供了一种符号化的、程序级的处理方法。

完备性： 该变换器精确地捕捉了“几乎可实现”的点集。帕累托前沿被识别为该集合的边界。
合成能力： 该框架允许机械地构造实现特定权衡的策略（确定化），前提是目标点是“暴露的”（可通过加权和进行优化）或者可以通过此类点进行逼近。对于非暴露点，论文指出虽然通过单一加权和进行精确合成可能会失败，但该点可以用暴露点进行任意精度的逼近（Straszewicz 定理）。
局限性： 作者谦虚地指出，验证存在精确最优确定性的充分条件（可实现集的 Scott 封闭性）并不总是容易。此外，目前的框架局限于简单的命令式语言 (pGCL)，尚未支持过程（procedures）、递归、堆操作或连续分布。折扣奖励或长期平均等目标也超出了目前的范围。

总之，这项工作架起了演绎程序验证与多目标 MDP 理论之间的桥梁，提供了一种统一的演算，用于对具有非确定性的概率程序中的权衡进行推理，即使是在无限状态的设定下。