Linear Temporal Logic (LTL) is a widely used task specification language for autonomous systems. To mitigate the significant manual effort and expertise required to define LTL-encoded tasks, several methods have been proposed for translating Natural Language (NL) instructions into LTL formulas, which, however, lack correctness guarantees. To address this, we propose a new NL-to-LTL translation method, called ConformalNL2LTL that achieves user-defined translation success rates on unseen NL commands. Our method constructs LTL formulas iteratively by solving a sequence of open-vocabulary question-answering (QA) problems using large language models (LLMs). These QA tasks are handled collaboratively by a primary and an auxiliary model. The primary model answers each QA instance while quantifying uncertainty via conformal prediction; when it is insufficiently certain according to user-defined confidence thresholds, it requests assistance from the auxiliary model and, if necessary, from the user. We demonstrate theoretically and empirically that ConformalNL2LTL achieves the desired translation accuracy while minimizing user intervention.

翻译：线性时序逻辑（LTL）是自主系统中广泛使用的任务规约语言。为了减少定义LTL编码任务所需的大量人工投入和专业知识，已有多种方法被提出用于将自然语言（NL）指令翻译成LTL公式，但这些方法缺乏正确性保证。为解决此问题，我们提出了一种新的NL到LTL翻译方法，称为ConformalNL2LTL，该方法在未见过的NL命令上实现了用户定义的翻译成功率。我们的方法通过使用大语言模型（LLM）解决一系列开放词汇问答（QA）问题来迭代地构建LTL公式。这些QA任务由主模型和辅助模型协作处理。主模型通过保形预测量化不确定性来回答每个QA实例；当根据用户定义的置信度阈值其确定性不足时，它会请求辅助模型并在必要时请求用户的协助。我们从理论和实验上证明，ConformalNL2LTL在最小化用户干预的同时实现了期望的翻译准确率。