Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

ConformalNL2LTL: Translating Natural Language Instructions into Temporal Logic Formulas with Conformal Correctness Guarantees

Jun Wang, David Smith Sundarsingh, Jyotirmoy V. Deshmukh, Yiannis Kantaros

TL;DR

This work introduces a new NL-to-LTL translation method, called ConformalNL2LTL, that can achieve user-defined translation success rates over unseen NL commands and leverages conformal prediction (CP), a distribution-free uncertainty quantification tool for black-box models.

Abstract

Linear Temporal Logic (LTL) has become a prevalent specification language for robotic tasks. 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 introduce a new NL-to-LTL translation method, called ConformalNL2LTL, that can achieve user-defined translation success rates over unseen NL commands. Our method constructs LTL formulas iteratively by addressing a sequence of open-vocabulary Question-Answering (QA) problems with LLMs. To enable uncertainty-aware translation, we leverage conformal prediction (CP), a distribution-free uncertainty quantification tool for black-box models. CP enables our method to assess the uncertainty in LLM-generated answers, allowing it to proceed with translation when sufficiently confident and request help otherwise. We provide both theoretical and empirical results demonstrating that ConformalNL2LTL achieves user-specified translation accuracy while minimizing help rates.

ConformalNL2LTL: Translating Natural Language Instructions into Temporal Logic Formulas with Conformal Correctness Guarantees

TL;DR

This work introduces a new NL-to-LTL translation method, called ConformalNL2LTL, that can achieve user-defined translation success rates over unseen NL commands and leverages conformal prediction (CP), a distribution-free uncertainty quantification tool for black-box models.

Abstract

Linear Temporal Logic (LTL) has become a prevalent specification language for robotic tasks. 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 introduce a new NL-to-LTL translation method, called ConformalNL2LTL, that can achieve user-defined translation success rates over unseen NL commands. Our method constructs LTL formulas iteratively by addressing a sequence of open-vocabulary Question-Answering (QA) problems with LLMs. To enable uncertainty-aware translation, we leverage conformal prediction (CP), a distribution-free uncertainty quantification tool for black-box models. CP enables our method to assess the uncertainty in LLM-generated answers, allowing it to proceed with translation when sufficiently confident and request help otherwise. We provide both theoretical and empirical results demonstrating that ConformalNL2LTL achieves user-specified translation accuracy while minimizing help rates.
Paper Structure (13 sections, 2 theorems, 10 equations, 2 figures, 2 tables, 1 algorithm)

This paper contains 13 sections, 2 theorems, 10 equations, 2 figures, 2 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Problem Statement
  3. Translating Natural Language to Linear Temporal Logic with Correctness Guarantees
  4. Incremental Translation using LLMs
  5. Constructing Local Prediction Sets using CP
  6. Translation Success Rate Guarantees
  7. Experimental Validation
  8. Setting Up Translation Scenarios for Robot Tasks
  9. Empirical Evaluation
  10. Conclusions and Future Work
  11. Comparisons Against Non-Conformalized LLM-based Translators
  12. Setting up Comparative Experiment
  13. Comparative Evaluation

Key Result

Proposition 3.1

It holds that $\bar{{\mathcal{C}}}(\bar{\ell}_{\text{test}})=\hat{{\mathcal{C}}}(\bar{\ell}_{\text{test}})$, where $\bar{{\mathcal{C}}}(\bar{\ell}_{\text{test}})$ and $\hat{{\mathcal{C}}}(\bar{\ell}_{\text{test}})$ are defined in eq:pred3 and eq:causalPred3, respectively.

Figures (2)

  • Figure 1: ConformalNL2LTL translates natural language-based robot tasks into Linear Temporal Logic formula with translation correctness guarantee.
  • Figure 2: Example of the constructed prompt for GPT-4o. This prompt refers to $t=1$ when the action history and the formula so far are both empty.

Theorems & Definitions (7)

  • Remark 2.1: Distribution ${\mathcal{D}}$
  • Example 2.2: NL-to-LTL
  • Proposition 3.1
  • Theorem 3.2: Translation Success Rates
  • proof
  • Remark 3.3: Multiple Semantically Equivalent Formulas
  • Remark 4.1: Translation Mistakes