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任务的机器人规划。该场景产生的新技术挑战在于如何验证机器人规划相对于这类LTL编码任务的正确性。为此，我们提出HERACLEs——一种层次化保形自然语言规划器，其核心机制包括：(i) 利用自动机理论判定当前应完成的自然语言子任务以推进任务进程；(ii) 借助大语言模型设计满足这些子任务的机器人规划；(iii) 通过保形预测对规划正确性进行概率推理，并判断是否需要外部协助。我们提供了理论概率任务满足保证，并在移动操作任务上进行了广泛对比实验。