对比LLM与规则方法生成C程序形式化注解的验证效果
Evaluating LLM-Generated ACSL Annotations for Formal Verification
- 用规则脚本、Frama-C插件和3个大模型生成ACSL注解
- 规则方法验证成功率更高，LLM结果波动大但有潜力
- 适合关注自动化验证与AI辅助开发的研究者
形式化规范对构建可验证、可靠软件系统至关重要，但为真实世界C程序生成准确且可验证的规范仍具挑战。本文对自动化的ACSL注解生成策略进行实证评估，比较基于规则的Python脚本、Frama-C的RTE插件以及三个大语言模型（DeepSeek-V3.2、GPT-5.2、OLMo 3.1 32B Instruct）在单次注解生成上的表现。研究聚焦于直接应用于验证任务的一次性生成，使用过滤后的CASP基准数据集，通过Frama-C的WP插件结合多个SMT求解器评估生成注解，分析证明成功率、求解器超时及内部处理时间。结果显示，规则方法在验证成功率上更稳定可靠，而基于LLM的方法表现更不稳定；这些发现揭示了当前LLM在该任务中的局限性，也凸显其作为辅助工具的潜力。
原文摘要 · Abstract (English)
Formal specifications are crucial for building verifiable and dependable software systems, yet generating accurate and verifiable specifications for real-world C programs remains challenging. This paper presents an empirical evaluation of automated ACSL annotation generation strategies for C programs, comparing a rule-based Python script, Frama-C's RTE plugin, and three large language models (DeepSeek-V3.2, GPT-5.2, and OLMo 3.1 32B Instruct). The study focuses on one-shot annotation generation, assessing how these approaches perform when directly applied to verification tasks. Using a filtered subset of the CASP benchmark, we evaluate generated annotations through Frama-C's WP plugin with multiple SMT solvers, analyzing proof success rates, solver timeouts, and internal processing time. Our results show that rule-based approaches remain more reliable for verification success, while LLM-based methods exhibit more variable performance. These findings highlight both the current limitations and the potential of LLMs as complementary tools for automated specification generation.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。