🤖 AI

dtControl2+ $\varepsilon$ : Trading Optimality for Explainability in MDPs via Decision Trees

本文介绍了 dtControl2+ $\varepsilon$ ，它是最先进工具 dtControl2 的一种扩展，通过以可控的优化程度（ $\varepsilon$ ）换取增强的可解释性，为马尔可夫决策过程生成显著更小且更具人类可理解性的决策树控制器。

原作者： Tereza Kinská, Jan Křetínský, Tobias Meggendorfer, Sabine Rieder, Maximilian Weininger

发布于 2026-07-29

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Tereza Kinská, Jan Křetínský, Tobias Meggendorfer, Sabine Rieder, Maximilian Weininger

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

想象一下，你正在试图教一个机器人如何通过迷宫。在计算机科学领域，这被称为“控制器合成”（controller synthesis）。你给机器人一套规则和一个目标，然后计算机程序会计算出到达那里的完美路径。但问题在于：对于复杂的迷宫，计算机通常会吐出一份庞大且混乱的指令列表——为机器人可能踏足的每一个方格都准备一份指令。这就像一本拥有百万页的食谱，而每一页仅仅是在说“左转”或“右转”，针对的是极其微小的特定瞬间。虽然这份列表在数学上是完美的，但人类根本无法阅读，更无法理解。如果机器人撞车了，没人能通过查看那份巨大的列表并说：“啊，我明白了，它是因为对红色的墙感到困惑才左转的。”我们需要这些指令是简短、简单且可解释的，就像一张清晰的地图，而不是一张巨大的电子表格。

这就是“决策树”（decision trees）发挥作用的地方。把决策树想象成一个流程图或是一个“二十个问题”的游戏。你不再拥有一个巨大的列表，而是一个简单的结构：“如果左边有墙，就向右走；否则，直走。”这些规则让人们更容易理解。然而，如果机器人面临棘手的状况或罕见的“极端情况”，即使是这些决策树也可能会变得过于庞大和复杂。研究人员提出的核心问题是：我们能否在不让机器人撞车的前提下，让这些树变得更小、更简单？答案在于一个概念——“ $\epsilon$ -最优性”（ $\epsilon$ -optimality）。想象一下你告诉机器人：“你不必做到100%完美，你可以做到99.9%完美。”这种允许微小误差的空间，给了机器人（以及计算机）忽略微小且不太可能发生的细节的自由，从而产生一套更短、更简洁且依然能安全完成任务的指令集。

论文《dtControl 2+ $\epsilon$ : 通过决策树在 MDP 中以最优性换取可解释性》介绍了一个名为 dtControl 2+ $\epsilon$ 的新工具，它正是为此而设计的。研究人员利用马尔可夫决策过程（Markov Decision Processes，一种描述具有随机性系统——例如机器人可能会在湿滑地面上打滑——的高级数学方法）进行研究，他们构建了一个系统，可以将复杂的、完美的控制器压缩成一个微小的、人类可读的决策树。他们实现这一点的手段是允许一个微小的、受控的误差（称为 $\epsilon$ ）。

以下是他们的“魔法”是如何运作的：该工具不再试图解释机器人的每一个动作，而是观察地图并询问：“哪些动作才是真正重要的？”如果机器人在某个位置几乎肯定永远不会去，或者无论它做什么动作结果都一样，该工具就会说：“让我们跳过解释这部分内容。”它将控制器提炼到了其“本质”。例如，在一次关于机器人在山坡上的测试中，完美的控制器拥有数十条复杂的规则。而这个允许仅为 0.001 误差的新工具，将指令缩减到了仅有 5 个节点（即决策点）。最终生成的规则非常优美且简单：“向上走到顶端，向右走到边缘，然后向下走。”它在每一个微观场景下并非数学意义上的完美，但它已经足够接近完美，以至于差异可以忽略不计，而且人类可以在几秒钟内理解它。

团队将他们的工具与其它最先进的方法进行了对比测试，发现它取得了巨大的进步。在许多情况下，他们的工具生成的决策树比竞争对手的工具要小几个数量级。事实上，在他们运行的近一半测试案例中，通过允许一个微小的误差 $\epsilon = 10^{-2}$ (0.01)，他们成功地将整个控制器压缩到了单个节点。这意味着机器人只需要选择一个主要动作，如果该动作不可行，则随机选择任何其他可用动作，其表现仍会几乎等同于复杂的完美策略。这是之前的工具完全忽略的事实。

研究人员谨慎地指出，他们并非凭空猜测；他们使用了一个强大的模型检查器（一种用于数学验证系统是否正常工作的工具）来反复核实每一个简化后的决策树。他们证明了即使进行了如此激进的简化，机器人的性能也绝不会低于设定的安全限度。他们还展示了该工具适用于各种类型的目标，不仅是到达目的地，还包括规避危险或收集奖励。

简而言之，这篇论文展示了一种用微小的、可控的数学完美性来换取巨大的人类理解能力的途径。通过让计算机承认它不需要解释每一个细微的细节，研究人员创造出了不仅安全有效，而且小到可以印在明信片上、简单到可以用几句话向朋友解释清楚的控制器。它将一本令人困惑的、百万页的说明书，变成了一份清晰的三步指南。

技术摘要：dtControl2+ε：通过决策树实现马尔可夫决策过程（MDP）中交易最优性的可解释性

问题陈述

马尔可夫决策过程（MDP）的控制器综合通常会产生以大型、无结构状态-动作表形式表示的最优控制器。虽然这些表格在数学上是精确的，但它们在资源受限的设备上难以实现，且缺乏可解释性，从而阻碍了验证与认证。现有工具（如 dtControl2）试图将这些控制器表示为决策树（DT），以提高可解释性。然而，对于大型系统或存在许多极端情况的情况，即使是这些决策树也可能变得过于复杂，难以被人理解。

减少决策树规模是一个非平凡的任务；移除一个关键决策可能会导致控制器失效。此外，许多可扩展的综合方法仅提供 $\epsilon$ -最优 控制器（性能在最优值 $\epsilon$ 范围内），而现有的决策树构建工具通常旨在实现精确（ $\epsilon=0$ ）表示，未能利用允许的不精确性来简化解释。

方法论

本文介绍了 dtControl2+ $\epsilon$ ，该工具通过引入“ $\epsilon$ ”功能扩展了最先进的 dtControl2。其核心工作流与概率模型检查器 Storm 紧密集成，以构建更小、更具可解释性的决策树，同时保证生成的控制器保持 $\epsilon$ -最优。

该方法分为三个步骤：

1. 模型求解与数据集构建

该工具不是从确定性的最优控制器开始，而是生成一个初始的**许可型（permissive）数据集（将状态映射到允许的动作集合）或组合型（combined）**数据集（将许可型动作限制在可达状态内）。

许可策略： 工具会识别最优或产生相同值的动作，允许决策树对状态进行“统一”。
简化启发式： 在学习决策树之前，工具会识别并移除那些特定动作选择不会影响结果，或者引入的误差被 $\epsilon$ $ϵ$ 所限制的状态。关键的简化技术包括：
- AllOpt： 移除所有可用动作均为最优的状态。
- Agency（能动性）： 移除最佳与最差可能结果之差小于 $\epsilon$ 的状态。
- Dominance（支配性）： 移除无论做出何种一致性控制器的选择，都几乎必然会被到达的状态。
- Unreach（不可达）： 移除在任何一致性控制器下均无法从初始状态到达的状态。

2. 决策树学习

该工具采用了一种改进的标准基于启发式的决策树构建算法（算法 1），并进行了多项增强：

谓词提取： 自动从高层模型描述（例如 PRISM 语言的转换守卫）中提取相关的谓词，改进了以往工具采用的半自动模板方法。
不纯度度量： 引入了针对模型的特定权重进行不纯度计算。它不再使用均匀权重，而是使用：
- Imp_Simulation： 根据访问频率对状态进行加权（设有安全底线以确保 $\epsilon$ -最优性）。
- Imp_Agency： 根据状态的能动性（潜在误差）进行加权。
- Imp_CoE (误差代价)： 根据在该特定状态下选择最差动作的影响进行加权。
带有验证的激进启发式： 该工具采用了 早停（Early-Stopping）（当不纯度低于阈值时终止分裂）和 贪婪剪枝（Greedy Pruning）（折叠子树）。与以往可能面临可靠性风险的“激进”方法不同，dtControl2+ $\epsilon$ 使用 Storm 在这些步骤后验证 $\epsilon$ -最优性。如果违反了精度约束，工具会放宽启发式规则并重试。

3. 验证循环

该工具的一个独特之处是与 Storm 进行紧密耦合以进行构建后验证。工具会检查生成的决策树的精度。如果与最优值的偏差超过 $\epsilon$ ，它会回溯并降低启发式规则的激进程度（例如，增加停止阈值或禁用剪枝），从而确保最终输出保证是 $\epsilon$ -最优的。

核心贡献

dtControl2+ $\epsilon$ 工具： 一个自包含的工具，通过扩展 dtControl2 来构建更小的决策树，利用了允许的不精确性 $\epsilon$ 。
安全 vs. 激进启发式： 一个清晰地将“安全”简化（其定义上保留了 $\epsilon$ -最优性）与“激进”启发式（通过模型检查进行验证）区分开来的框架。
自动谓词提取： 一种直接从模型转换守卫中导出决策谓词的方法，消除了对人工选择谓词领域知识的需求。
支持多样化目标： 该方法涵盖了标准目标（可达性、安全性、到达-规避、基于奖励的目标），并且独特地支持通过处理基于记忆的控制器来实现 线性时序逻辑 (LTL) 属性。

结果

作者在 38 个基准测试（包括包含高达 500,000 个状态的 PRISM 模型）上，将 dtControl2+ $\epsilon$ 与 dtControl2、dtPaynt、dtNESt 以及 CAV15 方法的重新实现进行了对比评估。

规模缩减： 即使对于精确表示（ $\epsilon=0$ ），由于改进了初始数据集和安全启发式，dtControl2+ $\epsilon$ 产生的决策树也比 dtControl2 小几个数量级。
$\epsilon$ 的影响： 当允许 $\epsilon = 10^{-2}$ 时，该工具为近一半的基准测试生成了单节点决策树，这表明单个动作（配合均匀随机回退）通常足以实现 $\epsilon$ -最优性。
对比：
- vs. dtControl2： dtControl2+ $\epsilon$ 始终产生更小的树。
- vs. dtPaynt： dtPaynt 在大多数基准测试中超时，并在成功时产生了较大的树。
- vs. dtNESt： dtNESt 是 $\epsilon=0$ 时的强力竞争者，但 dtControl2+ $\epsilon$ 在 38 个基准测试中的 23 个中产生的树大小至多只有其一半，在 10 个中甚至小了一个数量级。值得注意的是，当 $\epsilon > 0$ 时，dtNESt 通常会失败或产生更大的树，而 dtControl2+ $\epsilon$ 则擅长利用不精确性。
可扩展性： 该工具在 20 分钟的超时时间内解决了除一个之外的所有基准测试，证明了其在大型复杂模型上的可行性。

意义

论文声称，dtControl2+ $\epsilon$ 代表了可解释控制器综合领域的重大进步。通过用可控的最优性损失换取紧凑性，该工具能够生成以前过于复杂而无法解释的人类可理解控制器。其自动导出结构化见解（例如，识别出单个规则足以实现 $\epsilon$ -最优性）的能力以及对 LTL 属性的支持，使其区别于现有工具。作者强调，与以往可能损害正确性的基于启发式的剪枝方法不同，他们的方法提供了 $\epsilon$ -最优性保证。