⚡ electrical engineering

Learning Linear Temporal Specifications from Demonstrations with Uncertainty

本文提出了一种从不确定演示中学习最小线性时序逻辑（LTL）规范的新型框架，该框架通过汉明距离对轨迹不确定性进行建模，并将问题转化为伪布尔优化问题，从而在噪声条件下通过恢复地面真值公式的表现优于现有方法。

原作者： Parastou Fahim, Constantino Lagoa, Rômulo Meira-G'oes

发布于 2026-07-14

📖 1 分钟阅读☕ 轻松阅读

原作者： Parastou Fahim, Constantino Lagoa, Rômulo Meira-G'oes

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

想象一下，你正试图通过展示一段“完美的一天”的视频来教一个机器人如何表现。你想让机器人学习这条规则：“如果房间又热又有人，就打开空调。”但问题在于，你录制的视频有故障。也许是传感器闪跳了一下，或者某一帧损坏了，又或者是测量值稍微有点偏差。机器人看到的是一个“几乎正确”的版本，其中包含了一些模糊、不确定的部分。

现有的多数方法都像是严厉的老师，假设视频是完美的。如果视频显示在房间很冷的时候开启了空调，这些方法会感到困惑，甚至会发明一些奇怪、复杂的规则来解释这个错误。它们假设这种错误仅仅是“标签”弄混了（比如把猫误认作狗），但它们没有考虑到视频本身可能是模糊或不完整的。

这篇论文介绍了一种更具包容性的新方法，称为鲁棒 LTL 学习（Robust LTL Learning）。它不再要求视频必须完美，而是说：“好吧，这个视频是模糊的。让我们想象一下所有可能导致这种故障的视频版本。”

“假设”的气泡

作者使用了一个名为**汉明距离（Hamming distance）**的数学工具，在每个有故障的视频周围创建了一个“可能性气泡”。你可以把它想象成一个安全网。如果你的记录视频显示空调在第 3 步开启，但你知道传感器可能偏移了一步，那么该方法就不会只看第 3 步，而是会同时观察第 2 步、第 3 步和第 4 步。它创建了一组“轨迹估计”（trace estimates），即在这一小段误差范围内，这一天实际上可能发生的各种方式。

核心思想是：我们不需要知道这个视频的哪个版本才是真实的。 我们只需要找到一条对于该气泡内“至少一个”版本有效的规则即可。

“群体”规则

在旧的方法中，如果一段视频被标记为“良好行为”，机器人就必须针对该特定视频完美地遵循规则。如果视频有噪声，机器人就会失败。

而在这种新方法中，机器人会观察整个可能的视频群体。它会问：“是否存在这个群体中的某个版本，使得规则成立？”如果答案是肯定的，机器人就会接受它。这就像一名侦探，明知证人对时间的记忆可能有些混乱，但他不会直接把证人排除在外，而是会说：“只要嫌疑人在证人提到的那个时间窗口内的某个时刻出现在建筑内，那么不在场证明就成立。”

结果：深入观察

作者使用了一个**供暖、通风与空调（HVAC）**系统测试了这个想法。他们设定了一个基准规则：“总是，如果房间又热又有人，那么在下一步必须开启空调。”

然后，他们故意弄乱了数据以模拟传感器误差，创建了变量发生变化的“不确定性窗口”。他们将这种新方法与另外两种方法进行了对比：

Flie：一种无法很好处理不确定性的标准方法。
Modified Flie：一种经过微调的版本，试图修复一些问题，但仍然假设数据基本是正确的。

发生了什么？

Flie 通常会完全放弃复杂的基于时间的规则，转而学习一些简单但错误的模式，比如“如果现在不热，那么稍后会热”（这毫无意义）。
Modified Flie 表现稍好，有时能捕捉到部分规则，但它经常把因果关系搞反。它会学到“如果空调开着，那么房间里就有人”，这与事实正好相反。
鲁棒方法（作者的新方法）在大多数情况下都能成功恢复正确的时间结构，但它仍然经常颠倒因果方向。例如，虽然真实的规则是“占用 + 热量 $\rightarrow$ 空调”，但鲁棒方法学到的往往是“空调 $\rightarrow$ 占用”。然而，尽管存在这种反转，它比其他方法更接近预期的系统行为，因为它成功保留了关键的时间关系（如“下一步”）。

然而，这其中存在权衡。论文指出，这种新方法计算起来更慢。在 HVAC 测试中，其他方法耗时约 0.8 到 4.4 秒，而鲁棒方法根据复杂程度，耗时在 6.5 到 73.1 秒之间。这就像机器人在深呼吸并进行更深入的思考，以确保其正确性，而不是仅仅快速做出猜测。

这意味着什么（以及不意味着什么）

该论文明确排除了“我们可以直接忽略噪声或假设数据是完美”的想法。它认为，以往的方法之所以失败，是因为它们将不确定的数据视为简单的标签错误，而非受损的信号。

作者建议，对于传感器易失效的现实应用场景，他们的方法是一个更有前景的方向。他们通过模拟（使用合成数据和 HVAC 案例）表明，该方法所恢复的公式比现有最先进的方法更“接近”真相，即便逻辑并不总是完全完美。

他们并未声称已经彻底解决了这个问题。事实上，他们承认自己的结果是“初步的”。他们还没有证明该方法适用于每一种可能的机器人或现实世界中的每一场灾难场景。他们只是通过这些特定测试表明，观察“可能性气泡”比仅仅观察模糊的视频能让机器人学到更好的规则。

所以，如果你是一个正在构建需要应对故障传感器的机器人的好奇青少年，这篇论文给你的启示是：不要仅仅相信视频。去想象所有可能发生的变化，寻找一个至少符合其中一种可能性的规则，这样你的机器人就不太会因为一个坏像素而撞墙了。

技术摘要：从带有不确定性的演示中学习线性时序规范

问题陈述

本文解决了从系统演示中推断线性时序逻辑（LTL）规范的挑战，这在安全关键领域（如机器人、自动驾驶车辆）中至关重要。现有的学习方法在处理正向和负向轨迹（traces）时，通常假设这些轨迹被正确捕获，仅考虑标签分类错误，而现实世界的数据往往存在轨迹不确定性（trace uncertainty）。这种不确定性源于传感器故障、测量误差、数据丢失或通信延迟，导致轨迹出现损坏、不完整或不一致的情况。

当前的方法将观测到的轨迹视为基准真相（ground truth），当轨迹内容本身具有不确定性时，这些方法无法恢复准确的规范。作者定义了鲁棒 LTL 学习问题（Robust LTL Learning Problem）：即寻找一个能够解释系统行为的最小 LTL 公式，即使在观测轨迹存在有界不确定性的情况下也能保持有效，而不是假设轨迹是完全准确的。

方法论

所提出的框架对轨迹不确定性进行建模，并将其集成到伪布尔优化（Pseudo-Boolean Optimization）问题中。该方法通过以下步骤进行：

1. 轨迹不确定性建模

作者使用**汉明距离（Hamming distance）**来量化观测轨迹与潜在“正确”轨迹之间的不确定性。

轨迹估计组 ( $C^k_{tr}$ )：给定一个观测轨迹 $tr $和一个不确定性界限$ k $，轨迹估计集包括所有与$ tr $的汉明距离在$ k$ 以内的轨迹。
假设：假设真实的系统行为是该不确定性组中的某一个轨迹，而不一定是观测到的轨迹本身。

2. 鲁棒学习公式化

学习问题被重新表述为处理这些“组”而非单个轨迹：

组分类错误：框架不再要求每个观测轨迹都满足公式，而是要求每个不确定性组中至少有一个轨迹（对于正向轨迹）满足该公式，且至少有一个来自负向不确定性组的轨迹不满足该公式。
损失函数：定义了一个组分类错误损失函数 $\ell_g$ 。它惩罚那些没有任何轨迹在不确定性组内与所学公式保持一致的情况。

3. 算法实现（伪布尔优化）

该问题被编码为一个命题公式 $\Phi$ ，并使用 Max-SMT（具体为伪布尔优化）进行求解。该公式由四类约束组成：

语法约束 ( $\Phi_{syn}$ )：确保学习到的公式符合有效的 LTL 语法（以语法树的形式表示）。
语义约束 ( $\Phi_{sem}$ )：编码轨迹与 LTL 公式之间的满足关系。
选择约束 ( $\Phi_{sel}$ )：引入二值变量 $z_{tr}$ 来选择用于学习的特定轨迹估计。如果选择了某个轨迹（即 $z_{tr}=1$ ），则该轨迹必须满足（或不满足）公式。
组约束 ( $\Phi_{grp}$ )：一种软约束，强制要求对于每一个观测到的轨迹，其不确定性组中必须至少选择一个轨迹估计（即 $z_{tr'}=1$ ）。

目标是最小化组分类错误损失（按轨迹数量加权），同时满足所有硬约束。这通过最小化一个伪布尔目标函数来解决。

核心贡献

新颖的问题表述：本文引入了“鲁棒 LTL 学习问题”，明确解决了轨迹内容（损坏/不完整）引起的不确定性，而不仅仅是标签噪声。
不确定性建模：利用汉明距离来定义轨迹估计组，使系统能够考虑任何给定观测值背后的一系列可能的“真实”行为。
基于组的约束：框架强制要求每个不确定性组中至少有一个轨迹必须与学习到的公式保持一致，从而防止学习算法被损坏的数据点误导。
优化方法：将鲁棒学习问题归约为等价的伪布尔优化问题，可通过 SMT 求解器（如 Z3）求解。

实验结果

作者使用两个基准测试对该方法进行了评估，对比对象是现有的基于 SAT 的学习方法（特别是 “Flie” 算法及其结合了用户约束的 “Modified Flie” 变体）：

HVAC 控制系统：一个真实的场景，包含温度、占用情况和空调状态的原子命题。
合成 LTLf 模式：使用注入了不确定性的各种基准真相 LTL 公式进行的实验。

研究发现：

准确性：与现有方法相比，所提出的鲁棒学习方法恢复出的规范更接近基准真相公式。
时序关系：标准方法（Flie）在不确定性下往往无法捕捉时序依赖关系或学习到伪关系；而 Modified Flie 虽然能部分恢复关系，但经常反转因果方向；相比之下，鲁棒方法能够一致地保留关键的时序结构（例如全局条件和直接依赖关系）。
计算成本：鲁棒方法比基准方法需要更多的计算时间。作者将其归因于伪布尔优化相比于标准 Max-SAT 具有更高的复杂度。

重要性与主张

本文声称其框架弥合了理论 LTL 学习与实际应用场景之间的鸿沟，在实际应用中数据往往是不完美的。通过在规范学习过程中有效地捕捉不确定性，该方法能够推导出最小且具有可解释性的 LTL 公式，即使在输入轨迹存在噪声或不完整的情况下，也能反映真实的系统行为。

作者将这项工作定位为迈向更鲁棒的形式验证和安全关键系统控制器综合的重要一步。他们也谦虚地指出，虽然目前的结果仍处于初步阶段，但与假设轨迹完整性的现有最先进方法相比，该方法提供了一个“更具原则性且更有前景的方向”。未来的工作方向被确定为开发形式化的距离度量，以便定量地比较学习到的规范与基准真相。