Path2Spec：基于路径感知的大语言模型规格生成

中文摘要 AI 辅助

形式化规格对于程序验证、理解和维护至关重要。然而，手动编写规格成本高昂且难以扩展。近期研究表明，大语言模型（LLMs）在自动化规格生成方面具有潜力，但现有方法存在质量问题。我们分析了一种最先进的方法，发现至少34.6%的成功验证的规格实际上未能有意义地捕获程序的独特行为，这是一个仅衡量验证成功与否的指标无法捕获的质量问题。我们进一步发现，导致此类隐藏质量问题的一个主要因素源于现有方法的设计：这些方法将程序视为单一单元，导致约束过于笼统和粗粒度。为此，我们提出了Path2Spec，一个通过系统化的基于路径推理来解决这些局限性的分而治之框架。Path2Spec利用LLMs从输入程序中提取所有执行路径，为每条路径生成路径特定的规格，并将它们合并为全面的整体规格。对于基于路径生成困难的复杂程序，Path2Spec采用“分解-重试”策略，基于逻辑分支将程序递归分解为更小的子程序，为每个子程序生成规格，然后合并。我们在两个公共基准上评估了Path2Spec：SG-Bench（120个程序）和SV-COMP（265个程序）。结果表明，Path2Spec优于最先进的基线SpecGen：在SG-Bench上为87.5%对66.7%，在SV-COMP上为83.0%对44.2%。人工评估进一步验证了Path2Spec生成的规格质量更高，与代码的语义对齐更精确。

英文摘要

Formal specifications are critical for program verification, comprehension, and maintenance. However, manually writing them is costly and difficult to scale. Recent studies have shown that Large Language Models (LLMs) are promising for automated specification generation, but existing methods suffer from quality issues. We analyze a state-of-the-art approach and find that at least 34.6% of successfully verified specifications actually fail to meaningfully capture the program's distinct behavior, which is a quality issue not captured by metrics that only measure verification success. We further found that a major factor contributing to such hidden quality issues stems from the design of existing methods: these methods treat a program as a single unit, resulting in overly general, coarse-grained constraints. To this end, we introduce Path2Spec, a divide-and-conquer framework that addresses these limitations through systematic path-based reasoning. Path2Spec leverages LLMs to extract all execution paths from an input program, generates path-specific specifications for each, and merges them into a comprehensive overall specification. For complex programs where path-based generation struggles, Path2Spec employs a decompose-then-retry strategy that recursively breaks a program into smaller subprograms based on logical branches, generates specifications for each, and merges them back. We evaluate Path2Spec on two public benchmarks: SG-Bench (120 programs) and SV-COMP (265 programs). Results show that Path2Spec can outperform the state-of-the-art baseline SpecGen: 87.5% versus 66.7% on SG-Bench, and 83.0% versus 44.2% on SV-COMP. Human evaluation further validates that Path2Spec generates higher-quality specifications with precise semantic alignment to the code.

发表机构

• Singapore Management University（新加坡管理大学）

机构由 AI 辅助整理，请以论文原文为准。