基于 LLM 的基于自然语言要求的代码静态验证：行业经验报告

大语言模型 (LLM) 越来越多地用于生成需求规范、设计文档、代码和测试用例。相比之下，对更困难的保证问题的关注要少得多：静态验证实现的代码是否满足用自然语言编写的要求。传统的静态分析工具可以有效地检测编码缺陷和已知的漏洞模式，但它们无法确定程序行为是否符合预期的业务逻辑。检测此类缺陷需要对规范进行推理，而不仅仅是代码。软件测试可以暴露其中一些不匹配，但其有效性在很大程度上取决于测试设计、可执行工件和运行时环境。本文介绍了一个基于 LLM 的两阶段工作流程，用于解决智​​能车辆网络安全案例研究中的这一挑战。在第一阶段，基于人工智能的规则挖掘器从自然语言需求中提取可验证的规则，同时明确识别歧义、自相矛盾和其他不可验证的语句。在第二阶段，基于人工智能的代码审核员根据提取的规则检查实施证据。该工作流程不是要求单个 LLM 直接根据冗长的自然语言规范验证代码，而是引入结构化中间表示来减少幻觉、输出可变性、有限的可解释性和上下文丢失。由此产生的方法是一种需求感知和语义感知的静态分析形式，它补充了软件测试。通过分析需求和源代码而不需要编译、执行或运行时环境，该方法将验证和确认活动转移到了开发生命周期中。这种基于LLM的静态分析也是解决测试预言机问题的一种新方法。