Verifiable Natural Language to Linear Temporal Logic Translation: A Benchmark Dataset and Evaluation Suite

• URL: http://arxiv.org/abs/2507.00877v1
• Date: Tue, 01 Jul 2025 15:41:57 GMT
• Title: Verifiable Natural Language to Linear Temporal Logic Translation: A Benchmark Dataset and Evaluation Suite
• Authors: William H English, Chase Walker, Dominic Simon, Sumit Kumar Jha, Rickard Ewetz,
• Abstract summary: Empirical evaluation of state-of-the-art natural-language (NL) to temporal-logic (TL) translation systems reveals near-perfect performance on existing benchmarks.<n>We introduce the Verifiable Linear Temporal Logic Benchmark (VLTL-Bench), a unifying benchmark that measures verification and verifiability of automated NL-to-LTL translation.
• Score: 8.325455397285873
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Empirical evaluation of state-of-the-art natural-language (NL) to temporal-logic (TL) translation systems reveals near-perfect performance on existing benchmarks. However, current studies measure only the accuracy of the translation of NL logic into formal TL, ignoring a system's capacity to ground atomic propositions into new scenarios or environments. This is a critical feature, necessary for the verification of resulting formulas in a concrete state space. Consequently, most NL-to-TL translation frameworks propose their own bespoke dataset in which the correct grounding is known a-priori, inflating performance metrics and neglecting the need for extensible, domain-general systems. In this paper, we introduce the Verifiable Linear Temporal Logic Benchmark ( VLTL-Bench), a unifying benchmark that measures verification and verifiability of automated NL-to-LTL translation. The dataset consists of three unique state spaces and thousands of diverse natural language specifications and corresponding formal specifications in temporal logic. Moreover, the benchmark contains sample traces to validate the temporal logic expressions. While the benchmark directly supports end-to-end evaluation, we observe that many frameworks decompose the process into i) lifting, ii) grounding, iii) translation, and iv) verification. The benchmark provides ground truths after each of these steps to enable researches to improve and evaluate different substeps of the overall problem. To encourage methodologically sound advances in verifiable NL-to-LTL translation approaches, we release VLTL-Bench here: https://www.kaggle.com/datasets/dubascudes/vltl bench.

Related papers

• PARALLELPROMPT: Extracting Parallelism from Large Language Model Queries [16.40921376558516]
  We introduce PARALLELPROMPT, the first benchmark for measuring intra-query parallelism in natural user prompts.<n>Our dataset comprises over 37,000 real-world prompts from public LLM chat logs.<n>We provide an execution suite that benchmarks serial vs. parallel strategies, measuring latency, structural adherence, and semantic fidelity.
  arXiv  Detail & Related papers  (2025-06-23T15:05:54Z)
• LLM-Based Evaluation of Low-Resource Machine Translation: A Reference-less Dialect Guided Approach with a Refined Sylheti-English Benchmark [1.3927943269211591]
  We propose a comprehensive framework that enhances Large Language Models (LLMs)-based machine translation evaluation.<n>We extend the ONUBAD dataset by incorporating Sylheti-English sentence pairs, corresponding machine translations, and Direct Assessment (DA) scores annotated by native speakers.<n>Our evaluation shows that the proposed pipeline consistently outperforms existing methods, achieving the highest gain of +0.1083 in Spearman correlation.
  arXiv  Detail & Related papers  (2025-05-18T07:24:13Z)
• PASS-FC: Progressive and Adaptive Search Scheme for Fact Checking of Comprehensive Claims [2.187145486382368]
  PASS-FC is a Progressive and Adaptive Search Scheme for Fact Checking.<n>Each atomic claim is first grounded with a precise time span and disambiguated entity descriptors.<n>Experiments on six benchmark--covering general knowledge, scientific literature, real-world events, and ten languages--show that PASS-FC consistently outperforms prior systems.
  arXiv  Detail & Related papers  (2025-04-14T04:24:37Z)
• Context is Key: A Benchmark for Forecasting with Essential Textual Information [87.3175915185287]
  "Context is Key" (CiK) is a forecasting benchmark that pairs numerical data with diverse types of carefully crafted textual context.<n>We evaluate a range of approaches, including statistical models, time series foundation models, and LLM-based forecasters.<n>We propose a simple yet effective LLM prompting method that outperforms all other tested methods on our benchmark.
  arXiv  Detail & Related papers  (2024-10-24T17:56:08Z)
• CoT-TL: Low-Resource Temporal Knowledge Representation of Planning Instructions Using Chain-of-Thought Reasoning [0.0]
  CoT-TL is a data-efficient in-context learning framework for translating natural language specifications into representations. CoT-TL achieves state-of-the-art accuracy across three diverse datasets in low-data scenarios.
  arXiv  Detail & Related papers  (2024-10-21T17:10:43Z)
• Mind the Error! Detection and Localization of Instruction Errors in Vision-and-Language Navigation [65.25839671641218]
  We propose a novel benchmark dataset that introduces various types of instruction errors considering potential human causes.<n>We observe a noticeable performance drop (up to -25%) in Success Rate when evaluating the state-of-the-art VLN-CE methods on our benchmark.<n>We also propose an effective method, based on a cross-modal transformer architecture, that achieves the best performance in error detection and localization.
  arXiv  Detail & Related papers  (2024-03-15T21:36:15Z)
• NLPre: a revised approach towards language-centric benchmarking of Natural Language Preprocessing systems [2.141587359797428]
  It is arduous to compare novel solutions to well-entrenched preprocessing toolkits, relying on rule-based morphological analysers or dictionaries. Inspired by the GLUE benchmark, the proposed language-centric benchmarking system enables comprehensive ongoing evaluation of multiple NLPre tools. The prototype application is configured for Polish and integrated with the thoroughly assembled NLPre-PL benchmark.
  arXiv  Detail & Related papers  (2024-03-07T14:07:00Z)
• How to Handle Different Types of Out-of-Distribution Scenarios in Computational Argumentation? A Comprehensive and Fine-Grained Field Study [59.13867562744973]
  This work systematically assesses LMs' capabilities for out-of-distribution (OOD) scenarios. We find that the efficacy of such learning paradigms varies with the type of OOD. Specifically, while ICL excels for domain shifts, prompt-based fine-tuning surpasses for topic shifts.
  arXiv  Detail & Related papers  (2023-09-15T11:15:47Z)
• Generating Benchmarks for Factuality Evaluation of Language Models [61.69950787311278]
  We propose FACTOR: Factual Assessment via Corpus TransfORmation, a scalable approach for evaluating LM factuality. FACTOR automatically transforms a factual corpus of interest into a benchmark evaluating an LM's propensity to generate true facts from the corpus vs. similar but incorrect statements. We show that: (i) our benchmark scores increase with model size and improve when the LM is augmented with retrieval; (ii) benchmark score and perplexity do not always agree on model ranking; (iii) when perplexity and benchmark score disagree, the latter better reflects factuality in open-ended generation.
  arXiv  Detail & Related papers  (2023-07-13T17:14:38Z)
• Non-Parametric Domain Adaptation for End-to-End Speech Translation [72.37869362559212]
  End-to-End Speech Translation (E2E-ST) has received increasing attention due to the potential of its less error propagation, lower latency, and fewer parameters. We propose a novel non-parametric method that leverages domain-specific text translation corpus to achieve domain adaptation for the E2E-ST system.
  arXiv  Detail & Related papers  (2022-05-23T11:41:02Z)
• A Closer Look at Debiased Temporal Sentence Grounding in Videos: Dataset, Metric, and Approach [53.727460222955266]
  Temporal Sentence Grounding in Videos (TSGV) aims to ground a natural language sentence in an untrimmed video. Recent studies have found that current benchmark datasets may have obvious moment annotation biases. We introduce a new evaluation metric "dR@n,IoU@m" that discounts the basic recall scores to alleviate the inflating evaluation caused by biased datasets.
  arXiv  Detail & Related papers  (2022-03-10T08:58:18Z)
• Logical Natural Language Generation from Open-Domain Tables [107.04385677577862]
  We propose a new task where a model is tasked with generating natural language statements that can be emphlogically entailed by the facts. To facilitate the study of the proposed logical NLG problem, we use the existing TabFact dataset citechen 2019tabfact featured with a wide range of logical/symbolic inferences. The new task poses challenges to the existing monotonic generation frameworks due to the mismatch between sequence order and logical order.
  arXiv  Detail & Related papers  (2020-04-22T06:03:10Z)

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.