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

• URL: http://arxiv.org/abs/2504.21022v1
• Date: Tue, 22 Apr 2025 20:32:34 GMT
• Title: ConformalNL2LTL: Translating Natural Language Instructions into Temporal Logic Formulas with Conformal Correctness Guarantees
• Authors: Jun Wang, David Smith Sundarsingh, Jyotirmoy V. Deshmukh, Yiannis Kantaros,
• Abstract summary: We introduce a new NL-to-LTL translation method, called ConformalNL2LTL, that can achieve user-defined translation success rates over unseen NL commands.<n>Our method constructs formulas iteratively by addressing a sequence of open-vocabulary Question-Answering (QA) problems with LLMs.
• Score: 10.687644259002674
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Self-Correction Makes LLMs Better Parsers [19.20952673157709]
  Large language models (LLMs) have achieved remarkable success across various natural language processing (NLP) tasks.<n>Recent studies suggest that they still face challenges in performing fundamental NLP tasks essential for deep language understanding.<n>We propose a self-correction method that leverages grammar rules from existing treebanks to guide LLMs in correcting previous errors.
  arXiv  Detail & Related papers  (2025-04-19T03:50:59Z)
• Lost in Literalism: How Supervised Training Shapes Translationese in LLMs [51.04435855143767]
  Large language models (LLMs) have achieved remarkable success in machine translation.<n>However, translationese, characterized by overly literal and unnatural translations, remains a persistent challenge.<n>We introduce methods to mitigate these biases, including polishing golden references and filtering unnatural training instances.
  arXiv  Detail & Related papers  (2025-03-06T12:14:45Z)
• Attribute Controlled Fine-tuning for Large Language Models: A Case Study on Detoxification [76.14641982122696]
  We propose a constraint learning schema for fine-tuning Large Language Models (LLMs) with attribute control. We show that our approach leads to an LLM that produces fewer inappropriate responses while achieving competitive performance on benchmarks and a toxicity detection task.
  arXiv  Detail & Related papers  (2024-10-07T23:38:58Z)
• DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications for Multi-Task RL [59.01527054553122]
  Linear temporal logic (LTL) has recently been adopted as a powerful formalism for specifying complex, temporally extended tasks.<n>Existing approaches suffer from several shortcomings.<n>We propose a novel learning approach to address these concerns.
  arXiv  Detail & Related papers  (2024-10-06T21:30:38Z)
• Directed Exploration in Reinforcement Learning from Linear Temporal Logic [59.707408697394534]
  Linear temporal logic (LTL) is a powerful language for task specification in reinforcement learning. We show that the synthesized reward signal remains fundamentally sparse, making exploration challenging. We show how better exploration can be achieved by further leveraging the specification and casting its corresponding Limit Deterministic B"uchi Automaton (LDBA) as a Markov reward process.
  arXiv  Detail & Related papers  (2024-08-18T14:25:44Z)
• Translate-and-Revise: Boosting Large Language Models for Constrained Translation [42.37981028583618]
  We leverage the capabilities of large language models (LLMs) for constrained translation. LLMs can easily adapt to this task by taking translation instructions and constraints as prompts. We show 15% improvement in constraint-based translation accuracy over standard LLMs.
  arXiv  Detail & Related papers  (2024-07-18T05:08:09Z)
• Prefix Text as a Yarn: Eliciting Non-English Alignment in Foundation Language Model [50.339632513018934]
  supervised fine-tuning (SFT) has been a straightforward approach for tailoring the output of foundation large language model (LLM) to specific preferences. We critically examine this hypothesis within the scope of cross-lingual generation tasks. We introduce a novel training-free alignment method named PreTTY, which employs minimal task-related prior tokens.
  arXiv  Detail & Related papers  (2024-04-25T17:19:36Z)
• Building Accurate Translation-Tailored LLMs with Language Aware Instruction Tuning [57.323716555996114]
  Off-target translation remains an unsolved problem, especially for low-resource languages. Recent works have either designed advanced prompting strategies to highlight the functionality of translation instructions or exploited the in-context learning ability of LLMs. In this work, we design a two-stage fine-tuning algorithm to improve the instruction-following ability (especially the translation direction) of LLMs.
  arXiv  Detail & Related papers  (2024-03-21T13:47:40Z)
• Natural Language-conditioned Reinforcement Learning with Inside-out Task Language Development and Translation [14.176720914723127]
  Natural Language-conditioned reinforcement learning (RL) enables the agents to follow human instructions. Previous approaches generally implemented language-conditioned RL by providing human instructions in natural language (NL) and training a following policy. We develop an inside-out scheme for natural language-conditioned RL by developing a task language (TL) that is task-related and unique.
  arXiv  Detail & Related papers  (2023-02-18T15:49:09Z)
• From English to Signal Temporal Logic [7.6398837478968025]
  We propose DeepSTL, a tool and technique for the translation of informal requirements, given as free English sentences, into Signal Temporal Logic (STL), a formal specification language for cyber-physical systems. A major challenge to devise such a translator is the lack of publicly available informal requirements and formal specifications. In the second step, we use a state-of-the-art transformer-based neural translation technique, to train an accurate attentional translator of English to STL.
  arXiv  Detail & Related papers  (2021-09-21T16:13:29Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.