STeP：信号时态逻辑，用于通过视觉语言模型生成动作的精确规范

自然语言机器人指令通常指定的不仅仅是粗略的任务目标：它们可能会施加在整个执行过程中必须保持满足的空间、时间和逻辑要求。我们提出了 STeP，一种基于规范的代理框架，它使用信号时态逻辑（STL）作为高层语言推理和底层机器人执行之间的显式接口。 STeP 不是将这些要求隐式编码在学习策略中，而是将它们形式化为任务规范，可以跨多阶段操作进行分解、在执行期间强制执行、在线监控，并用作重新规划的结构化反馈。我们在标准 LIBERO 和 LIBERO-PRO 上评估 STeP，并引入 LIBERO-Constrained，这是一个针对具有空间、时间和逻辑要求的操作任务的新基准，以及现实世界的桌面实验。在 LIBERO-PRO 上，STeP 在六种评估的扰动设置中的五种中保持了 54%-89% 的成功率，在分布偏移下大大优于 VLA 和代码即策略基线。在 LIBERO-Constrained 上，STeP 在 49 个任务约束实例中实现了 80% 的安全成功率；在现实世界的任务中，它在所有四个任务类别中比无规范的基于模型的基线提高了安全成功率，增幅高达 45 个百分点。这些结果支持明确的形式规范作为基础模型推理和可靠的机器人执行之间的实用接口。