This paper addresses a new motion planning problem for mobile robots tasked with accomplishing multiple high-level sub-tasks, expressed using natural language (NL). These sub-tasks should be accomplished in a temporal and logical order. To formally define the overarching mission, we leverage Linear Temporal Logic (LTL) defined over atomic predicates modeling these NL-based sub-tasks. This is in 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 (i) automata theory to determine what NL-specified sub-tasks should be accomplished 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 to determine if external assistance is required. We provide theoretical probabilistic mission satisfaction guarantees as well as extensive comparative experiments on mobile manipulation tasks.

翻译：本文针对移动机器人需完成多个用自然语言表述的高级子任务的新运动规划问题展开研究。这些子任务需按时间逻辑顺序完成。为形式化定义总体任务，我们利用基于原子谓词定义的线性时序逻辑对自然语言子任务进行建模，这与相关规划方法在原子谓词上定义低层级系统配置的LTL任务形成对比。我们的目标是设计满足基于自然语言原子命题的LTL任务的机器人规划方案。该设定中产生的新技术挑战在于如何推理机器人规划方案相对于此类LTL编码任务的正确性。为解决该问题，我们提出HERACLEs——一种层级化共形自然语言规划器，其核心依赖于：(i)自动机理论确定下一个需完成的自然语言子任务以推进任务进度；(ii)大语言模型设计满足这些子任务的机器人规划方案；(iii)共形预测对规划方案的正确性进行概率推理，并判定是否需要外部辅助。我们提供了理论概率任务满足性保证，并在移动操作任务上开展了广泛的对比实验。