用大语言模型对照自然语言需求做代码静态验证：一份工业经验报告

用大语言模型对照自然语言需求做代码静态验证：一份工业经验报告（中文全译）

翻译说明：本文是 arXiv 论文 LLM-Based Static Verification of Code Against Natural-Language Requirements: An Industrial Experience Report（arXiv:2605.17926，2026-05-18 提交，v1）的中文全译，由智测团队翻译。原作者：Zhi Quan Zhou（蔚来 NIO Inc.）、Dave Towey（宁波诺丁汉大学）、Tsong Yueh Chen（斯威本科技大学）。原文以 CC BY 4.0 许可发布，允许翻译与再分发，须署名。译文保留原文全部章节、数据与结论；参考文献列表从略，文内引注编号保留。模型名、工具名、数据字段名保留英文。原文索引词中的拼写（Static anslysis、cosnsitency）按原文保留并在括号中注明。

摘要

大语言模型（LLM）越来越多地被用来生成需求规格、设计文档、代码和测试用例。相比之下，一个更难的保障问题得到的关注少得多：静态地验证已实现的代码是否满足用自然语言写成的需求。Coverity、SonarQube 这类传统静态分析工具擅长发现编码缺陷和已知漏洞模式，但无法判断程序行为是否符合预期的业务逻辑。例如，一个本应做乘法、实际却用加法实现的程序，可能既没有内存安全缺陷，也没有可识别的漏洞特征。发现这类缺陷需要针对规格说明进行推理，而不是只看代码本身。软件测试能暴露其中一部分不一致，但其效果高度依赖测试设计、可执行产物和运行环境。许多业务逻辑缺陷除非充分行使边界情况或很大的输入空间，否则仍然很难被发现。

本文给出一套两阶段、基于 LLM 的工作流，用来在智能汽车网络安全案例中处理这一挑战。第一阶段，一个基于 AI 的规则挖掘器从自然语言需求中抽取可验证规则，并显式标出歧义、自相矛盾以及其他不可验证的陈述。抽取规则的完整性通过一条简单的蜕变关系来增强。第二阶段，一个基于 AI 的代码审计器对照抽取出的规则检查实现证据。这种分离是有意为之。工作流没有让单个 LLM 直接拿冗长的自然语言规格去验证代码，而是引入结构化的中间表示，以降低幻觉、输出不稳定、可解释性不足和上下文丢失。由此得到的方法可以看成一种面向需求、面向语义的静态分析，它补充而不是取代软件测试。由于分析需求和源代码时不需要编译、执行或运行环境，该方法把相当一部分验证与确认活动左移到开发生命周期的更早阶段。可公开的案例材料表明，把需求澄清和面向业务逻辑的代码验证结合起来在实践中有用，并且能够验证超过 50% 此前只能靠软件测试来评估的需求。这项研究也表明，基于 LLM 的静态分析是处理测试 oracle 问题的一条新途径。

索引词：静态分析（原文拼写作 Static anslysis）、LLM、规格与实现的一致性（原文拼写作 cosnsitency）、规则挖掘、代码审计、业务逻辑、功能正确性、蜕变关系、网络安全需求、oracle 问题

I 引言

LLM 现在已经被常规地用在软件生命周期的各处，包括需求起草、设计支持、代码生成和测试生成。更广泛地说，用自然语言处理做需求工程已经相当成熟，但歧义处理、形式化和可追溯性仍然是持续存在的挑战 [4, 6]。然而，少得多的工作考察过：在不使用动态测试的情况下，已实现的代码是否符合仍然用自然语言书写的规格。这一局限在工业安全和网络安全场景中尤其重要。许多与安全、安全相关的行为仍然主要用散文定义，实现是否正确取决于需求的预期功能含义，而不只是局部的编码质量。

传统工具的局限很直接。Coverity、SonarQube 等静态分析器擅长识别编码缺陷、不安全模式和已知漏洞类别，但并不确立已实现行为是否匹配功能规格。考虑一个简单例子：若程序本应计算乘法，实现却做了加法，代码里可能没有内存安全问题、没有可疑的 API 用法，也没有可识别的漏洞模式。缺陷却是真实的，发现它需要把实现行为与规格相比较。同样的局限出现在网络安全业务逻辑中：需求可能规定系统生成的密码不得呈现可识别的模式，而实现仍然强加一种规则结构，例如第一位是字母、第二位是数字。传统的基于代码的扫描器发现不了这种需求与实现的不一致。理论上，动态测试可以发现这类缺陷；实践中，由于测试所用用例数量有限，这很难做到。与之相对，本工作的目标是发展一种面向需求、面向语义的静态分析方法论，对照需求规格检查源代码，而不要求程序执行。

本文针对智能汽车网络安全软件中上述依赖规格的验证问题，给出一项工业案例研究和一套工作流。第一个 AI 智能体 ruleMiner 逐句分析需求，只保留既是规范性的、又可证伪的逻辑，产出可验证规则集，同时通过 requirements_specs_issues 这一数据结构暴露歧义、自相矛盾、措辞不清以及其他不可验证的内容。第二个 AI 智能体 codeAuditor 再对照抽取出的规则评估源代码，它对触发条件、约束、禁止状态和跨文件证据进行推理，而不是依赖浅层关键词匹配。

这种两阶段设计是核心的方法论选择，而不是实现上的方便。工作流没有让单个 LLM 直接判断代码是否满足一份很长的自然语言规格，而是引入显式的中间表示，使验证目标更窄、更可检查、更容易审计。这种分离有助于控制常见的 LLM 失败模式，包括幻觉、输出不稳定、可解释性不足和上下文丢失，同时保留工业目标：在同一条保障流水线里把需求澄清和实现验证连起来。

II 方法

工作流组织为两阶段验证流水线。第一阶段把自然语言需求转换成经过净化的、可验证的规则集，同时显式保留需求质量缺陷。为提高结果的完整性，AI 智能体 ruleMiner 利用下面这条蜕变关系：

MR1：当底层 LLM 的 temperature 设为最小值时，理想的规则挖掘器对同一输入在多次执行中应产生一致的输出。

然而我们的观察表明，即使 temperature 固定为 0，ruleMiner 在重复执行中仍可能产生不同输出。基于这一观察，我们采用一种汇集策略：对多次运行的输出进行调和，必要时加以合并，以得到更完整的已挖掘规则集。实验中 ruleMiner 被执行一到三次。蜕变关系的形式定义请读者参阅 Chen 等人 [3]。

第二阶段对照代码库中的实现证据检查所得规则。

第一、第二阶段分别由基于 LLM 的 AI 智能体 ruleMiner 和 codeAuditor 执行，如表 I 所示。

表 I：两阶段验证工作流

在需求一侧，ruleMiner 被指示只保留可强制执行的逻辑，通常是显式的 “shall”（应当）陈述，以及当上下文实际上使其成为强制要求时、与安全相关的 “should”（应该）陈述。这种从规范性文本中抽取操作性义务的做法，与先前把监管和政策规则用于需求工程的分析工作一致 [2]。解释性、许可性、示例性和主观性材料被排除在规则库之外。“random”（随机）、“strong”（强）、“lowest”（最低）或 “instantly”（立即）这类词，除非能落实到可度量的验证条件，否则不会被转成规则。同样，当一条需求包含内部冲突、未定义的操作状态或不完整的验收标准时，有问题的内容被记入 requirements_specs_issues 这一数据结构，而不是被翻译成一条会误导的规则。这种分离很重要，因为它防止有缺陷的需求文本悄悄污染下游的实现检查。

代码一侧的阶段建立在这套清理后的规则集之上。codeAuditor 主要依据每条规则的语义内容进行评估，导出具体的验证点，例如允许值和禁止值、最小长度、阈值计数、唯一性条件以及操作触发器。然后它对照源代码、配置、常量、校验逻辑和跨文件调用关系检查这些点。有代表性的以代码为中心的安全分析，包括代码属性图方法，对结构性漏洞发现很有力，但它们并不是为了判断实现语义是否满足自然语言业务规则而设计的 [5]。一条规则不会仅仅因为代码里出现了暗示性的标识符、注释或孤立检查，就被当成已满足。反过来，一条禁止也不会仅仅因为代码库某处存在相关功能，就被当成已违反；分析要寻找的是实际的使能路径、可达行为或不安全回退的证据。在这个意义上，工作流是由业务逻辑驱动的，而不是基于模式的。

III 工业案例研究与观察

源材料描述的是一项可公开讨论其安全性的工业案例，涉及车载 WiFi 安全子系统。需求一侧的一个代表性例子是密码策略文本：它要求大写字母、小写字母、数字和特殊字符，同时又错误地给了一个实际上并不满足这些条件的示例模式。ruleMiner 没有把这句话转换成一条看起来精确的验证规则，而是把它作为矛盾内容记入 requirements_specs_issues。这一区分在实践中很重要：流水线不会通过过度规范化，把规格缺陷藏进看起来机器可检查、语义上却不可靠的规则里。值得注意的是，这一需求缺陷未被发现超过一年。

第二个经过脱敏的例子说明需求侧的不确定性如何与代码侧证据相互作用。有一条需求说，当系统 “not in use”（未在使用）时，WiFi 热点应自动关闭，但触发状态定义得不够精确，无法仅凭规格做无歧义的验证。因此需求侧结果被标为低置信，而不是当成一条完全稳定的规则。即便如此，随后的代码审计报告了一处高置信的不匹配：已实现的触发依赖的是某些局部不活跃条件，而不是整个系统 “未在使用”；同时没有发现与需求似乎暗示的更广运行状态相集成的证据。更一般地，分析检查的是已实现的触发逻辑和可达行为，而不是仅仅匹配需求短语或暗示性标识符。这揭示的是需求缺陷，而不是编码 bug。

目前可用的定量结果应被理解为初步结果，而不是基准声明。需求一侧，更广的分析在 222 个被分析条目中报告了 75 个需求问题。对所审查的 WiFi 安全需求子集，人工检查没有发现不正确的已抽取规则。召回率没有评估，因为在那个规模上做穷尽的完整性检查需要大量额外的人工。

代码一侧（注意代码库是成熟的，因为它通过了此前的测试），对 WiFi 代码库的分析产生了 8 个 Fail/Unknown 发现。在人工检查过的发现中，没有观察到假阳性，并检测到一个高优先级编码问题，随后由开发团队修复。少数有争议的情况并没有被归因于验证技术本身的失败；它们来自不完整的需求到实现映射，以及缺失的跨部门可追溯性信息，这限制了对某些发现做确定性解释。这一区分很重要，因为它有助于把组织可追溯性上的缺口与底层验证方法的局限分开。

IV 讨论与经验

这项研究得出三条经验。第一，需求分析应当显式建模需求文本自身的缺陷。requirements_specs_issues 这一数据结构是必要的，因为它把可强制执行的逻辑，与矛盾、有歧义或规格不足的陈述分开；没有这种分离，自动检查会制造虚假的信心。

第二，对含义依赖于运行上下文的网络安全需求，面向业务逻辑的代码审计常常是必要的。实践中，重要缺陷不仅来自缺失的关键词或局部语法违规，也来自不匹配的触发条件、部分执行或错误的执行路径。因此最有用的分析是关于预期行为的推理，而不只是文本相似。这对难以通过测试暴露的缺陷尤其相关，特别是当合适的测试 oracle 很难定义，或有意义的评估需要许多生成样本时 [1]。因此，一种面向语义的静态分析方法论可以补充动态测试：在开发生命周期更早的时候暴露需求与实现的不一致，而不需要编译、执行或目标运行环境。目标不是取代测试，而是引入左移的验证能力，既能减少某些类别缺陷的测试工作量，也能识别传统基于代码的扫描器并不打算检测的问题。在本案例中，所提出的静态分析流水线能够验证超过 50% 此前只能通过软件测试评估的需求。此外，该方法可能有助于缓解测试 oracle 问题 [1]，因为基于 LLM 的分析工具链推理的是源代码语义和实现逻辑，而不是只依赖程序的期望输出。

第三，需求分析和实现分析在被当成耦合过程时最有效。需求越来越多地不仅由人类工程师消费，也由 AI 辅助工作流消费，而后者对歧义、矛盾和缺失的可追溯性没那么稳健。因此一条重要的工业经验是：需求应当清晰、无歧义、不自相矛盾，并且需求与代码库之间的映射——尤其是合并请求和变更历史的可追溯性——应当完整。这些关切与基于自然语言处理的需求工程中的长期观察一致，特别是围绕歧义管理和可追溯性 [4, 6]。对高质量可追溯性的依赖在工业环境中非常显眼，但在学术讨论中常常被低估。

IV-A 未来工作

需求侧当前的质量控制依赖于上文描述的规则净化标准，以及对本报告所考察的 WiFi 安全需求集的人工检查。ruleMiner 只保留可强制执行的逻辑，并把矛盾、有歧义或因其他原因不可验证的需求内容记录下来，而不是把这类内容翻译成规则。我们的智能体使用的 LLM 是 Claude Opus 4.6。

作为未来工作，蜕变关系和蜕变测试可以进一步用到规则挖掘上。一条直接的途径是提交同一需求在语义上等价的改写或释义，然后比较并在适当处合并所得规则集。更多蜕变关系可以包括添加或删除相关陈述，以验证挖掘出的规则是否相应变化，从而为 ruleMiner 的正确性和有效性提供证据。类似策略也可以用于 codeAuditor。原文 “Simlar” 为拼写，应为 Similar。

V 结论

本文报告了一套工业中由 LLM 辅助的工作流，用于检测网络安全需求与实现中的业务逻辑错误。核心想法是把可验证规则抽取与对 requirements_specs_issues 的显式记录耦合起来，随后做针对业务逻辑而不是浅层模式匹配的代码审计。蜕变关系被用来提高工具链的输出质量。所报告的案例材料表明，该工作流可以精确暴露大量矛盾或不可验证的需求，支持规则抽取，并识别实现层缺陷，其中包括成熟 WiFi 代码库中一个随后被修复的高优先级 bug。本研究没有评估规则挖掘的召回率和完整性。

尽管当前证据仍然是初步的、范围有限，所报告的经验表明：在统一工作流中集成需求澄清、可追溯性意识，以及基于 LLM 的、面向需求的静态分析，是工业保障中一个有希望的实践方向。更具体地说，该工作流应被理解为补充而非取代动态测试和传统静态分析工具。它通过不要求编译、执行或运行环境来支持左移验证，并且可能减少这样一类缺陷的测试工作量：它们的表现依赖于规格语义以及合适测试 oracle 是否可用，因而难以用常规测试用例暴露。这里的 “规格语义” 指的是需求所表达的预期约束和业务逻辑，而不是其表面措辞本身。

署名与许可

原文：Zhou, Z. Q., Towey, D., Chen, T. Y. LLM-Based Static Verification of Code Against Natural-Language Requirements: An Industrial Experience Report. arXiv:2605.17926, 2026-05-18. https://arxiv.org/abs/2605.17926

许可：Creative Commons Attribution 4.0 International（CC BY 4.0）。译文对原文的改动仅为语言转换；数据、结论与作者观点以原文为准。

译者：智测团队（OpenQA / openqa.cn）。