To make robots accessible to a broad audience, it is critical to endow them with the ability to take universal modes of communication, like commands given in natural language, and extract a concrete desired task specification, defined using a formal language like linear temporal logic (LTL). In this paper, we present a learning-based approach for translating from natural language commands to LTL specifications with very limited human-labeled training data. This is in stark contrast to existing natural-language to LTL translators, which require large human-labeled datasets, often in the form of labeled pairs of LTL formulas and natural language commands, to train the translator. To reduce reliance on human data, our approach generates a large synthetic training dataset through algorithmic generation of LTL formulas, conversion to structured English, and then exploiting the paraphrasing capabilities of modern large language models (LLMs) to synthesize a diverse corpus of natural language commands corresponding to the LTL formulas. We use this generated data to finetune an LLM and apply a constrained decoding procedure at inference time to ensure the returned LTL formula is syntactically correct. We evaluate our approach on three existing LTL/natural language datasets and show that we can translate natural language commands at 75\% accuracy with far less human data ($\le$12 annotations). Moreover, when training on large human-annotated datasets, our method achieves higher test accuracy (95\% on average) than prior work. Finally, we show the translated formulas can be used to plan long-horizon, multi-stage tasks on a 12D quadrotor.
翻译:为了使机器人面向广泛受众,赋予它们接受通用交流形式的能力,例如使用自然语言给出的命令,并提取一个明确的期望任务规范,采用类似线性时间逻辑(LTL)这样的形式语言定义。本文提出了一种论文基于学习的方法,使用非常有限的人工标注训练数据,将自然语言命令翻译成LTL规范。这与现有的自然语言到LTL翻译器形成鲜明对比,后者需要大量的人工标注数据,通常采用已标记的LTL公式和自然语言命令。数据集来训练翻译器。为了减少对人工数据的依赖,我们的方法通过算法生成LTL公式,将其转换为结构化英语,然后利用现代大型语言模型(LLM)的释义能力,综合合成对应于LTL公式的多样化自然语言命令语料库来生成大量的合成训练数据。我们使用这些生成的数据来微调LLM,并在推理时应用受限解码过程,以确保返回的LTL公式在语法上是正确的。我们在三个现有的LTL /自然语言数据集上评估了我们的方法,并展示了我们可以使用更少的人工数据($ \ le $12个注释)将自然语言命令翻译成LTL规范,准确率达到75%。此外,当在大型人工注释的数据集上进行训练时,我们的方法实现了更高的测试准确度(平均95%)比先前的工作。最后,我们展示了翻译后的公式可用于规划12D四旋翼的长周期、多阶段任务。