LiveFMBench：揭示代理工作流在规范生成中的威力和局限性

正式规范对于严格的程序验证至关重要，但编写正确的规范仍然成本高昂且难以自动化。尽管 大语言模型 (LLM) 和代理已经显示出有希望的进展，但它们的真实功能和故障模式仍不清楚。我们提出了第一个针对 LLM 和基于代理的 C 程序正式规范生成的系统性和污染感知研究。我们推出 LiveFMBench，这是一个不断发展的 630 个 ACSL（ANSI/ISO C 规范语言）注释的 C 程序基准，其中包括 360 个新收集的案例，旨在减少数据泄漏。使用这个基准，我们评估不同采样大小的直接提示、推理（思维模式）推理、代理管道，并执行细粒度的故障分析。实验结果表明，朴素评估大大高估了性能，因为直接提示下的模型可能会表现出不忠实的行为，例如欺骗自动证明者或忽略代码上下文约束；排除此类情况后，真实规格生成精度下降约 20\%。我们进一步发现，增加采样和思维模式都可以显着提高成功率，较小的模型从思维模式中受益更多。代理管道在低采样预算和更困难的数据集上特别有效。故障分析进一步表明，不正确的循环不变量是主要错误类型，而代理管道显着减少了断言错误。这些结果暴露了当前基于 LLM 的方法的基本局限性，并表明它们距离取代人类编写的正式规范还很远。我们在 https://huggingface.co/datasets/fm-universe/Live-FM-Bench 上发布了 LiveFMBench 以及所有评估工件以支持未来的研究。