一句话：提出Req2LTL，用LLM分层语义分解与规则合成将自然语言需求自动翻译为LTL。
将自然语言软件需求自动翻译为形式规约，是在工业场景特别是安全关键领域推广形式验证的关键挑战。现有基于规则或学习的方法均存在明显局限，而GPT-4o等大语言模型虽擅长语义抽取，仍难以处理真实工业需求的复杂性、歧义性和逻辑深度。本文提出Req2LTL，一个连接自然语言与线性时序逻辑（LTL）的模块化框架，其核心是名为OnionL的层次化中间表示。该框架利用LLM进行语义分解，并结合确定性的基于规则的合成，以保证翻译结果的语法有效性和语义保真度。在真实航空航天需求上的综合评估表明，Req2LTL达到88.4%的语义准确率和100%的语法正确率，显著优于现有方法。
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 GPT4o 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.
@inproceedings{paperbot9462,
title = {Bridging Natural Language and Formal Specification–Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs},
author = {Zhi Ma and Cheng Wen and Zhexin Su and Xiao Liang and Cong Tian and Shengchao Qin and Mengfei Yang},
booktitle = {ASE},
year = {2025},
doi = {10.1109/ase63991.2025.00104}
}