To enable non-experts to specify long-horizon, multi-robot collaborative tasks, language models are increasingly used to translate natural language commands into formal specifications. However, because translation can occur in multiple ways, such translations may lack accuracy or lead to inefficient multi-robot planning. Our key insight is that concise hierarchical specifications can simplify planning while remaining straightforward to derive from human instructions. We propose Nl2Hltl2Plan, a framework that translates natural language commands into hierarchical Linear Temporal Logic (LTL) and solves the corresponding planning problem. The translation involves two steps leveraging Large Language Models (LLMs). First, an LLM transforms instructions into a Hierarchical Task Tree, capturing logical and temporal relations. Next, a fine-tuned LLM converts sub-tasks into flat LTL formulas, which are aggregated into hierarchical specifications, with the lowest level corresponding to ordered robot actions. These specifications are then used with off-the-shelf planners. Our Nl2Hltl2Plan demonstrates the potential of LLMs in hierarchical reasoning for multi-robot task planning. Evaluations in simulation and real-world experiments with human participants show that Nl2Hltl2Plan outperforms existing methods, handling more complex instructions while achieving higher success rates and lower costs in task allocation and planning. Additional details are available at https://nl2hltl2plan.github.io .

翻译：为使非专家能够指定长时程、多机器人协作任务，语言模型被越来越多地用于将自然语言指令翻译为形式化规约。然而，由于翻译可能存在多种方式，此类翻译可能缺乏准确性或导致低效的多机器人规划。我们的核心见解是，简洁的分层规约可以在保持易于从人类指令推导的同时，简化规划过程。我们提出了Nl2Hltl2Plan，一个将自然语言指令翻译为分层线性时序逻辑（LTL）并解决相应规划问题的框架。该翻译过程利用大型语言模型（LLM）分两步进行。首先，一个LLM将指令转换为分层任务树，以捕捉逻辑与时序关系。接着，一个经过微调的LLM将子任务转换为扁平的LTL公式，这些公式被聚合成分层规约，其中最低层级对应于有序的机器人动作。这些规约随后与现成的规划器结合使用。我们的Nl2Hltl2Plan展示了LLM在多机器人任务规划中进行分层推理的潜力。在仿真和真人参与的实物实验中的评估表明，Nl2Hltl2Plan优于现有方法，能够处理更复杂的指令，同时在任务分配和规划中实现更高的成功率和更低的成本。更多细节请访问 https://nl2hltl2plan.github.io 。