This paper addresses a new motion planning problem for mobile robots tasked with accomplishing multiple high-level sub-tasks, expressed using natural language (NL), in a temporal and logical order. To formally define such missions, we leverage LTL defined over NL-based atomic predicates modeling the considered NL-based sub-tasks. This is contrast to related planning approaches that define LTL tasks over atomic predicates capturing desired low-level system configurations. Our goal is to design robot plans that satisfy LTL tasks defined over NL-based atomic propositions. A novel technical challenge arising in this setup lies in reasoning about correctness of a robot plan with respect to such LTL-encoded tasks. To address this problem, we propose HERACLEs, a hierarchical conformal natural language planner, that relies on a novel integration of existing tools that include (i) automata theory to determine the NL-specified sub-task the robot should accomplish next to make mission progress; (ii) Large Language Models to design robot plans satisfying these sub-tasks; and (iii) conformal prediction to reason probabilistically about correctness of the designed plans and mission satisfaction and to determine if external assistance is required. We provide extensive comparative experiments on mobile manipulation tasks. The project website is ltl-llm.github.io.

翻译：本文针对移动机器人在时序与逻辑顺序下，使用自然语言表达的多重高层子任务，提出了一种新的运动规划问题。为正式定义此类任务，我们利用基于自然语言原子谓词定义的线性时序逻辑，对所述自然语言子任务进行建模。这与相关规划方法形成对比——后者定义线性时序逻辑任务时采用捕捉期望低层系统配置的原子谓词。我们的目标是设计满足基于自然语言原子命题的线性时序逻辑任务的机器人规划。该设置中产生的新技术挑战在于：如何针对此类线性时序逻辑编码任务，推理机器人规划的正确性。为解决此问题，我们提出HERACLEs——一种层次化保形自然语言规划器，它创新性地整合了以下现有工具：(i)自动机理论，用于确定机器人下一步应完成的自然语言指定子任务，以推进任务进程；(ii)大语言模型，用于设计满足这些子任务的机器人规划；(iii)保形预测，用于概率性地推理所设计规划的正确性与任务满足程度，并判定是否需要外部协助。我们在移动操作任务上进行了广泛对比实验。项目网站为ltl-llm.github.io。