POMDP策略合成：通过学习融合采样与模型检测

# 综合 POMDP 策略：通过学习实现采样与模型检验的结合 来源：https://arxiv.org/html/2605.14440 11institutetext:南洋理工大学, 新加坡 11email:[email protected] 22institutetext:塔塔基础研究学院, 印度孟买 22email:[email protected] 33institutetext:布鲁塞尔自由大学, 比利时布鲁塞尔 33email:{prince.mathew,jean-francois.raskin}@ulb.be 44institutetext:IITB 可信赖实验室, 计算机科学与工程系, 印度孟买印度理工学院 44email:[email protected] Anirban Majumdarhttps://orcid.org/0000-0003-4793-1892 Prince Mathewhttps://orcid.org/0000-0001-6410-1474 Sayan Mukherjeehttps://orcid.org/0000-0001-6473-3172 Jean-François Raskinhttps://orcid.org/0000-0002-3673-1097 ###### 摘要 部分可观察马尔可夫决策过程 \(POMDP\) 是不确定环境下决策制定的标准框架。虽然基于采样的方法具有良好的可扩展性，但它们缺乏形式化的正确性保证，因此不适用于安全关键应用。相反，形式化综合技术提供了“通过构造保证正确性”的优势，但通常难以扩展，因为一般的 POMDP 综合问题是不可判定的。为了弥合这一差距，我们提出了一种综合框架，该框架整合了采样、自动机学习和模型检验。受 Angluin 的 \(L^{*}\) 算法的启发，我们的方法利用采样作为成员资格预言机，利用模型检验作为等价性预言机。这使我们能够在采样诱导的策略是正则的前提下，综合出具有形式化保证的有限状态控制器。我们为这个框架建立了一个相对完备性结果。我们原型实现的实验结果表明，该方法成功解决了现有形式化综合工具难以处理的阈值安全问题。我们相信，我们的算法可以作为组合方法中的一个有价值的组成部分，以应对 POMDP 综合问题固有的难度。 ## 1 引言 部分可观察马尔可夫决策过程 \(POMDP\) 是在不确定性和部分可观察性下进行决策制定的基本模型。它们形式化了一系列广泛的现实世界控制问题，其中环境随机演化，而控制器只能接收到对底层状态的间接、有噪声或不完整的观察。因此，它们在机器人学、规划和人工智能等领域得到了广泛研究，并为在复杂和不确定环境中制定反应式控制器综合问题提供了一个强大的框架。 尽管 POMDP 具有强大的表达能力和实际重要性，但用于 POMDP 中控制器综合的工具支持仍然有限。这主要是由于该模型固有的算法复杂性。即使是与综合相关的最基本决策问题——是否存在一个控制器，能以高于给定阈值的概率确保安全性 \(*即*，避免坏状态\)——通常是不可判定的 \[28 (https://arxiv.org/html/2605.14440#bib.bib10)\]，从而排除了完全算法解决方案的可能性。因此，大多数实际方法依赖于基于采样的技术，例如蒙特卡洛树搜索 \(MCTS\) \[24 (https://arxiv.org/html/2605.14440#bib.bib33)\] 及其变体。这些方法具有可扩展性，并且在实际中通常能产生高质量的策略，但它们不提供静态的正确性保证，因此不适用于安全关键应用。此外，当这类技术引入不可接受的运行时开销时，它们在实际部署中可能具有挑战性。 相比之下，形式化方法通过静态 \(*即*，部署前\) 综合技术和逻辑规约语言提供了“通过构造保证正确性”，但通常无法扩展到具有现实尺寸或复杂度的 POMDP。在这项工作中，我们提出通过一种受 \(L^{*}\) 算法 \[4 (https://arxiv.org/html/2605.14440#bib.bib6)\] 启发的学习技术，将基于采样的方法与形式化方法结合起来，从而弥合两者之间的差距。我们将我们的框架称为*基于反例指导的策略学习*\(Cplus\)。这里的关键见解是，基于观察的策略的综合可以被构建为一个学习问题。用 \(L^{*}\) 的术语来说，Cplus 使用了成员资格查询——称为*动作查询*——这些查询由一个*动作预言机* \(O^{A}\) 来回答，该预言机在给定观察和动作的历史后，返回从该位置采取的最优动作。基于采样的 POMDP 分析技术非常适合回答这类查询。这些查询的答案随后被概括以构建假设——表示为 Mealy 机的有限状态控制器 \(FSCs\)。一旦构建了一个假设，它就会被传递给一个*模型检验预言机* \(O^{M}\)，该预言机验证候选控制器是否满足给定的规约——这些被称为*模型检验查询*。如果模型检验预言机验证了该假设，Cplus 就会终止，并提供一个经过验证的解决方案，从而提供形式化方法的强有力保证。否则，它会返回一组违反规约的迹。然后分析这些迹，以识别一个前缀，其中候选控制器与 \(O^{A}\) 存在分歧。这个前缀被称为*反例*，它被纳入 \(如 L^{*}\) 学习算法中以细化假设，然后重复该过程。 虽然单独使用采样工具不提供静态的形式化保证，但在我们的框架中，它被专门用于回答成员资格查询，而正确性完全由后续的模型检验阶段来保证。重要的是，候选策略的模型检验决策问题是可处理的，因为它简化为对一个马尔可夫链——POMDP 与 FSC 的乘积——针对一个无限持续时间安全属性的模型检验。这可以在关于 POMDP 和表示候选策略的 FSC 规模的多项式时间内解决，这与一般综合问题的不可判定性形成了对比。 尽管由于 POMDP 综合的不可判定性，完全完备性是无法达到的，但我们建立了一个*相对完备性*结果。首先，我们证明了有限状态策略总是足以应对*阈值安全目标* \(定理 1 (https://arxiv.org/html/2605.14440#Thmproblem1)\)。然后，我们证明，如果由 \(O^{A}\) 隐式定义的策略既是正确的又是正则的 \(即，能被一个有限状态机识别\)，那么我们的算法保证会终止并产生一个正确的解决方案 \(定理 4 (https://arxiv.org/html/2605.14440#S4.SS0.SSS0.Px4)\)。在这种情况下，我们相比在线执行 \(O^{A}\) 获得了两个重要优势。首先，我们的过程产生的解决方案在部署之前就已经通过构造被认证了。其次，该解决方案采用有限状态控制器的形式，可以高效地部署和在线执行，只需要常数时间的更新——不像在线采样方法，由于其计算开销可能会引入延迟。 为了展示我们方法的潜力，我们使用 Python 实现了 Cplus 的原型。对于动作预言机 \(O^{A}\)，我们依赖于在线规划器 Despot \[40 (https://arxiv.org/html/2605.14440#bib.bib7)\]，它可以按需查询以计算局部最优动作，而无需预先计算完整策略。对于模型检验预言机 \(O^{M}\)，我们的实现使用了 Storm \[20 (https://arxiv.org/html/2605.14440#bib.bib20)\]。该实现是模块化的。特别是，其他规划器——无论是基于采样的，还是基于形式化方法的，如后文所述——都可以用作 \(O^{A}\)。类似地，其他概率模型检验器，如 Prism \[26 (https://arxiv.org/html/2605.14440#bib.bib28)\] 或 Modest \[19 (https://arxiv.org/html/2605.14440#bib.bib1)\]，也可以用作 \(O^{M}\)，而无需修改整体框架。 实验结果是令人鼓舞的。我们的实现（其开发目的是评估该框架的潜力）能够解决对现有形式化方法算法具有挑战性的阈值安全问题。同时，它通过模型检验提供了强有力的形式化正确性保证，这是纯基于采样的方法无法提供的。因此，最终的框架结合了采样、学习和验证，既有坚实的理论基础，又有实际的相关性。然而，由于 POMDP 综合问题的不可判定性，我们的方法应被视为一种补充方法，而非完整的解决方案。特别是，它最适合作为一套互补技术组合的一部分，与基于形式化方法的其他半算法一起使用。 ### 1.0.1 相关工作。 与我们的方法最密切相关的工作是 \[42 (https://arxiv.org/html/2605.14440#bib.bib38)\]。该工作致力于学习 POMDP 中面向有界地平线可达性目标的非确定性 FSC，*即*，在固定步数内以超过给定阈值的概率到达一组状态。与我们方法中考虑的无限地平线属性相比，有界地平线属性对于 POMDP 是可判定的。此外，他们的方法并非旨在解决综合问题，而是计算一个最大允许的策略，之后可以细化为具体的控制器。对允许策略的搜索会导致动作空间的指数级增长，而这在我们的框架中不会发生。他们的方法仅在一个手工制作的示例上进行了说明，并且据我们所知，目前没有可用的实现。 用于策略计算的在线算法包括即时确定策略的树搜索方法。例如，POMCP \[38 (https://arxiv.org/html/2605.14440#bib.bib8)\] 算法将 MCTS 与粒子滤波相结合，而 Despot \[40 (https://arxiv.org/html/2605.14440#bib.bib7)\] 则采用确定性稀疏树来提高可扩展性。这些方法具有良好的可扩展性，但缺乏强大的正确性保证，使其不太适用于安全关键应用。 经典的离线 POMDP 求解器，如 Perseus \[41 (https://arxiv.org/html/2605.14440#bib.bib12)\] 和 SARSOP \[25 (https://arxiv.org/html/2605.14440#bib.bib13)\]，使用基于点的方法 \[34 (https://arxiv.org/html/2605.14440#bib.bib11)\]，这些方法在信念空间的选定子集上近似值函数。另一方面，基于对底层信念 MDP 进行部分探索 \[7 (https://arxiv.org/html/2605.14440#bib.bib15),8 (https://arxiv.org/html/2605.14440#bib.bib16)\] 或抽象 \[32 (https://arxiv.org/html/2605.14440#bib.bib14)\] 的方法已在诸如 Storm \[20 (https://arxiv.org/html/2605.14440#bib.bib20)\] 和 Prism \[26 (https://arxiv.org/html/2605.14440#bib.bib28)\] 等概率模型检验器中实现。 归纳式综合工具，如 Paynt \[3 (https://arxiv.org/html/2605.14440#bib.bib18),2 (https://arxiv.org/html/2605.14440#bib.bib19)\]，通过增量评估候选解决方案来探索控制器空间，但当所需内存大小增加时，它们难以扩展。 \[6 (https://arxiv.org/html/2605.14440#bib.bib17)\] 中描述的算法应用 \(L^{*}\) 学习算法，从使用 Storm 预先计算的策略中综合出一个 FSC。我们的方法在以下两个关键方面不同于他们的方法：\((i)\) 我们不预先计算完整策略，而是在需要时才查询动作预言机，并且 \((ii)\) 我们引入了一种新颖的、基于模型检验器的等价性查询，以确保正确性。 其他方法通过从基于循环神经网络 \(RNN\) 的 POMDP 策略中提取自动机来推导 FSC \[11 (https://arxiv.org/html/2605.14440#bib.bib22)\]，但这些方法不提供形式化保证。 黑盒检验 \[33 (https://arxiv.org/html/2605.14440#bib.bib44),37 (https://arxiv.org/html/2605.14440#bib.bib45)\] 也与我们的方法相关，因为它将自动机学习与验证结合在一个更大的工作流中。然而，在黑盒检验中，对学习到的假设进行正的模型检验结果本身是不够的，因为还必须与底层系统建立一致性。相比之下，在我们的设置中，一旦模型检验器返回真值，综合出的 FSC 就已经是阈值安全问题的认证解决方案。此外，经典的黑盒检验针对的是可表示为 Mealy 机的确定性反应系统，而我们的框架处理的是随机的、部分可观察的 POMDP，其一般的综合问题是不可判定的。 文章中缺失的证明可在附录中找到。 ## 2 预备知识 一个*\(离散\) 概率分布* 在一个可数集合 \(S\) 上是一个函数 \(d: S \to [0,1]\)，满足 \(\sum_{s \in S} d(s) = 1\)。我们将集合 \(S\) 上所有概率分布的集合记为 \(\mathsf{Dist}(S)\)。对于 \(d \in \mathsf{Dist}(S)\)，\(d\) 的*支撑集* 是 \(\mathsf{supp}(d) = \{ s \in S \mid d(s) > 0 \}\)。 ###### 定义 1 \(马尔可夫链\) 一个*马尔可夫链 \(MC\)* 是一个三元组 \(\mathcal{M} = (S, P, s_0)\)，其中 \(S\) 是一个可数状态集合，\(P: S \to \mathsf{Dist}(S)\) 是转移函数，\(s_0 \in S\) 是初始状态。对于状态 \(s, s' \in S\)，\(P(s)(s')\) 表示从状态 \(s\) 一步转移到状态 \(s'\) 的概率，我们将这个概率记为 \(P(s, s')\)。 一个长度为 \(i \ge 0\) 的*有限路径* \(\rho = s_0 s_1 \ldots s_i\) 是 \(i+1\) 个连续状态的序列，使得对于所有 \(t \in [0, i-1]\)，\(s_{t+1} \in \mathsf{supp}(P(s_t))\)。类似地，一个无限路径是状态的一个无限序列 \(\rho = s_0 s_1 s_2 \ldots\)，使得对于所有 \(t \in \mathbb{N}\)，\(s_{t+1} \in \mathsf{supp}(P(s_t))\)。有限路径 \(\rho = s_0 s_1 \dots s_n\) 在 MC \(\mathcal{M}\) 中的概率，记为 \(\mathcal{M}(\rho)\)，由 \(\prod_{i=0}^{n-1} P(s_i, s_{i+1})\) 给出。对于有限路径 \(\rho\)，令 \(\mathsf{Cyl}(\rho)\) 表示所有以 \(\rho\) 为前缀的无限路径 \(\rho'\) 组成的集合。集合 \(\mathsf{Cyl}(\rho)\) 称为 \(\rho\) 的柱形集。对于一组有限路径 \(R\)，我们定义 \(\mathsf{Cyl}(R) = \bigcup_{\rho \in R} \mathsf{Cyl}(\rho)\)。我们用 \(\mathbb{P}_{\mathcal{M}}\) 表示由马尔可夫链 \(\mathcal{M}\) 诱导的无限路径上的概率测度 \(详见，例如 \([5 (https://arxiv.org/html/2605.14440#bib.bib29)]\) 的形式定义\)。直观上，\(\mathbb{P}_{\mathcal{M}}\) 为每个可测的无限路径集合 \(称为*事件*\) 分配一个概率，即 \(\mathcal{M}\) 的执行将遵循该集合中一条路径的概率。 给定两个状态集合 \(\mathsf{Good}, \mathsf{Bad} \subseteq S\)，我们首先将 \(\Diamond \mathsf{Good}\) 定义为最终到达 \(\mathsf{Good}\) 中某个状态的路径集合：\(\Diamond \mathsf{Good} = \{ s_0 s_1 \ldots \mid \exists i \ge 0: s_i \in \mathsf{Good} \}\)。这定义了一个*可达性目标*。我们还定义 \(\Box \neg \mathsf{Bad}\) 为避开 \(\mathsf{Bad}\) 中所有状态的路径集合：\(\Box \neg \mathsf{Bad} = \{ s_0 s_1 \ldots \mid \forall i \ge 0: s_i \notin \mathsf{Bad} \}\)。