Learning GR(1) Specifications from Traces

想象一下，你正试图教会一个机器人如何行为，但你无法写下规则，因为你并不知道规则是什么。相反，你有一台摄像机正在记录这个机器人。你向摄像机展示许多机器人表现出色的片段（“好”的轨迹）以及许多它发生碰撞或表现异常的片段（“坏”的轨迹）。你的目标是编写一本规则手册，完美地将好的片段与坏的片段区分开来。这就是**规范挖掘（specification mining）**的世界：通过挖掘数据来寻找支配系统的隐藏规律。

但问题在于，在现实世界中，像自动驾驶汽车或工厂机器人这样的系统不仅仅是遵循规则；它们会对环境做出反应。如果环境（比如雨中的道路或按下按钮的人类）做了某些事情，系统必须做出响应。这被称为反应式系统（reactive system）。为了让这些系统保持安全，计算机科学家使用一种特殊的逻辑，称为 GR(1)。把 GR(1) 想象成一份严格的合同：“如果环境承诺表现良好（假设），那么系统就承诺履行其职责（保证）。”如果你正确制定了这份合同，你就可以自动构建出一个在数学上保证能够工作的机器人。如果你制定错了，机器人可能会失败，或者更糟的是，数学会判定这个机器人是无法构建的，而实际上它是可以构建的。

寻找正确的合同是非常困难的。现有的工具通常试图通过查看逻辑语言中所有可能的句子来猜测规则。这就像是在试图通过检查宇宙中每一根稻草来寻找一根特定的针。这需要耗费极长的时间，而且这些工具给出的规则看起来可能还不错，但实际上是一个陷阱——它虽然区分了好的片段和坏的片段，但它是一个机器人永远无法真正遵循的规则。

这正是这篇论文的意义所在。由 Sam Nicholas Kouteili 及其团队领导的研究人员开发了一个名为 GR1MINE 的新工具。GR1MINE 不再进行随机猜测，它预先知道合同的形状。它知道 GR(1) 规则的骨架：“如果环境做 X，那么系统必须做 Y。”它只需要弄清楚 X 和 Y 到底是什么。

为了实现这一点，他们使用了一个巧妙的技巧，涉及到一个“SAT 求解器（SAT solver）”，它就像一个超快速的解谜器。想象一下你正在尝试搭建一座乐高城堡，但你不知道该使用哪些积木。与其搭建一整座城堡、进行测试，然后再拆掉重来，GR1MINE 会先搭建出城堡的框架。然后，它会在这个框架内尝试不同的积木组合。如果某种组合失败了，求解器会记住为什么失败，并利用这段记忆瞬间跳过成千上万种其他错误的组合。这被称为“增量求解（incremental solving）”。

该团队在取自现实世界硬件和机器人挑战的 120 个不同谜题（基准测试）上测试了他们的工具。结果令人震惊。当谜题由标准的 GR(1) 规则组成时，GR1MINE 解决了全部 60 个 中的 60 个。相比之下，之前的最优工具只能解决大约一半或三分之一。更令人印象深刻的是，在这些特定谜题上，GR1MINE 的速度比通用工具快了 30 多倍。

但真正的魔力发生在他们测试那些并非完美 GR(1) 规则的谜题时。即使原始规则很混乱且不符合整齐的模板，GR1MINE 仍然设法为 60 个这类混乱案例中的 38 个 找到了一个可实现的有效规则。其他工具则表现挣扎，只能找到极少数有效的规则，而且它们找到的规则往往是“不可实现的（unrealizable）”——意味着在数学上机器人无法遵循。

简而言之，GR1MINE 不仅仅是寻找一条区分好与坏的规则；它寻找的是一条机器人可以真正遵循的规则。通过坚持 GR(1) 的已知结构并使用智能记忆技巧来避免重复劳动，该团队证明了我们可以比以前更快、更可靠地自动发现复杂的、安全的机器人合同。他们不仅是在干草堆里找针，他们还制造了一块只吸引正确针头的磁铁。