Bridging Natural Language and Formal Specification--Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs

• URL: http://arxiv.org/abs/2512.17334v1
• Date: Fri, 19 Dec 2025 08:25:54 GMT
• Title: Bridging Natural Language and Formal Specification--Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs
• Abstract summary: Req2LTL is a modular framework that bridges NL and Linear Temporal Logic.<n>It achieves 88.4% semantic accuracy and 100% syntactic correctness on real-world aerospace requirements.
• Score: 10.958536923155101
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automating the translation of natural language (NL) software requirements into formal specifications remains a critical challenge in scaling formal verification practices to industrial settings, particularly in safety-critical domains. Existing approaches, both rule-based and learning-based, face significant limitations. While large language models (LLMs) like GPT-4o demonstrate proficiency in semantic extraction, they still encounter difficulties in addressing the complexity, ambiguity, and logical depth of real-world industrial requirements. In this paper, we propose Req2LTL, a modular framework that bridges NL and Linear Temporal Logic (LTL) through a hierarchical intermediate representation called OnionL. Req2LTL leverages LLMs for semantic decomposition and combines them with deterministic rule-based synthesis to ensure both syntactic validity and semantic fidelity. Our comprehensive evaluation demonstrates that Req2LTL achieves 88.4% semantic accuracy and 100% syntactic correctness on real-world aerospace requirements, significantly outperforming existing methods.

Related papers

• Automatic Translation of Unstructured Requirements into Linear Temporal Logic through Large Language Models [46.28810845443601]
  This paper evaluates whether contemporary off-the-shelf Large Language Models (LLMs) can help bridge this gap by generating Linear Temporal Logic (LTL) formulas directly from unstructured requirements.<n>The study examines six modern LLMs using a few-shot prompting strategy on a heterogeneous benchmark of 15 structurally varied requirements.<n>The results indicate that current general-purpose LLMs can achieve practically significant performance on the unstructured NLto-LTL task without task-specific fine-tuning.
  arXiv  Detail & Related papers  (2026-08-06T17:13:07Z)
• ClarifyCodeBench: Evaluating LLMs on Clarifying Ambiguous Requirements for Code Generation [54.788849448970154]
  We introduce ClarifyCodeBench, a novel interactive benchmark for evaluating Large Language Models' capability in resolving requirement ambiguity.<n>We conduct a systematic evaluation of six state-of-the-art LLMs using ClarifyCodeBench.<n>Our empirical results yield three critical insights: 1) Capability Decoupling: Strong code generation performance does not inherently translate to effective requirement clarification; 2) The Reasoning Paradox: While increased computational thinking enhances code correctness, it yields marginal gains in identifying ambiguities.
  arXiv  Detail & Related papers  (2026-07-01T09:58:59Z)
• ReasonSTL: Bridging Natural Language and Signal Temporal Logic via Tool-Augmented Process-Rewarded Learning [5.961092142323502]
  textscReasonSTL is a tool-augmented framework that adapts local open-source language models for natural-language-to-STL generation.<n>textscReasonSTL decomposes the translation process into explicit reasoning, deterministic tool calls, and structured formula construction.<n>Experiments show that a 4B model trained with textscReasonSTL achieves state-of-the-art performance in both automatic metrics and human evaluations.
  arXiv  Detail & Related papers  (2026-05-07T16:07:30Z)
• ClarifySTL: An Interactive LLM Agent Framework for STL Transformation through Requirements Clarification [41.040507019193775]
  Signal Temporal Logic (STL) is a formal language for specifying real-time behaviors of cyber-physical systems.<n>Recent efforts leveraging large language models (LLMs) have demonstrated impressive performance, but some natural language requirements contain vague or ambiguous information.<n>We propose ClarifySTL, an interactive LLM-agent framework that enhances STL transformation through requirements clarification.
  arXiv  Detail & Related papers  (2026-05-02T02:55:06Z)
• Assessing the Impact of Requirement Ambiguity on LLM-based Function-Level Code Generation [14.755517753769837]
  We introduce Orchid, the first code generation benchmark specifically designed with ambiguous requirements.<n>It comprises 1,304 function-level tasks covering four distinct types of ambiguity: lexical, syntactic, semantic, and vagueness.<n>Our results demonstrate that ambiguity consistently degrades the performance of all evaluated LLMs, with the most pronounced negative effects observed in highly advanced models.
  arXiv  Detail & Related papers  (2026-04-23T10:07:33Z)
• Automated LTL Specification Generation from Industrial Aerospace Requirements [21.94000502237098]
  We present AeroReq2LTL, a framework that automates property generation using large language models (LLMs)<n>On a real aerospace dataset, AeroReq2LTL achieves 85% recall in generation, and its outputs can be directly consumed by existing verification tools.
  arXiv  Detail & Related papers  (2026-04-21T01:20:33Z)
• Evaluating the Formal Reasoning Capabilities of Large Language Models through Chomsky Hierarchy [62.32144504442516]
  It is unknown whether SOTA LLMs can grasp the structured, hierarchical complexity of formal languages.<n>ChomskyBench is a benchmark for systematically evaluating LLMs through the lens of Chomsky Hierarchy.<n>ChomskyBench is composed of a comprehensive suite of language recognition and generation tasks designed to test capabilities at each level.
  arXiv  Detail & Related papers  (2026-04-03T04:06:39Z)
• Semantically Labelled Automata for Multi-Task Reinforcement Learning with LTL Instructions [61.479946958462754]
  We study multi-task reinforcement learning (RL), a setting in which an agent learns a single, universal policy.<n>We present a novel task embedding technique leveraging a new generation of semantic translations-to-automata.
  arXiv  Detail & Related papers  (2026-02-06T14:46:27Z)
• Connecting the Dots: Training-Free Visual Grounding via Agentic Reasoning [63.109585527799005]
  GroundingAgent is a visual grounding framework that operates without task-specific fine-tuning.<n>It achieves an average zero-shot grounding accuracy of 65.1 % on widely-used benchmarks.<n>It also offers strong interpretability, transparently illustrating each reasoning step.
  arXiv  Detail & Related papers  (2025-11-24T03:11:08Z)
• Towards Autoformalization of LLM-generated Outputs for Requirement Verification [0.6015898117103068]
  Autoformalization, the process of translating informal statements into formal logic, has gained renewed interest with the emergence of powerful Large Language Models.<n>This paper explores the use of a simple LLM-based autoformalizer to verify LLM-generated outputs against a small set of natural language requirements.<n>Our findings, while limited, suggest that autoformalization holds significant potential for ensuring the fidelity and logical consistency of LLM-generated outputs.
  arXiv  Detail & Related papers  (2025-11-14T19:45:17Z)
• Data Dependency-Aware Code Generation from Enhanced UML Sequence Diagrams [54.528185120850274]
  We propose a novel step-by-step code generation framework named API2Dep.<n>First, we introduce an enhanced Unified Modeling Language (UML) API diagram tailored for service-oriented architectures.<n>Second, recognizing the critical role of data flow, we introduce a dedicated data dependency inference task.
  arXiv  Detail & Related papers  (2025-08-05T12:28:23Z)
• From Legal Texts to Defeasible Deontic Logic via LLMs: A Study in Automated Semantic Analysis [1.5749416770494706]
  We present a novel approach to the automated semantic analysis of legal texts using large language models (LLMs)<n>We propose a structured pipeline that segments complex normative language into atomic snippets, extracts deontic rules, and evaluates them for syntactic and semantic coherence.
  arXiv  Detail & Related papers  (2025-06-10T15:25:19Z)
• ConformalNL2LTL: Translating Natural Language Instructions into Temporal Logic Formulas with Conformal Correctness Guarantees [10.687644259002674]
  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.
  arXiv  Detail & Related papers  (2025-04-22T20:32:34Z)
• $\texttt{SEM-CTRL}$: Semantically Controlled Decoding [53.86639808659575]
  $texttSEM-CTRL$ is a unified approach that enforces rich context-sensitive constraints and task- and instance-specific semantics directly on an LLM decoder.<n>texttSEM-CTRL$ allows small pre-trained LLMs to efficiently outperform larger variants and state-of-the-art reasoning models.
  arXiv  Detail & Related papers  (2025-03-03T18:33:46Z)
• Elevating Legal LLM Responses: Harnessing Trainable Logical Structures and Semantic Knowledge with Legal Reasoning [19.477062052536887]
  We propose the Logical-Semantic Integration Model (LSIM), a supervised framework that bridges semantic and logical coherence.<n>LSIM comprises three components: reinforcement learning predicts a structured fact-rule chain for each question, a trainable Deep Structured Semantic Model (DSSM) retrieves the most relevant candidate questions and in-answer learning generates the final answer.<n>Our experiments on a real-world legal dataset QA-validated through both automated metrics and human evaluation-demonstrate that LSIM significantly enhances accuracy and reliability compared to existing methods.
  arXiv  Detail & Related papers  (2025-02-11T19:33:07Z)
• Large Language Models are Interpretable Learners [53.56735770834617]
  In this paper, we show a combination of Large Language Models (LLMs) and symbolic programs can bridge the gap between expressiveness and interpretability. The pretrained LLM with natural language prompts provides a massive set of interpretable modules that can transform raw input into natural language concepts. As the knowledge learned by LSP is a combination of natural language descriptions and symbolic rules, it is easily transferable to humans (interpretable) and other LLMs.
  arXiv  Detail & Related papers  (2024-06-25T02:18:15Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  We propose a model-free RL algorithm that enables the use of Linear Temporal Logic (LTL) to formulate a goal for unknown continuous-state/action Markov Decision Processes (MDPs) The algorithm is guaranteed to synthesise a control policy whose traces satisfy the specification with maximal probability.
  arXiv  Detail & Related papers  (2019-02-02T20:09:32Z)

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.