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

arXiv: https://arxiv.org/abs/2507.00877 · HTML: https://mlsanity.com/paper/2507.00877/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 17 of its 35 references that are in the map.
- First posted on arXiv 1 Jul 2025.

## Builds on (most cited first, 17 of 17)

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Microsoft COCO: Common Objects in Context](https://mlsanity.com/paper/1405.0312/) (2014)
- [Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformer](https://mlsanity.com/paper/1910.10683/) (2019)
- [Grammar-Constrained Decoding for Structured NLP Tasks without Finetuning](https://mlsanity.com/paper/2305.13971/) (2023)
- [Fast Lexically Constrained Decoding with Dynamic Beam Allocation for Neural Machine Translation](https://mlsanity.com/paper/1804.06609/) (2018)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [NL2TL: Transforming Natural Languages to Temporal Logics using Large Language Models](https://mlsanity.com/paper/2305.07766/) (2023)
- [Grounding Complex Natural Language Commands for Temporal Tasks in Unseen Environments](https://mlsanity.com/paper/2302.11649/) (2023)
- [Data-Efficient Learning of Natural Language to Linear Temporal Logic Translators for Robot Task Specification](https://mlsanity.com/paper/2303.08006/) (2023)
- [Formal Specifications from Natural Language](https://mlsanity.com/paper/2206.01962/) (2022)
- [Learning a natural-language to LTL executable semantic parser for grounded robotics](https://mlsanity.com/paper/2008.03277/) (2020)
- [DeepSTL -- From English Requirements to Signal Temporal Logic](https://mlsanity.com/paper/2109.10294/) (2021)
- [Formal Synthesis of Controllers for Safety-Critical Autonomous Systems: Developments and Challenges](https://mlsanity.com/paper/2402.13075/) (2024)
- [Generalizing to New Domains by Mapping Natural Language to Lifted LTL](https://mlsanity.com/paper/2110.05603/) (2021)
- [ConformalNL2LTL: Translating Natural Language Instructions into Temporal Logic Formulas with Conformal Correctness Guarantees](https://mlsanity.com/paper/2504.21022/) (2025)
- [Metrics for Signal Temporal Logic Formulae](https://mlsanity.com/paper/1808.03315/) (2018)
- [On Systematically Building a Controlled Natural Language for Functional Requirements](https://mlsanity.com/paper/2005.01355/) (2020)

## Built on by (most cited first, 4 of 4)

- [AgentLTL: A Trace-Verification Framework for Measuring, Enforcing, and Training Procedural Compliance in Tool-Using LLM Agents](https://mlsanity.com/paper/2607.02599/) (2026)
- [VeriTrans: Fine-Tuned LLM-Assisted NL-to-PL Translation via a Deterministic Neuro-Symbolic Pipeline](https://mlsanity.com/paper/2604.10341/) (2026)
- [GinSign: Grounding Natural Language Into System Signatures for Temporal Logic Translation](https://mlsanity.com/paper/2512.16770/) (2025)
- [ASP-Bench: From Natural Language to Logic Programs](https://mlsanity.com/paper/2602.01171/) (2026)

## Abstract (arXiv)

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 four 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.