T3 Planner: A Self-Correcting LLM Framework for Robotic Motion Planning with Temporal Logic

📄 arXiv: 2510.16767v1 📥 PDF

作者: Jia Li, Guoxiang Zhao

分类: cs.RO

发布日期: 2025-10-19

🔗 代码/项目: GITHUB

💡 一句话要点

T3 Planner：基于自校正LLM的机器人时序逻辑运动规划框架

🎯 匹配领域: 支柱一：机器人控制 (Robot Control) 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 机器人运动规划 大语言模型 时序逻辑 形式化验证 自我校正

📋 核心要点

  1. 现有机器人运动规划方法依赖领域专家定制规划器，难以处理时空耦合约束，导致运动不可行或任务规划与运动执行不一致。
  2. T3 Planner利用LLM进行高层语义推理，并通过信号时序逻辑(STL)验证器进行自我校正，确保生成满足复杂约束的可行运动规划。
  3. 实验表明，T3 Planner在不同场景下显著优于现有方法，并且可以通过蒸馏技术部署到轻量级模型中。

📝 摘要（中文）

本文提出了一种基于LLM的机器人运动规划框架T3 Planner，该框架能够通过形式化方法进行自我校正。T3 Planner通过三个级联模块分解时空任务约束，每个模块驱动LLM生成候选轨迹序列，并使用信号时序逻辑(STL)验证器检查其可行性，直到找到满足复杂的空间、时间及逻辑约束的轨迹。实验结果表明，T3 Planner显著优于基线方法。所需的推理能力可以提炼到一个轻量级的Qwen3-4B模型中，从而实现高效部署。所有补充材料可在https://github.com/leeejia/T3_Planner获取。

🔬 方法详解

问题定义：机器人运动规划旨在将自然语言指令转化为可执行的运动轨迹。现有方法通常需要领域专家进行定制，且难以处理复杂的时空约束，容易导致规划出的运动轨迹不可行，或者任务规划与实际运动执行之间存在偏差。LLM虽然擅长高层语义推理，但其幻觉问题可能导致生成不可行的运动规划。

核心思路：T3 Planner的核心思路是利用LLM的语义理解能力生成候选轨迹，并结合形式化方法（STL验证器）对轨迹进行验证和校正，从而确保生成的运动规划既符合自然语言指令，又满足复杂的时空逻辑约束。这种结合LLM和形式化验证的方法，可以有效解决LLM的幻觉问题，并提高运动规划的可靠性。

技术框架：T3 Planner包含三个级联模块：任务分解模块、轨迹生成模块和轨迹验证模块。任务分解模块负责将自然语言指令分解为一系列时空约束；轨迹生成模块利用LLM根据这些约束生成候选轨迹序列；轨迹验证模块使用STL验证器检查候选轨迹是否满足所有约束。如果轨迹不满足约束，则反馈给轨迹生成模块进行调整，直到找到满足所有约束的轨迹。

关键创新：T3 Planner的关键创新在于将LLM与形式化方法相结合，实现运动规划的自我校正。通过STL验证器对LLM生成的轨迹进行验证，可以有效避免LLM的幻觉问题，并确保生成的运动规划满足复杂的时空逻辑约束。此外，T3 Planner采用级联模块的设计，将复杂的运动规划问题分解为多个子问题，降低了每个模块的难度，提高了整体规划效率。

关键设计：T3 Planner使用Qwen3-4B模型作为LLM，并通过蒸馏技术将其压缩到更小的尺寸，以实现高效部署。STL验证器采用现有的工具，并根据具体任务进行定制。在轨迹生成模块中，使用了特定的prompt工程来引导LLM生成符合要求的轨迹。此外，还设计了反馈机制，将STL验证器的结果反馈给LLM，指导其进行轨迹调整。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，T3 Planner在不同场景下均显著优于基线方法。具体而言，T3 Planner能够成功生成满足复杂时空逻辑约束的运动规划，而基线方法则容易出现违反约束的情况。此外，通过蒸馏技术，可以将T3 Planner部署到轻量级的Qwen3-4B模型中，从而实现高效部署。

🎯 应用场景

T3 Planner可应用于各种需要机器人执行复杂任务的场景，例如智能制造、仓储物流、家庭服务等。它可以帮助机器人理解自然语言指令，并生成满足时空逻辑约束的运动规划，从而实现更智能、更可靠的机器人操作。该研究的未来影响在于推动机器人运动规划的自动化和智能化，降低机器人应用门槛。

📄 摘要（原文）

Translating natural language instructions into executable motion plans is a fundamental challenge in robotics. Traditional approaches are typically constrained by their reliance on domain-specific expertise to customize planners, and often struggle with spatio-temporal couplings that usually lead to infeasible motions or discrepancies between task planning and motion execution. Despite the proficiency of Large Language Models (LLMs) in high-level semantic reasoning, hallucination could result in infeasible motion plans. In this paper, we introduce the T3 Planner, an LLM-enabled robotic motion planning framework that self-corrects it output with formal methods. The framework decomposes spatio-temporal task constraints via three cascaded modules, each of which stimulates an LLM to generate candidate trajectory sequences and examines their feasibility via a Signal Temporal Logic (STL) verifier until one that satisfies complex spatial, temporal, and logical constraints is found.Experiments across different scenarios show that T3 Planner significantly outperforms the baselines. The required reasoning can be distilled into a lightweight Qwen3-4B model that enables efficient deployment. All supplementary materials are accessible at https://github.com/leeejia/T3_Planner.