FormalSpecCpp: A Dataset of C++ Formal Specifications created using LLMs

📄 arXiv: 2502.15217v1 📥 PDF

作者: Madhurima Chakraborty, Peter Pirkelbauer, Qing Yi

分类: cs.SE, cs.AI, cs.LG, cs.PL

发布日期: 2025-02-21

备注: Accepted at the 2025 IEEE/ACM 22nd International Conference on Mining Software Repositories (MSR)

🔗 代码/项目: GITHUB

💡 一句话要点

FormalSpecCpp：利用LLM创建的C++形式化规约数据集，促进程序验证研究

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

关键词: C++程序 形式化规约 数据集 程序验证 规约推断 大型语言模型 自动化测试

📋 核心要点

  1. 现有C++程序形式化规约验证缺乏标准基准，阻碍了相关工具的评估和改进。
  2. FormalSpecCpp数据集提供包含前置条件和后置条件的C++程序，为规约推断提供结构化基准。
  3. 该数据集可用于评估规约推断工具、微调LLM以自动生成规约，并分析规约在程序验证中的作用。

📝 摘要（中文）

FormalSpecCpp是一个旨在填补C++程序中形式化规约验证标准化基准空白的数据集。据我们所知，这是第一个包含明确定义的前置条件和后置条件的C++程序综合集合。它为评估规约推断工具和测试生成规约的准确性提供了一个结构化的基准。研究人员和开发人员可以使用此数据集来评估规约推断工具，微调用于自动规约生成的大型语言模型（LLM），并分析形式化规约在改进程序验证和自动化测试中的作用。通过公开提供此数据集，我们旨在推进程序验证、规约推断和AI辅助软件开发领域的研究。

🔬 方法详解

问题定义：现有C++程序的形式化规约验证缺乏统一的标准基准，这使得评估和比较不同的规约推断工具变得困难。同时，也缺乏高质量的数据集来训练和评估基于机器学习的规约生成模型。因此，需要一个包含明确定义的前置条件和后置条件的C++程序数据集，以促进程序验证和自动化测试领域的研究。

核心思路：该论文的核心思路是利用大型语言模型（LLM）的强大代码生成和理解能力，自动生成具有形式化规约的C++程序。通过精心设计提示词和约束条件，引导LLM生成满足特定要求的代码，并确保生成的代码具有明确的前置条件和后置条件。

技术框架：该论文主要关注数据集的构建，并没有提出特定的技术框架。其核心在于利用LLM生成C++代码，并确保代码的正确性和规约的准确性。具体流程可能包括：1）定义C++程序的功能和接口；2）设计包含前置条件和后置条件的提示词；3）使用LLM生成C++代码；4）验证代码的正确性和规约的准确性；5）将生成的代码和规约添加到FormalSpecCpp数据集中。

关键创新：该论文的关键创新在于构建了一个高质量的C++形式化规约数据集，填补了该领域的空白。该数据集的构建方法利用了LLM的强大能力，可以高效地生成大量的具有形式化规约的C++程序。此外，该数据集还提供了一个结构化的基准，可以用于评估和比较不同的规约推断工具。

关键设计：论文中没有详细描述关键设计细节，例如LLM的具体选择、提示词的设计、验证方法等。这些细节可能在后续的研究中进一步完善。数据集的规模和多样性是关键的设计考虑因素，需要覆盖不同的C++编程范式和应用场景。

🖼️ 关键图片

fig_0
fig_1

📊 实验亮点

FormalSpecCpp是首个包含明确定义的前置条件和后置条件的C++程序综合集合，为C++程序的形式化规约验证提供了一个结构化的基准。该数据集的发布将极大地促进程序验证、规约推断和AI辅助软件开发领域的研究。

🎯 应用场景

FormalSpecCpp数据集可广泛应用于程序验证、规约推断和AI辅助软件开发等领域。研究人员可以利用该数据集评估和改进现有的规约推断工具，开发新的基于机器学习的规约生成模型。开发人员可以利用该数据集提高软件的可靠性和安全性，降低软件开发的成本。

📄 摘要（原文）

FormalSpecCpp is a dataset designed to fill the gap in standardized benchmarks for verifying formal specifications in C++ programs. To the best of our knowledge, this is the first comprehensive collection of C++ programs with well-defined preconditions and postconditions. It provides a structured benchmark for evaluating specification inference tools and testing theaccuracy of generated specifications. Researchers and developers can use this dataset to benchmark specification inference tools,fine-tune Large Language Models (LLMs) for automated specification generation, and analyze the role of formal specifications in improving program verification and automated testing. By making this dataset publicly available, we aim to advance research in program verification, specification inference, and AI-assisted software development. The dataset and the code are available at https://github.com/MadhuNimmo/FormalSpecCpp.