mlsanityData to 7 Oct 2026

nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models

arXiv 2303.04864 ↗First posted 8 Mar 2023cs.LO cs.AI cs.LGcited by 57

Not on the map. Why?

Abstract (arXiv)

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 nl2spec, 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.

Key facts. Cited by 57 papers in the map (data through 7 Oct 2026). Builds on 25 of its 52 references that are in the map. First posted on arXiv 8 Mar 2023.

Builds on

25 of 52 references.

References · 25

  1. 2017Attention Is All You Needcited by 59,932
  2. 2018BERT: Pre-training of Deep Bidirectional Transformers for Language Understandingcited by 40,204
  3. 2020Language Models are Few-Shot Learnerscited by 32,199
  4. 2019Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformercited by 14,491
  5. 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,302
  6. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  7. 2020Scaling Laws for Neural Language Modelscited by 6,411
  8. 2013Efficient Estimation of Word Representations in Vector Spacecited by 4,346
  9. 2020The Pile: An 800GB Dataset of Diverse Text for Language Modelingcited by 2,346
  10. 2019HuggingFace's Transformers: State-of-the-art Natural Language Processingcited by 2,201
  11. 2022BLOOM: A 176B-Parameter Open-Access Multilingual Language Modelcited by 1,968
  12. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,359
13 more
  1. 2022STaR: Bootstrapping Reasoning With Reasoningcited by 895
  2. 2021Datasets: A Community Library for Natural Language Processingcited by 526
  3. 2022Autoformalization with Large Language Modelscited by 252
  4. 2023The BigScience ROOTS Corpus: A 1.6TB Composite Multilingual Datasetcited by 148
  5. 2018Character-Level Language Modeling with Deeper Self-Attentioncited by 138
  6. 2017Rasa: Open Source Language Understanding and Dialogue Managementcited by 67
  7. 2020Teaching Temporal Logics to Neural Networkscited by 51
  8. 2022Formal Specifications from Natural Languagecited by 33
  9. 2020Learning a natural-language to LTL executable semantic parser for grounded roboticscited by 22
  10. 2021DeepSTL -- From English Requirements to Signal Temporal Logiccited by 22
  11. 2021Neural Circuit Synthesis from Specification Patternscited by 17
  12. 2023Iterative Circuit Repair Against Formal Specificationscited by 9
  13. 2021Generating Symbolic Reasoning Problems with Transformer GANscited by 5

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2023: 5; 2024: 11; 2025: 20; 2026: 21.

57 papers.

Sort:

By area:

  1. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  2. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  3. 2024Autoformalizing Euclidean Geometrycited by 27
  4. 2023Conformal Temporal Logic Planning using Large Language Modelscited by 21
  5. 2025VeriSafe Agent: Safeguarding Mobile GUI Agent via Logic-based Action Verificationcited by 20
  6. 2024LLM4SecHW: Leveraging Domain Specific Large Language Model for Hardware Debuggingcited by 18
  7. 2024Verifiably Following Complex Robot Instructions with Foundation Modelscited by 15
  8. 2025VeriCoder: Enhancing LLM-Based RTL Code Generation through Functional Correctness Validationcited by 11
  9. 2025We'll Fix it in Post: Improving Text-to-Video Generation with Neuro-Symbolic Feedbackcited by 9
  10. 2025ConformalNL2LTL: Translating Natural Language Instructions into Temporal Logic Formulas with Conformal Correctness Guaranteescited by 9
  11. 2024Guiding LLM Temporal Logic Generation with Explicit Separation of Data and Controlcited by 8
  12. 2026Agentic Trading: When LLM Agents Meet Financial Marketscited by 7
38 more
  1. 2025HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinementcited by 6
  2. 2025Grammar-Forced Translation of Natural Language to Temporal Logic using LLMscited by 6
  3. 2023Co-audit: tools to help humans double-check AI-generated contentcited by 5
  4. 2024Towards Logically Sound Natural Language Reasoning with Logic-Enhanced Language Model Agentscited by 5
  5. 2024Generative Agents for Multi-Agent Autoformalization of Interaction Scenarioscited by 5
  6. 2025LogiDebrief: A Signal-Temporal Logic based Automated Debriefing Approach with Large Language Models Integrationcited by 5
  7. 2025Hybrid-NL2SVA: Integrating RAG and Finetuning for LLM-based NL2SVAcited by 5
  8. 2025QuArch: A Question-Answering Dataset for AI Agents in Computer Architecturecited by 4
  9. 2025Verifiable Natural Language to Linear Temporal Logic Translation: A Benchmark Dataset and Evaluation Suitecited by 4
  10. 2025QuadSentinel: Sequent Safety for Machine-Checkable Control in Multi-agent Systemscited by 4
  11. 2023Trusta: Reasoning about Assurance Cases with Formal Methods and Large Language Modelscited by 3
  12. 2024NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesiscited by 3
  13. 2024CoT-TL: Low-Resource Temporal Knowledge Representation of Planning Instructions Using Chain-of-Thought Reasoningcited by 3
  14. 2025PAT-Agent: Autoformalization for Model Checkingcited by 3
  15. 2025Formalising Software Requirements using Large Language Modelscited by 2
  16. 2025Can LLMs Generate User Stories and Assess Their Quality?cited by 2
  17. 2025Synthesizing Precise Protocol Specs from Natural Language for Effective Test Generationcited by 2
  18. 2023Towards Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal cross- and self-attention Large Language Model Approachcited by 1
  19. 2025Bridging Logic and Learning: Decoding Temporal Logic Embeddings via Transformerscited by 1
  20. 2025Bounded PCTL Model Checking of Large Language Model Outputscited by 1
  21. 2025Verifying Memoryless Sequential Decision-making of Large Language Modelscited by 1
  22. 2026Structural-Ambiguity-Aware Translation from Natural Language to Signal Temporal Logiccited by 1
  23. 2026Intent-aligned Formal Specification Synthesis via Traceable Refinementcited by 1
  24. 2026ReasonSTL: Bridging Natural Language and Signal Temporal Logic via Tool-Augmented Process-Rewarded Learningcited by 1
  25. 2026SCP-NL2TL: Selective Conformal Prediction with Semantic Verification for Natural Language to Temporal Logic Specificationscited by 1
  26. 2024Nl2Hltl2Plan: Scaling Up Natural Language Understanding for Multi-Robots Through Hierarchical Temporal Logic Task Representationcited by 0
  27. 2024Robot Tasks with Fuzzy Time Requirements from Natural Language Instructionscited by 0
  28. 2025AutoICE: Automatically Synthesizing Verifiable C Code via LLM-driven Evolutioncited by 0
  29. 2025GinSign: Grounding Natural Language Into System Signatures for Temporal Logic Translationcited by 0
  30. 2026Exploring Plan Space through Conversation: An Agentic Framework for LLM-Mediated Explanations in Planningcited by 0
  31. 2026Talking with Verifiers: Automatic Specification Generation for Neural Network Verificationcited by 0
  32. 2026LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoningcited by 0
  33. 2026Evaluating the Formal Reasoning Capabilities of Large Language Models through Chomsky Hierarchycited by 0
  34. 2026Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specificationscited by 0
  35. 2026Coherency through formalisations of Structured Natural Language, A case study on FRETishcited by 0
  36. 2026Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Modelscited by 0
  37. 2026NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logiccited by 0
  38. 2026Translating Natural Language to Strategic Temporal Specifications via LLMscited by 0

50 most cited of 57 All 57 (JSON)