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

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

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 19 Dec 2025.

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

- [Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction](https://mlsanity.com/paper/2602.04892/) (2026)
- [Toward Safe LLM Agents: A Survey of Specification, Verification, and Enforcement](https://mlsanity.com/paper/2608.14590/) (2026)
- [Semantic Constraint Synthesis for Adaptive Trajectory Optimization via Large Language Models](https://mlsanity.com/paper/2606.04123/) (2026)
- [LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning](https://mlsanity.com/paper/2603.05728/) (2026)
- [Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications](https://mlsanity.com/paper/2604.18228/) (2026)
- [LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation](https://mlsanity.com/paper/2605.01394/) (2026)
- [Provably Secure Agent Guardrail](https://mlsanity.com/paper/2605.29251/) (2026)
- [Specification-Guided Synthesis of Deadlock-Free Communication Protocol Refinements with Large Language Models](https://mlsanity.com/paper/2607.27964/) (2026)
- [MENTOR: Procedural Shielding of Tool-Using LLM Agents](https://mlsanity.com/paper/2610.17039/) (2026)

## Abstract (arXiv)

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.