将自然语言转为带层级结构的几何时空逻辑，提升机器人操作任务验证能力
NL2SpaTiaL: Generating Geometric Spatio-Temporal Logic Specifications from Natural Language for Manipulation Tasks
- 用分层逻辑树结构解析语义，分离空间关系与时间嵌套
- 在深度嵌套逻辑下准确率超基线模型37.2%，显著提升生成质量
- 首个带层级标注的自然语言到时空逻辑数据集，适合机器人路径验证研究者
时序逻辑虽能严格验证机器人行为，但通常仅作用于轨迹级信号，无法天然表达操作任务中关键的以物体为中心的几何关系。时空逻辑（SpaTiaL）通过显式刻画几何空间约束，成为操作任务验证的理想形式化工具。因此，将自然语言（NL）转化为可验证的SpaTiaL规范是一项关键目标。然而，现有方法将规范视为扁平序列，导致深层嵌套时性能急剧下降。本文提出NL2SpaTiaL，将规范建模为分层逻辑树（HLT），通过单次生成结构化HLT，解耦语义解析与语法生成，契合人类组合式空间推理。我们构建了目前已知首个带有显式层级监督的NL-to-SpaTiaL数据集，基于逻辑优先合成流程。使用开源大模型的实验表明，该方法在多种逻辑深度下显著优于平坦生成基线。结果证明，显式的HLT结构对可扩展的自然语言到时空逻辑转换至关重要，最终实现语言条件机器人中‘生成-测试’范式的严谨验证。
原文摘要 · Abstract (English)
While Temporal Logic provides a rigorous verification framework for robotics, it typically operates on trajectory-level signals and does not natively represent the object-centric geometric relations that are central to manipulation. Spatio-Temporal Logic (SpaTiaL) overcomes this by explicitly capturing geometric spatial requirements, making it a natural formalism for manipulation-task verification. Consequently, translating natural language (NL) into verifiable SpaTiaL specifications is a critical objective. Yet, existing NL-to-Logic methods treat specifications as flat sequences, entangling nested temporal scopes with spatial relations and causing performance to degrade sharply under deep nesting. We propose NL2SpaTiaL, a framework modeling specifications as Hierarchical Logical Trees (HLT). By generating formulas as structured HLTs in a single shot, our approach decouples semantic parsing from syntactic rendering, aligning with human compositional spatial reasoning. To support this, we construct, to the best of our knowledge, the first NL-to-SpaTiaL dataset with explicit hierarchical supervision via a logic-first synthesis pipeline. Experiments with open-weight LLMs demonstrate that our HLT formulation significantly outperforms flat-generation baselines across various logical depths. These results show that explicit HLT structure is critical for scalable NL-to-SpaTiaL translation, ultimately enabling a rigorous ``generate-and-test'' paradigm for verifying candidate trajectories in language-conditioned robotics. Project website: https://sites.google.com/view/nl2spatial
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。