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
• Authors: Zhi Ma, Cheng Wen, Zhexin Su, Xiao Liang, Cong Tian, Shengchao Qin, Mengfei Yang,
• 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

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