Evaluating LLM-Generated ACSL Annotations for Formal Verification

📄 arXiv: 2602.13851v1 📥 PDF

作者: Arshad Beg, Diarmuid O'Donoghue, Rosemary Monahan

分类: cs.SE, cs.AI

发布日期: 2026-02-14

备注: 12 pages. Submitted to Formal Techniques for Judicious Programming FTfJP-2026 at ECOOP. Under review

💡 一句话要点

评估LLM生成的ACSL注解在形式化验证中的有效性

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式化验证 ACSL规约 大型语言模型 代码生成 软件可靠性

📋 核心要点

  1. 为C程序生成准确可验证的形式化规约是难点，现有方法依赖人工或学习辅助，效率和准确性受限。
  2. 利用大型语言模型（LLM）自动生成ACSL规约，并使用形式化验证工具评估其质量，无需人工干预。
  3. 在包含506个C程序的数据集上，对比了五种ACSL生成系统，评估了注解质量、求解器敏感性和证明稳定性。

📝 摘要（中文）

形式化规约对于构建可验证和可靠的软件系统至关重要，但为实际C程序生成准确且可验证的规约仍然具有挑战性。本文实证评估了形式分析工具在无需人工或基于学习的辅助下，自动生成和验证ACSL规约的程度。我们对一个最近发布的包含506个C程序的数据集进行了受控研究，将其从交互式的、开发者驱动的工作流程重新用于自动化评估设置。比较了五个ACSL生成系统：一个基于规则的Python脚本、Frama-C的RTE插件，以及三个大型语言模型--DeepSeek-V3.2、GPT-5.2和OLMo 3.1 32B Instruct。所有生成的规约都在相同的条件下使用由多个SMT求解器驱动的Frama-C WP插件进行验证，从而可以直接比较注解质量、求解器敏感性和证明稳定性。我们的结果为自动化ACSL生成的性能和局限性提供了新的经验证据，补充了先前的基于调查的工作。

🔬 方法详解

问题定义：论文旨在解决为C程序自动生成ACSL（ANSI/ISO C Specification Language）形式化规约的问题。现有方法，如手动编写或基于规则的系统，耗时且容易出错。基于学习的方法虽然有潜力，但需要大量训练数据和计算资源。因此，如何高效、准确地为C程序生成ACSL规约是一个挑战。

核心思路：论文的核心思路是利用大型语言模型（LLM）的强大代码生成能力，直接生成ACSL规约。通过将C代码作为LLM的输入，期望LLM能够理解代码的语义并生成相应的形式化规约。这种方法避免了手动编写的繁琐和基于规则系统的局限性。

技术框架：整体流程包括：1) 选择C程序数据集；2) 使用五种ACSL生成系统（Python脚本、Frama-C RTE插件、DeepSeek-V3.2、GPT-5.2、OLMo 3.1 32B Instruct）生成ACSL规约；3) 使用Frama-C WP插件和多个SMT求解器验证生成的规约；4) 分析验证结果，比较不同生成系统的性能。

关键创新：该研究的关键创新在于直接评估了LLM在自动化ACSL规约生成中的能力，并与传统方法进行了对比。它提供了一个无需人工干预的自动化评估框架，可以系统地评估不同ACSL生成系统的性能。

关键设计：实验中，所有ACSL规约都在相同的条件下使用Frama-C WP插件进行验证，确保了评估的公平性。使用了多个SMT求解器来提高验证的可靠性。数据集包含506个C程序，具有一定的代表性。对注解质量、求解器敏感性和证明稳定性进行了详细的分析。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，LLM在ACSL规约生成方面具有一定的潜力，但与传统方法相比仍有差距。不同LLM的性能差异较大，DeepSeek-V3.2表现相对较好。实验还揭示了求解器敏感性和证明稳定性等问题，为未来的研究提供了方向。

🎯 应用场景

该研究成果可应用于软件形式化验证领域，提高软件可靠性和安全性。通过自动化生成ACSL规约，可以降低形式化验证的成本和难度，促进其在工业界的应用。未来，可以进一步研究如何提高LLM生成ACSL规约的准确性和效率，并将其应用于更复杂的软件系统。

📄 摘要（原文）

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 empirically evaluates the extent to which formal-analysis tools can automatically generate and verify ACSL specifications without human or learning-based assistance. We conduct a controlled study on a recently released dataset of 506 C programs, repurposing it from interactive, developer-driven workflows to an automated evaluation setting. Five ACSL generation systems are compared: 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. All generated specifications are verified under identical conditions using the Frama-C WP plugin powered by multiple SMT solvers, allowing a direct comparison of annotation quality, solver sensitivity, and proof stability. Our results provide new empirical evidence on the capabilities and limitations of automated ACSL generation, complementing prior survey-based work.