LiveFMBench: 揭示基于智能体的工作流程在规范生成中的效能与局限
软件工程
2026-05-05 v1 人工智能
摘要
形式规范是严格程序验证的关键要素，但编写正确的规范仍然代价高昂且难以自动化。虽然大语言模型（LLM）和智能体已显示出有前景的进展，但其真实的能力与失效模式仍不明确。我们提出首个系统性且具备防篡改性的LLM和智能体驱动的C语言程序形式规范生成研究。我们引入LiveFMBench，一个持续演进的包含630个ACSL（ANSI/ISO C规范语言）标注C程序的基准测试，其中包括360个新收集的案例，以缓解数据泄露风险。通过该基准测试，我们评估了不同采样规模下的直接提示、推理启用（思考模式）推理、智能体管线，并进行细粒度失效分析。实验结果表明，粗略评估显著高估了性能，因为直接提示下的模型可能 exhibit 虚假行为，如欺骗自动证明器或忽略代码上下文约束；在排除此类案例后，真实的规范生成准确率下降约20%。进一步发现，增加采样次数和思考模式均显著提升成功率，小型模型从思考模式受益更大。智能体管线在低采样预算和更难数据集上尤其有效。失效分析进一步显示，错误的循环不变量是主要错误类型，而智能体管线显著减少断言错误。这些结果暴露了当前LLM方法的根本局限，表明它们距离取代人工编写的形式规范仍有很长的路要走。我们在https://huggingface.co/datasets/fm-universe/Live-FM-Bench上发布LiveFMBench及所有评估数据集，以支持未来研究。
引用
@article{arxiv.2605.01394,
title = {LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation},
author = {Dong Xu and Jialun Cao and Guozhao Mo and Junjie Hu and Cheng Wen and Hongyu Lin and Xianpei Han and Shengchao Qin and Cong Tian and Shing-Chi Cheung and Le Sun and Yaojie Lu},
journal= {arXiv preprint arXiv:2605.01394},
year = {2026}
}