一句话：SpecGen 利用 LLM 对话式生成并变异筛选可验证的形式化程序规约，在 385 个程序上成功生成 279 个可验证规约。
形式化程序规约在需求分析、软件测试与验证中至关重要，但人工编写耗时耗力，且难以正确、全面地刻画复杂程序语义。现有自动生成方法多依赖预定义模板或文法，难以准确描述真实复杂程序的行为与功能。为此，作者提出 SpecGen，其核心洞见是利用大语言模型的代码理解能力突破既有方法的限制。SpecGen 分两阶段：第一阶段采用对话式方法引导 LLM 为给定程序生成合适的规约；第二阶段针对 LLM 生成失败的情形，对模型生成的规约施加四种变异算子，并通过一种新颖的启发式选择策略为不同变体高效分配权重，从中筛选出可验证的规约。实验在 SV-COMP Java 基准与包含 120 个程序的人工数据集上进行，SpecGen 在 385 个程序中为 279 个成功生成可验证规约，优于现有基于 LLM 的方法以及 Houdini、Daikon 等传统规约生成工具。进一步的规约质量分析表明，SpecGen 能较全面地表达输入程序的行为。
In the software development process, formal program specifications play a crucial role in various stages, including requirement analysis, software testing, and verification. However, manually crafting formal program specifications is rather difficult, making the job time-consuming and labor-intensive. Moreover, it is even more challenging to write specifications that correctly and comprehensively describe the semantics of complex programs. To reduce the burden on software developers, automated specification generation methods have emerged. However, existing methods usually rely on predefined templates or grammar, making them struggle to accurately describe the behavior and functionality of complex real-world programs. To tackle this challenge, we introduce SpecGen, a novel technique for formal program specification generation based on Large Language Models (LLMs). Our key insight is to overcome the limitations of existing methods by leveraging the code comprehension capability of LLMs. The process of SpecGen consists of two phases. The first phase employs a conversational approach that guides the LLM in generating appropriate specifications for a given program, aiming to utilize the ability of LLM to generate high-quality specifications. The second phase, designed for where the LLM fails to generate correct specifications, applies four mutation operators to the model-generated specifications and selects verifiable specifications from the mutated ones through a novel heuristic selection strategy by assigning different weights of variants in an efficient manner. We evaluate SpecGen on two datasets, including the SV-COMP Java category benchmark and a manually constructed dataset containing 120 programs. Experimental results demonstrate that SpecGen succeeds in generating verifiable specifications for 279 out of 385 programs, outperforming the existing LLM-based approaches and conventional specification generation tools like Houdini and Daikon. Further investigations on the quality of generated specifications indicate that SpecGen can comprehensively articulate the behaviors of the input program.
DOI 原文 ·
@inproceedings{paperbot8901,
title = {SpecGen: Automated Generation of Formal Program Specifications via Large Language Models},
author = {Lezhi Ma and Shangqing Liu and Yi Li and Xiaofei Xie and Lei Bu},
booktitle = {ICSE},
year = {2025},
doi = {10.1109/icse55347.2025.00129}
}