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

论文信息

@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的形式化能力

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

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

方法论的"五行分类法"

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

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

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

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

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

典型案例与工具

工具/框架	应用领域	核心方法	效果数据
Laurel	Dafny断言生成	定位代码缺失位置+示例提示	生成超50%辅助断言
AssertLLM	硬件验证断言	3个定制LLMs分阶段处理	89%正确断言率
SpecSyn	软件规范合成	序列到序列学习	准确率比前代工具高21%
nl2spec	自然语言转形式化	迭代细化翻译	开源实现+Web界面

方法论分类

类别	特点	代表研究
仅提示（Prompt-only）	直接使用LLM，无额外调优	GPT-3.5验证代码
提示+迭代/人机交互	结合人工反馈或链式推理	nl2spec、Chain-of-Thought
微调（Fine-tuned）	针对任务优化LLM参数	SpecSyn、Req2Spec
神经符号（Neuro-symbolic）	LLM+逻辑推理工具	SAT-LLM（SMT solver）
验证器集成（Verifier-in-loop）	LLM与验证工具联动	Lemur、Explanation-Refiner

关键研究发现

任务可靠性差异：断言生成（如Laurel的50%、AssertLLM的89%）比完整契约合成（如GPT-4o生成的VeriFast规范常失败）更可靠。
任务范围影响：小范围、明确任务（如单个断言）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）。