用大模型自动生成可验证的程序规范，错误率更低、速度更快。
AutoReSpec: A Framework for Generating Specification using Large Language Models
- 根据程序结构动态选模型和提示，失败时自动修正
- 72个测试用例中通过67个，成功率58.2%，完整度69.2%
- 适合需要高可靠性的软件验证场景
形式化规范生成近年来受到软件工程领域关注，旨在不依赖人工标注的情况下提升程序正确性。大语言模型（LLMs）在此方面展现出潜力，但早期结果暴露出诸多局限：生成的规范常因语法错误、逻辑偏差或推理不全而无法通过验证，尤其在含循环或分支逻辑的程序中更为明显。现有方法如SpecGen和FormalBench虽通过提示工程与基准测试缓解问题，但多依赖静态提示，缺乏失败恢复与结构适应机制。本文提出AutoReSpec，一种结合开源与闭源模型的协作框架，能够根据输入程序结构动态选择模型对与提示配置。若主模型生成失败，将触发协同模型，利用验证器反馈进行迭代修正。该两阶段设计兼顾效率与鲁棒性。我们在包含72个真实与合成Java程序的新基准上评估AutoReSpec，结果显示其在72个用例中成功通过67个，显著优于SpecGen与FormalBench，在成功率（58.2%）与完整性（69.2%）上均领先，且平均评估时间减少26.89%。结果表明，AutoReSpec为基于大模型的形式化规范生成提供了可扩展、高效且可靠的解决方案。
原文摘要 · Abstract (English)
Formal specification generation has recently drawn attention in software engineering as a way to improve program correctness without requiring manual annotations. Large Language Models (LLMs) have shown promise in this area, but early results reveal several limitations. Generated specifications often fail verification due to syntax errors, logical inaccuracies, or incomplete reasoning, especially in programs with loops or branching logic. Techniques like SpecGen and FormalBench attempt to address this through prompting and benchmarking, but they typically rely on static prompts and do not offer mechanisms for recovering from failure or adapting to different program structures. In this paper, we present AutoReSpec, a collaborative framework that combines open and closed-source LLMs for verifiable specification generation. AutoReSpec dynamically chooses an LLM pair and prompt configuration based on the structure of the input program. If the primary LLM fails to produce a valid output, a collaborative model is invoked, using validator feedback to refine and correct the specification. This two-stage design enables both speed and robustness. We evaluate AutoReSpec on a new benchmark of 72 real-world and synthetic Java programs. Our results show that it achieves 67 passes out of 72, outperforming SpecGen and FormalBench in both Success Probability and Completeness. Our experimental evaluation achieves a 58.2% success probability and a 69.2% completeness score, while cutting evaluation time by 26.89% on average compared to prior methods. Together, these results demonstrate that AutoReSpec offers a scalable, efficient, and reliable approach to LLM-based formal specification generation.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。