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

TL;DR

This paper introduces Req2LTL, a framework that uses hierarchical semantic decomposition and LLMs to translate natural language software requirements into formal LTL specifications, improving accuracy and reliability.

Contribution

The paper presents Req2LTL, a novel modular approach combining LLMs and rule-based synthesis with hierarchical semantics for translating NL to LTL.

Findings

Achieves 88.4% semantic accuracy on aerospace requirements

Attains 100% syntactic correctness

Outperforms existing translation methods

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.