桥接自然语言与形式规范——基于层次语义分解的 LLM 自动将软件需求翻译为 LTL
软件工程
2025-12-22 v1
摘要
自动将自然语言 (NL) 软件需求翻译为形式规范，仍是扩大形式验证实践在工业领域应用，尤其是安全关键领域的关键挑战。现有方法（规则导向和学习导向）面临显著局限。虽然大型语言模型 (LLM) 如 GPT-4o 在语义提取方面表现突出，但仍难以应对真实工业需求的复杂性、歧义性和逻辑深度。在本文中，我们提出 Req2LTL，一个模块化框架，通过层次中间表示 OnionL 桥接 NL 与线性时序逻辑 (LTL)。Req2LTL 利用 LLM 进行语义分解，并结合确定性规则综合以确保语法有效性和语义忠实性。我们的全面评估表明，Req2LTL 在真实航空需求上实现了 88.4% 的语义准确率和 100% 的语法正确性，显著优于现有方法。
引用
@article{arxiv.2512.17334,
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},
journal= {arXiv preprint arXiv:2512.17334},
year = {2025}
}