💻 computer science

Automated LTL Specification Generation from Industrial Aerospace Requirements

本文提出了 AeroReq2LTL 框架，利用大语言模型结合术语标准化词典与模板化需求语言，成功解决了工业级航空航天自然语言需求向线性时序逻辑（LTL）属性自动转换中存在的术语复杂与隐含逻辑难以捕捉的难题，并在真实数据集上实现了高精度与高召回率的验证效果。

原作者： Zhi Ma, Xiao Liang, Cheng Wen, Rui Chen, Bin Gu, Shengchao Qin, Cong Tian, Mengfei Yang

发布于 2026-04-24

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Zhi Ma, Xiao Liang, Cheng Wen, Rui Chen, Bin Gu, Shengchao Qin, Cong Tian, Mengfei Yang

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

这篇论文介绍了一个名为 AeroReq2LTL 的“智能翻译官”，它的任务是帮航空航天工程师把人类写的自然语言需求（比如“如果太阳没被检测到，就切换模式”），自动翻译成计算机能严格验证的逻辑公式（LTL）。

为了让你更容易理解，我们可以把整个过程想象成给一个不懂行情的“超级 AI 翻译官”配备一本“行业字典”和一套“填空模板”。

1. 为什么要造这个工具？（痛点：翻译的“水土不服”）

想象一下，你有一个非常聪明的 AI 翻译官（大语言模型，LLM），它读过很多书，逻辑很强。现在，你让它把一份航天飞机的操作手册翻译成给机器执行的代码指令。

普通场景：如果手册写的是“红灯亮了，车不能走”，AI 能轻松翻译成 红灯 -> 不能走。
航天场景：手册里写的是“如果所有轴上的角速率绝对值连续 44.8 秒小于 0.15 度/秒，或者速率阻尼模式持续 128 秒，工作模式从速率阻尼切换到俯仰搜索”。

问题出在哪？

黑话太多：AI 不知道“角速率”、“速率阻尼”具体对应代码里的哪个变量（比如 dwCount 或 flagSP）。就像让一个不懂中医的人翻译“气虚”，他可能翻译成“没力气”，但医生需要的是具体的“脉象数据”。
潜台词太多：工程师写“切换到..."，意思是“下一秒立刻切换”。但 AI 可能会理解成“以后某个时间切换”，这就差之毫厘，谬以千里了。
上下文缺失：需求文档里，一段话旁边可能还有一张表格，写着变量的定义。AI 如果只看那段话，不看表格，就会“断章取义”。

结果就是：AI 翻译出来的指令，要么逻辑不通，要么跟实际硬件对不上，导致航天器可能出大事故。

2. AeroReq2LTL 是怎么解决的？（两大法宝）

为了解决这个问题，作者给 AI 翻译官配了两样神器：

法宝一：SpaceKG（行业专属“翻译字典”）

比喻：这就像给翻译官发了一本航天术语对照表。
作用：当文档里出现“角速率小于 0.15"时，SpaceKG 会立刻告诉 AI：“别瞎猜了，这在代码里对应的是变量 dwCount，而且它的单位是秒。”
效果：它把模糊的“人话”强行映射成精确的“代码变量”，防止 AI 把“太阳”翻译成“星星”，或者把“时间”翻译成“温度”。

法宝二：SpaceRDL（带填空的“逻辑模板”）

比喻：这就像给翻译官发了一张填空题试卷，而不是让他自由发挥写文章。
作用：SpaceRDL 强制要求 AI 把需求拆解成固定的结构：
- 在什么模式下？（工作模式）
- 什么条件触发？（条件）
- 什么时候发生？（时间：是“立刻”还是“下一秒”？）
- 做什么动作？（动作）
效果：通过这种“填空”，AI 被迫把那些没说出来的潜台词（比如“下一秒”、“立刻”）显性化地填进去。这样，原本模糊的“切换模式”，就被规范成了严谨的“如果满足条件，下一个周期立即切换”。

3. 工作流程（三步走）

整个系统的工作流程就像是一个精密的流水线：

第一步：双管齐下（收集情报）
- 系统不仅读取需求文档里的文字（目标流），还同时读取旁边的接口表格（知识流）。
- 比喻：就像翻译官一边读文章，一边手边放着字典和电路图，确保不遗漏任何背景信息。
第二步：改写与填空（标准化）
- 利用SpaceKG（字典）把专业术语替换成标准变量。
- 利用SpaceRDL（模板）把长句子拆解成填空结构，把隐性的时间逻辑显性化。
- 比喻：把“如果太阳没被检测到..."改写为“在 [搜索模式] 下，如果 [flagSP=FALSE] 且 [时间>720s]，则 [切换到翻滚搜索]"。
第三步：确定性翻译（生成公式）
- 最后，系统不再依赖 AI 的“随机发挥”，而是用一套死板的规则，把填好空的模板直接转换成数学逻辑公式（LTL）。
- 比喻：就像把填好的填空题，直接套用公式 G(条件 -> X(动作))，生成机器能读懂的“法律条文”。

4. 效果如何？（实战表现）

作者在真实的航天软件项目（ACS-LEOS，一种卫星姿态控制软件）中测试了这个工具：

准确率：达到了 85% 的精准度（Precision）和 88% 的召回率（Recall）。
对比：如果不加这两个法宝，直接用普通的 AI 翻译，准确率只有 35% 左右，几乎没法用。
落地：生成的公式可以直接被现有的工业验证工具（TRACE）拿来用，自动检查软件有没有 Bug。

总结

这篇论文的核心思想就是：在航天这种容错率为零的领域，不能只靠 AI“猜”逻辑。

AeroReq2LTL 就像是给 AI 戴上了专业眼镜（SpaceKG 字典）和紧箍咒（SpaceRDL 模板），强迫它把人类模糊的“行话”和“潜台词”，变成计算机能严格执行的“铁律”。这不仅省去了人工翻译的繁琐，更重要的是，它让航天软件的验证变得更加安全、可靠和自动化。

这篇论文介绍了一个名为 AeroReq2LTL 的自动化框架，旨在解决航空航天领域安全关键软件中，将自然语言（NL）需求转化为线性时序逻辑（LTL）规范时的痛点。以下是该论文的详细技术总结：

1. 问题背景与挑战 (Problem & Challenges)

在航空航天软件的开发与验证中，LTL 被广泛用于表达复杂的系统属性。然而，将自然语言需求转化为形式化 LTL 规范存在巨大的“形式化瓶颈”：

人工成本高且易错：传统方法依赖既懂航空航天控制工程又精通形式化方法的专家，过程耗时且容易出错。
现有工具失效：虽然现有的基于大语言模型（LLM）的工具（如 NL2SPEC, NL2TL 等）在合成基准测试中表现尚可，但在真实的工业文档中表现不佳。
工业需求的复杂性：
1. 上下文依赖：单一需求句子的含义往往依赖于接口描述表（Interface Description）中的信号定义、数据类型和控制周期，LLM 难以将这些分散的信息关联起来（上下文盲区）。
2. 领域术语歧义：工业文档包含大量专业术语和缩写，LLM 容易将其错误拆解为无意义的原子命题，或映射到错误的变量。
3. 隐式时序逻辑：需求中常隐含时序操作符（如“切换”隐含了下一时刻 $X$ 的状态变化），LLM 往往无法准确捕捉这些隐式约束，导致生成的规范在语义上偏离控制逻辑。

2. 方法论：AeroReq2LTL 框架 (Methodology)

AeroReq2LTL 是一个系统化的工程框架，通过两个核心工业创新模块，利用 LLM 的推理能力并加以约束，实现了从自然语言到 LTL 的自动化生成。其工作流程分为三个阶段：

阶段一：双流上下文重构 (Dual-stream Context Reconstructing)

为了解决上下文盲区，框架从原始 PDF 文档中提取两条互补的信息流：

目标流 (Target Stream)：提取完整的功能段落，保留控制周期等显式调用条件，而非孤立的句子。
知识流 (Knowledge Stream)：从关联的接口描述表中提取信号名称、数据类型、初始值和有效范围等元数据。

阶段二：NL 到模板化自然语言 (NL-to-TNL Rewriting)

这是核心处理阶段，将非结构化的自然语言转化为结构化的模板化自然语言 (Templated Natural Language, TNL)。

SpaceKG (领域知识图谱)：基于提取的知识流构建。它将复杂的工程谓词（如“角速度小于 0.15°/s"）映射为精确的代码级原子命题（如 dwCount > 44.8s）。通过 BERT 分类和专家映射，解决术语碎片化和变量映射错误问题。
SpaceRDL (结构化需求描述语言)：一种基于模板的语言，用于显式化隐式的时序和逻辑关系。它定义了如 workmode (工作模式), condition (条件), timing (时序), action (动作) 等强制字段。LLM 被引导将这些字段填入预定义模板中，从而将隐式前提（如“立即切换”）转化为显式的逻辑结构。

阶段三：TNL 到 LTL 转换 (TNL-to-LTL Converting)

利用确定性的翻译规则，将结构化的 TNL 直接映射为 LTL 公式。
由于 TNL 已经消除了歧义并显式化了时序，此步骤避免了 LLM 生成过程中的随机性，确保生成的 LTL 在语法和语义上均符合航空航天控制逻辑。

3. 关键贡献 (Key Contributions)

AeroReq2LTL 框架：首个专为航空航天工业需求设计的 LTL 自动生成框架，成功将 LLM 能力与领域工程实践相结合。
SpaceKG (领域数据字典)：一种自动从工程 artifacts（如接口表）中构建的知识库，能够将模糊的领域术语规范化为精确的原子命题，解决了“落地”问题。
SpaceRDL (模板化语言)：一种中间表示语言，通过强制结构化的语义模板，显式化了工业需求中隐含的时序逻辑（如 $X$ 算子）和逻辑关系，显著降低了 LLM 的推理难度。
端到端工具链集成：框架生成的 LTL 可直接被现有的工业验证工具（如 TRACE）消费，实现了从需求文档到可执行验证的完整闭环。

4. 实验结果 (Results)

研究团队在真实的低地球轨道卫星姿态控制软件（ACS-LEOS）的 Sun Search Control System (SSCS) 模块上进行了评估，包含 79 条生产级需求。

性能指标：
- AeroReq2LTL (基于 GPT-4o)：达到了 85% 的精确率 (Precision) 和 88% 的召回率 (Recall)。
- 对比基线：现有的 SOTA 工具（如 NL2SPEC, NL2LTL）结合最强 LLM (GPT-4o) 的精确率仅为 49%-61%，召回率也较低。直接提示（SimPro）的效果更差（约 19%-35%）。
消融实验：
- 移除 SpaceKG：精确率降至 69%，主要错误是术语映射错误（如混淆 flagSP 和 flagSPS）。
- 移除 SpaceRDL：精确率降至 52%，主要错误是时序结构缺失（如遗漏 $X$ 算子或错误放置逻辑前提）。
- 这证明了两个核心组件对于处理工业级复杂需求是不可或缺的。
验证工具集成：生成的 67 条正确 LTL 规范中，有 63 条成功通过了 TRACE 工具的运行时验证，证明了其生成的规范具有实际可用性。

5. 意义与影响 (Significance)

填补工业空白：解决了现有 NL-to-LTL 工具在真实工业场景中因缺乏领域知识和上下文理解而失效的问题。
降低门槛与成本：将原本需要专家手动完成的高难度形式化工作自动化，显著减少了航空航天软件验证的人力成本和错误率。
可推广性：虽然针对航空航天设计，但其基于工程 artifacts（接口表）构建知识库的思路，可推广至汽车、医疗等其他安全关键领域。
工程实践价值：该框架已实际应用于航天软件项目，并证明了其生成的规范可以直接进入现有的验证流水线，为高可靠性软件的自动化保障提供了切实可行的路径。

总结：AeroReq2LTL 通过引入领域知识图谱（SpaceKG）和结构化模板语言（SpaceRDL），成功克服了通用大模型在处理工业级复杂、隐含时序需求时的局限性，实现了高精度、可验证的 LTL 规范自动生成，是形式化方法在工业界落地的重要突破。