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

技术摘要：通过层次化语义分解桥接自然语言与形式化规范

问题陈述
将自然语言（NL）软件需求准确且自动化地翻译为形式化规范（特别是线性时序逻辑 LTL）是实现航空航天等安全关键工业领域形式化验证规模化应用的关键瓶颈。目前的工业实践高度依赖于人类专家的手动翻译，这一过程既耗时又易出错。虽然现有的自动化方法——从基于规则的系统到基于学习的方法——提供了一定程度的自动化，但它们面临着显著的局限性。基于规则的方法缺乏灵活性，难以应对自然语言的多变性；而基于学习的方法则往往难以泛化到训练数据之外。此外，最近的大型语言模型（LLMs）尽管在语义提取方面表现出色，但在处理现实工业需求中固有的隐式时序语义、深层嵌套逻辑结构以及特定上下文约束时仍显得力不从心。直接应用 LLMs 往往会导致“沉默失败（silent failures）”，即生成的公式在语法上是正确的，但由于误差累积和缺乏结构化验证，在语义上却是错误的。

方法论：REQ2LTL 框架
为了解决这些挑战，作者提出了 REQ2LTL，这是一个通过一种名为 OnionL 的新型层次化中间表示来连接自然语言与 LTL 的模块化框架。该框架通过一个两阶段流水线运行，结合了 LLM 的语义提取能力与确定性基于规则的合成保证。

1. 中间表示 (OnionL)：
   OnionL 是一种树状结构的中间语言，旨在显式编码时序语义、作用域和逻辑关系。它将需求分解为三个组成元素：

   • 原子命题 (APs)： 带有语义子字段（组件、变量、关系、公式）的谓词级事实。
   • 作用域 (Scopes)： 对应于一元算子（如 Globally、Eventually、Next）或基于模式的前件的上下文边界。
   • 关系 (Relations)： 连接子公式的逻辑或时序依赖关系（如 And、Or、Implies、Until）。
     该结构镜像了 LTL 的组合语法，作为一个语义桥梁，允许 LLM 专注于局部语义解析，同时将全局逻辑组合交给基于规则的机制。

2. 第一阶段：REQ2ONIONL（语义分解）：
   该模块利用提示引导的 LLM 将自由形式的自然语言需求转换为结构化的 OnionL 树。它采用了一种名为 BUILDING-ONIONL 的特定思维链（Chain-of-Thought）算法，该算法分为两个阶段运行：

   • 宏观结构提取： 识别全局时序或基于模式的作用域，以构建顶层节点。
   • 递归子句分解： 递归地将子句分解为嵌套的作用域、关系和归一化的原子命题。
     该过程由定义 OnionL 递归语法的知识库进行引导，并辅以工业模式的少样本（few-shot）示例进行强化。

3. 第二阶段：ONIONL2LTL（基于规则的合成）：
   该模块执行将经过验证的 OnionL 树转换为标准化 LTL 公式的一系列确定性的、基于规则的翻译。

   • 验证： 在翻译之前，系统通过深度优先遍历来验证结构的完备性（例如，算子的正确元数、有效的作用域嵌套）。针对安全关键型应用，该框架支持“人机协同（human-in-the-loop）”机制，通过 Mermaid 图表可视化 OnionL 结构，供工程师进行检查和修正。
   • 翻译： 后序遍历将每个节点转换为其对应的 LTL 语法（例如，将 Globally 映射为 $G$，将 Implies 映射为 $\rightarrow$）。这一过程确保了所有输出在构造上都是语法正确的。

核心贡献

• OnionL 中间表示： 一种显式编码时序语义和逻辑关系的层次化语言，充当了自然语言与 LTL 之间稳健的语义桥梁。
• 层次化语义分解： 一种两阶段、提示驱动的算法（BUILDING-ONIONL），能够系统地分解需求，显著提升了结构的完整性和语义准确性。
• REQ2LTL 框架： 一个结合了基于 LLM 的分解与确定性基于规则的翻译及验证的自动化流水线。与现有方法相比，它实现了更高的准确度和完美的语法正确性。

实验结果
作者在学术基准（Circuit、Navigation、Office Email）和包含 112 个航空航天需求的真实工业数据集上对 REQ2LTL 进行了评估。

• 工业性能： 在航空航天数据集上，REQ2LTL 实现了 88.4% 的语义准确率（精确匹配）和 100% 的语法正确性。这显著优于现有的先进基准方法（如 NL2SPEC、NL2LTL、NL2TL），后者在处理嵌套逻辑和隐式时序线索时表现挣扎，精确匹配率仅在 55% 到 65% 之间。
• 学术性能： 在学术基准测试中，REQ2LTL 展示了持续的高性能（二元准确率 >94%，BLEU >0.97），即使在歧义较小的设置下也能有效泛化。
• 消融研究： 实验证实，结构化建模（OnionL）、分阶段提示和验证反馈的结合是必不可少的。移除结构化中间表示会导致语义准确率降至 65.2%，而移除分阶段提示则会降至 58.9%。
• 错误分析： 该框架有效地消除了与时序误解、条件混淆和嵌套丢失相关的错误，这些错误在零样本（zero-shot）和其他基准方法中十分普遍。剩余的错误主要归因于输入需求中固有的语言歧义。

意义与主张
本文声称 REQ2LTL 有效地弥合了非正式自然语言需求与形式化规范之间的鸿沟，为在安全关键工业系统中实现规模化应用提供了实践基础。通过引入结构化中间表示和混合 LLM 与基于规则的架构，该框架缓解了直接使用 LLM 进行翻译的局限性，特别是解决了隐式时序语义和深层逻辑嵌套的挑战。作者强调，通过基于规则的合成确保 100% 语法正确性，结合高语义保真度的能力，使该框架成为工业验证工作流中可行的工具。此外，包含可视化的、人机协同的验证步骤解决了语言歧义问题，允许工程师在不破坏自动化流程的情况下高效地修正语义错误。作者指出，虽然目前的工作侧重于 LTL，但未来的扩展可以针对更具表达力的时序逻辑，如信号时序逻辑 (STL) 和度量时序逻辑 (MTL)。