nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models
Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, Caroline Trippel · 2023 · 122 citationsRead the paper
Abstract A rigorous formalization of desired system requirements is indispensable when performing any verification task. This often limits the application of verification techniques, as writing formal specifications is an error-prone and time-consuming manual task. To facilitate this, we present , a framework for applying Large Language Models (LLMs) to derive formal specifications (in temporal logics) from unstructured natural language. In particular, we introduce a new methodology to detect and resolve the inherent ambiguity of system requirements in natural language: we utilize LLMs to map subformulas of the formalization back to the corresponding natural language fragments of the input. Users iteratively add, delete, and edit these sub-translations to amend erroneous formalizations, which is easier than manually redrafting the entire formalization. The framework is agnostic to specific application domains and can be extended to similar specification languages and new neural models. We perform a user study to obtain a challenging dataset, which we use to run experiments on the quality of translations. We provide an open-source implementation, including a web-based frontend.
What the full text shows
Working prototype- Interactive refinement significantly improves translation accuracy compared to initial translations. — 86.1% accuracy vs. 44.4% initial accuracy (using Codex) (Benchmark dataset of 36 challenging LTL instances)
- In-distribution few-shot prompting increases initial translation quality. — 58.3% accuracy vs. 44.4% with minimal prompt (using Codex) (Benchmark dataset of 36 challenging LTL instances)
- Providing high-quality sub-translations from a stronger model (Codex) improves the performance of a weaker model (Bloom). — 36.4% of previously unsolved instances were solved (Teacher-Student experiment using Codex as teacher and Bloom as student)
- The framework outperforms previous neural and grammar-based translation methods on unstructured data. — 44.4% (nl2spec+Codex initial) vs. 5.5% (T-5 fine-tuned) and 2.7% (nl2ltl) (Benchmark dataset of 36 challenging LTL instances)
- Setup
- Benchmark dataset of 36 unique LTL instances provided by five experts, restricted to one sentence and five atomic propositions per instance.
- How
- The framework uses LLMs to translate natural language to LTL and decomposes the result into sub-translations (mappings of formula fragments to text). Users interactively refine these sub-translations to resolve ambiguities and errors, which then informs a new prompt for the LLM.
- Limitations
- Reliance on computational resources at inference time · Initial quality depends on the pre-training data of the underlying LLM (logics, code, math)
Summarized by Gemma 4 from the open-access full text · 10 Oct 2026. Read it