基于 LLM 的代码静态验证：一种工业经验报告
摘要
大语言模型 (LLM) 正在越来越多地用于生成需求规范、设计文档、代码和测试用例。相比之下，更少有人关注更困难的保证问题：静态验证实现的代码是否满足以自然语言书写的需求。传统静态分析工具擅长检测编码缺陷和已知漏洞模式，但无法确定程序行为是否匹配预期的业务逻辑。检测此类缺陷需要对规范进行推理。软件测试可暴露某些不匹配，但其有效性高度依赖测试设计、可执行制品和运行时环境。本文提出了针对智能车辆网络安全案例研究的两阶段 LLM 工作流程。第一阶段，AI 基于规则的矿工从自然语言需求中提取可验证规则，同时明确识别歧义、自相矛盾和其他不可验证语句。在第二阶段，AI 基于代码的审计员检查实现证据是否符合提取的规则。该工作流程不要求单一 LLM 直接验证代码与冗长自然语言规范，而是引入结构化的中间表示以减少幻觉、输出变异性、解释性有限和上下文丢失。 resulting approach is a requirement-aware and semantics-aware form of static analysis that complements software testing. By analyzing requirements and source code without requiring compilation, execution, or runtime environments, the method shifts verification and validation activities left in the development lifecycle. This LLM-based static analysis is also a new approach to addressing the test oracle problem.
关键词
引用
@article{arxiv.2605.17926,
title = {LLM-Based Static Verification of Code Against Natural-Language Requirements: An Industrial Experience Report},
author = {Zhi Quan Zhou and Dave Towey and Tsong Yueh Chen},
journal= {arXiv preprint arXiv:2605.17926},
year = {2026}
}