arXiv:2504.21022v1 宣传类型: cross 摘要:线性时序逻辑(LTL)已成为机器人任务的广泛规范语言。为了减轻定义LTL编码任务所需的重大手动工作和专业知识，已经提出了将自然语言(NL)指令转换为LTL公式的多种方法，但这些方法缺乏正确性保证。为了解决这个问题，我们提出了一种新的NL到LTL转换方法，称为ConformalNL2LTL，该方法可以在未见过的NL指令上实现用户定义的转换成功率。我们的方法通过使用LLMs逐步解决一系列开放词汇量的问答(QA)问题来构建LTL公式。为了实现不确定性感知的转换，我们利用了形式化预测(CP)，这是一种适用于黑盒模型的无分布不确定性量化工具。CP使我们的方法能够评估LLM生成的答案的不确定性，当足够有信心时可以继续转换，否则则请求帮助。我们提供了理论和实证结果，证明ConformalNL2LTL能够在保证用户指定的转换准确性的同时，减少求助率。