[论文阅读] 人工智能 + 软件工程 | 用大语言模型架起软件需求形式化的桥梁

用大语言模型架起软件需求形式化的桥梁

论文信息

@misc{beg2025short,
    title={A Short Survey on Formalising Software Requirements with Large Language Models}, 
    author={Arshad Beg and Diarmuid O'Donoghue and Rosemary Monahan},
    year={2025},
    eprint={2506.11874},
    archivePrefix={arXiv},
    primaryClass={cs.SE}
}

一段话总结

本文是关于利用大语言模型（LLMs）辅助软件需求形式化的聚焦文献综述，介绍了从自然语言需求生成Dafny、C和Java等形式化规范的案例，如Laurel框架可生成超50%的Dafny辅助断言。研究通过多个学术数据库结合AI工具Elicit筛选文献，将现有方法分为“仅提示”“提示+迭代”“微调”等类别，指出断言生成可靠性高于完整契约合成，未来将聚焦提示工程、链思维推理及神经符号混合方法。

思维导图

研究背景：当自然语言遇上形式化验证的鸿沟

想象一下，你让朋友帮忙买杯咖啡，说"来杯冰美式，少糖"，结果收到一杯加了奶的热咖啡——这就是自然语言歧义在日常生活中的小麻烦。而在软件领域，这种歧义可能引发大问题：某自动驾驶系统的需求文档中"紧急情况下优先制动"的描述，因缺乏形式化定义，可能导致系统在雨天湿滑路面误判制动时机。

传统上，解决这个问题需要将自然语言需求转化为形式化规范（如Dafny、LTL逻辑公式），但这需要工程师同时掌握需求工程、形式化方法和定理证明，直接导致软件开发周期延长30%。就像让诗人同时成为数学家，既要懂"床前明月光"的意境，又要能推导微分方程。大语言模型（LLMs）的出现，就像给这位"诗人"配备了智能数学助手——既能理解自然语言的语义，又能生成严谨的形式化表达式，这正是本文研究的核心课题：如何用LLMs打通自然语言需求到形式化验证的"任督二脉"。

创新点：LLM如何改写需求形式化的游戏规则

这篇综述的独特价值在于，它首次系统梳理了LLM在软件需求形式化中的"十八般武艺"，并揭示了三个颠覆性创新：

1. 自动化断言生成的突破
传统上，工程师需要手动为代码添加断言（如Dafny中的assert语句），而Laurel框架通过LLM能自动生成超50%的辅助断言，就像IDE的智能补全功能突然学会了形式化逻辑。例如，在解析十进制字符串的Dafny函数中，LLM能自动生成"assert s1 + ‘.’ + s2 == [s1[0]] + (s1[1…] + ‘.’ + s2)"这样的关键断言，帮助验证器理解字符串分解逻辑。

2. 神经符号方法的融合魔法
SAT-LLM等框架将LLM与逻辑求解器（SMT solver）结合，就像让翻译家与数学家合作：LLM理解需求语义，SMT solver验证逻辑一致性。这种组合能以100%的精度检测需求冲突，而单纯使用ChatGPT的精度仅为60%左右。

3. 领域定制化的prompt工程
不同于通用LLM应用，文中提出的"双阶段提示法"（定位代码缺失位置+提供断言示例）如同给LLM戴上"领域眼镜"，使硬件验证断言生成正确率达到89%。这就像让GPT-4专门训练成"需求形式化专家"，而不是万能但不精的"百科全书"。

研究方法和思路：如何系统性探索LLM的形式化能力

文献综述的"三步淘金法"

1. 数据库地毯式搜索：在IEEE Xplore、ACM Digital Library等平台用"LLM+软件需求"等关键词搜索，结果差异巨大（Google Scholar返回1.48万篇，而IEEE Xplore仅17篇），突显精准筛选的重要性。
2. AI助手初筛：用Elicit工具自动提取论文摘要和DOI，将人工筛选量减少70%，就像用搜索引擎过滤海量信息。
3. 人工精挑细选：通过"是否涉及NLP与形式化方法结合"的标准，最终从数千篇文献中锁定35篇核心研究。

方法论的"五行分类法"

作者将现有研究分为五类，每类就像不同的"武器装备"：

• 仅提示（Prompt-only）：直接用LLM生成规范，如GPT-3.5验证代码是否符合需求。
• 提示+迭代：通过"思考步骤"引导LLM，类似教孩子做题时逐步引导。
• 模型微调：针对需求形式化任务优化LLM参数，如SpecSyn框架使规范生成准确率提升21%。
• 验证器集成：LLM与VeriFast等验证工具联动，实时检查规范可验证性。
• 神经符号混合：LLM与定理证明器结合，如Explanation-Refiner用LLM生成解释，再用定理证明器验证正确性。

案例研究的"显微镜观察"

以Dafny断言生成为例，研究团队解剖了LLM的工作机制：

1. 错误信息定位：通过Dafny验证器的错误信息，确定需要添加断言的代码位置。
2. 示例模式学习：给LLM提供代码库中的断言示例，如"确保整数部分正确提取"的形式化表达。
3. 增量验证：生成的断言会被插入代码中，由Dafny自动验证是否能解决原始错误。

典型案例与工具

方法论分类

关键研究发现

1. 任务可靠性差异：断言生成（如Laurel的50%、AssertLLM的89%）比完整契约合成（如GPT-4o生成的VeriFast规范常失败）更可靠。
2. 任务范围影响：小范围、明确任务（如单个断言）LLM表现更优，复杂系统级规范需迭代优化。

主要贡献：给领域带来的三大实在价值

1. 建立需求形式化的"武器库"

整理出35篇核心文献的工具矩阵，从Laurel（Dafny断言生成）到AssertLLM（硬件验证断言），再到nl2spec（自然语言转时序逻辑），就像为工程师提供了"需求形式化工具超市"，可根据项目类型（如航天软件、芯片设计）选择合适的LLM工具。

2. 揭示任务成功的"黄金法则"

通过对比研究发现：断言生成（如硬件验证中的89%正确率）比完整契约合成（如Java建模语言JML的50%正确率）更易成功。这提示工程师应优先将复杂需求拆解为小颗粒度的断言生成任务，如同将大工程拆分成可管理的子模块。

3. 绘制未来研究的"藏宝图"

明确指出三个高价值研究方向：

• 提示工程升级：用"链思维（CoT）"让LLM分步推导，如先分析需求语义再生成逻辑公式。
• 人机协同进化：开发"需求形式化IDE"，让工程师能实时纠正LLM生成的规范，类似程序员与AI结对编程。
• 安全关键领域深耕：针对自动驾驶等场景，将ISO 26262等安全标准嵌入LLM训练数据，确保生成的规范直接满足安全要求。

关键问题

问题1：LLMs在软件需求形式化中的主要方法论有哪些？

答案：主要包括“仅提示”（直接使用LLM，如GPT-3.5验证代码）、“提示+迭代/人机交互”（结合人工反馈或链式推理，如nl2spec）、“微调”（针对任务优化LLM参数，如SpecSyn）、“神经符号”（LLM与逻辑推理工具结合，如SAT-LLM集成SMT solver）及“验证器集成”（LLM与验证工具联动，如Lemur）。

问题2：现有LLM工具在形式化任务中的表现如何？

答案：断言生成工具表现更优，如Laurel可生成超50%的Dafny辅助断言，AssertLLM生成硬件验证断言的正确率达89%；而完整契约合成工具如GPT-4o生成的VeriFast规范常因冗余或验证失败表现不佳。

问题3：未来LLM在需求形式化中的关键研究方向是什么？

答案：核心方向包括高级提示工程（如链思维、结构化提示）、神经符号混合方法（LLM与定理证明器集成）、领域深度适配（如安全关键系统），以及通过行业与学术合作提升模型实用性。

未来研究方向

1. 高级提示工程：链思维（CoT）、结构化提示（SCoT）、自动提示生成（Automate-CoT）提升复杂任务推理能力。
2. 神经符号混合方法：LLM与定理证明器（如LeanDojo）、SMT solver集成，增强逻辑验证。
3. 领域深度适配：针对安全关键系统（如自动驾驶、航天）优化模型，结合行业需求。

总结：LLM让需求形式化从"奢侈品"变"日用品"

这篇综述就像一幅精密的导航图，展示了LLM如何将软件需求形式化从"只有少数专家能玩的高端游戏"变为"可规模化应用的工程实践"。通过35篇文献的系统分析，作者证明：LLM不仅能生成形式化规范，还能与定理证明器、验证工具深度融合，形成"需求理解-规范生成-自动验证"的闭环。

当然，挑战依然存在：如何让LLM理解安全关键领域的微妙语义（如航天软件中"故障容错"的形式化定义），如何处理跨多个模块的复杂需求，这些都需要未来研究持续突破。但可以肯定的是，LLM已成为需求形式化领域不可忽视的变革力量，就像编译器彻底改变了软件开发方式，LLM可能正在重塑需求工程的未来图景。