让AI把自然语言指令转成带可信度保证的逻辑公式
ConformalNL2LTL: Translating Natural Language Instructions into Temporal Logic Formulas with Conformal Correctness Guarantees
- 用大模型分步问答生成逻辑公式，边生成边评估不确定性
- 用户设定准确率目标后，系统自动调节求助频率以达标
- 适合需要高可靠性任务规范的自动驾驶等场景
线性时序逻辑（LTL）是自主系统常用的任务描述语言。为减少人工编写LTL公式的繁琐与专业门槛，已有方法尝试将自然语言（NL）指令转化为LTL公式，但缺乏正确性保障。为此，我们提出ConformalNL2LTL方法，可实现对未见自然语言命令的用户定义翻译成功率。该方法通过大语言模型（LLMs）迭代求解一系列开放词汇问答（QA）问题，构建LTL公式。主模型在回答每个问题时，使用近似预测量化不确定性；当置信度低于用户设定阈值时，会向辅助模型或用户求助。我们从理论上和实证上证明，ConformalNL2LTL能在最小化用户干预的前提下，达成期望的翻译准确率。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。