Recent advances in the development of robotic foundation models have led to promising end-to-end and general-purpose capabilities in robotic systems. Trained on vast datasets of simulated and real-world trajectories, these policies map multimodal observations directly to action sequences for physical execution. Despite promising real-world capabilities, these models are still data-driven and, therefore, lack explicit notions of behavioral correctness. We address this gap by introducing SafeDec, a constrained decoding framework for autoregressive, transformer-based robot navigation foundation models that enforces safety specifications expressed as Signal Temporal Logic (STL) formulas. Our method ensures that generated actions provably satisfy STL specifications under assumed dynamics at runtime without retraining while remaining agnostic of the underlying policy. We evaluate SafeDec on tasks from the CHORES benchmark for state-of-the-art embodied navigation policies across hundreds of procedurally generated environments and show that our decoding-time interventions are useful not only for filtering unsafe actions but also for conditional action generation. Videos are available at constrained-robot-fms.github.io

翻译：近期机器人基础模型的发展使机器人系统具备了令人瞩目的端到端通用能力。这些策略通过海量仿真与现实世界轨迹数据集训练，能够将多模态观测结果直接映射为物理执行的动作序列。尽管展现出强大的现实世界应用潜力，但这些模型仍为数据驱动型，缺乏对行为正确性的显式概念。为弥补这一缺陷，我们提出SafeDec——面向自回归、基于Transformer的机器人导航基础模型的约束解码框架，该框架能够实施以信号时序逻辑（STL）公式表达的安全规范。该方法可在运行时确保生成动作在假设动力学条件下可证明地满足STL规范，无需重新训练且与底层策略无关。我们在CHORES基准测试的系列任务上评估SafeDec，覆盖数百个程序化生成环境中的最先进具身导航策略，结果表明我们的解码时干预不仅可用于过滤不安全动作，还能进行条件性动作生成。视频资料见constrained-robot-fms.github.io