AutoReSpec: A Framework for Generating Specification using Large Language Models
作者: Ragib Shahariar Ayon, Shibbir Ahmed
分类: cs.SE, cs.AI
发布日期: 2026-04-07
💡 一句话要点
AutoReSpec：利用大语言模型自动生成可验证规约的协同框架
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 形式规约生成 大型语言模型 程序验证 自动化测试 协同框架
📋 核心要点
- 现有基于LLM的规约生成方法在处理复杂程序时，易出现语法错误、逻辑不准确等问题，导致验证失败。
- AutoReSpec通过动态选择LLM和提示配置，并引入协同模型利用验证器反馈进行规约修正，提升生成质量。
- 实验表明，AutoReSpec在成功率和完整性上优于现有方法，并显著降低了评估时间，验证了其有效性。
📝 摘要（中文）
形式规约生成是软件工程中提高程序正确性的一种新兴方法，无需手动标注。大型语言模型（LLMs）在该领域展现出潜力，但早期结果也暴露出一些局限性。由于语法错误、逻辑不准确或推理不完整，生成的规约常常无法通过验证，尤其是在包含循环或分支逻辑的程序中。SpecGen和FormalBench等技术试图通过提示和基准测试来解决这个问题，但它们通常依赖于静态提示，并且没有提供从失败中恢复或适应不同程序结构的机制。本文提出了AutoReSpec，一个结合了开源和闭源LLM的协同框架，用于生成可验证的规约。AutoReSpec基于输入程序的结构动态地选择LLM对和提示配置。如果主LLM未能产生有效输出，则调用协同模型，使用验证器的反馈来改进和纠正规约。这种两阶段设计实现了速度和鲁棒性。我们在一个包含72个真实和合成Java程序的新基准上评估了AutoReSpec。结果表明，AutoReSpec在72个程序中成功通过了67个，在成功概率和完整性方面均优于SpecGen和FormalBench。我们的实验评估实现了58.2%的成功概率和69.2%的完整性得分，同时与先前方法相比，平均评估时间缩短了26.89%。这些结果共同表明，AutoReSpec为基于LLM的形式规约生成提供了一种可扩展、高效且可靠的方法。
🔬 方法详解
问题定义：论文旨在解决利用大型语言模型自动生成程序的形式规约时，现有方法（如SpecGen和FormalBench）在处理包含循环或分支逻辑的复杂程序时，生成的规约容易出现语法错误、逻辑不准确，导致验证失败的问题。这些方法通常依赖静态提示，缺乏从失败中恢复和适应不同程序结构的能力。
核心思路：AutoReSpec的核心思路是构建一个协同框架，该框架能够根据输入程序的结构动态选择合适的LLM组合和提示配置，并在主LLM生成失败时，利用协同模型和验证器的反馈进行规约的修正和完善。这种动态选择和协同修正机制旨在提高规约生成的成功率和完整性。
技术框架：AutoReSpec框架包含两个主要阶段：首先，根据输入程序的结构，动态选择一个LLM对（一个主LLM和一个协同LLM）和相应的提示配置。主LLM尝试生成规约。如果主LLM生成失败，则进入第二阶段，调用协同LLM，并利用验证器提供的反馈信息，对规约进行修正和改进。整个流程旨在通过协同工作和反馈循环，提高规约生成的质量和效率。
关键创新：AutoReSpec的关键创新在于其动态选择LLM和提示配置的能力，以及利用协同模型和验证器反馈进行规约修正的机制。与现有方法相比，AutoReSpec能够更好地适应不同程序结构，并从失败中恢复，从而提高规约生成的鲁棒性和准确性。
关键设计：AutoReSpec的关键设计包括：1) 程序结构分析模块，用于确定输入程序的复杂度和特征，从而选择合适的LLM对和提示配置；2) LLM选择策略，根据程序结构选择最适合的主LLM和协同LLM；3) 提示工程，设计有效的提示，引导LLM生成高质量的规约；4) 验证器反馈机制，利用验证器提供的错误信息，指导协同LLM进行规约修正。
🖼️ 关键图片
📊 实验亮点
AutoReSpec在包含72个Java程序的基准测试中，成功通过了67个，成功概率达到58.2%，完整性达到69.2%，均优于SpecGen和FormalBench等现有方法。此外，AutoReSpec还显著降低了评估时间，平均缩短了26.89%。这些实验结果充分证明了AutoReSpec在形式规约生成方面的优越性能。
🎯 应用场景
AutoReSpec可应用于软件开发过程中的自动化测试和验证，帮助开发者更早地发现和修复程序中的错误，提高软件的可靠性和安全性。该技术还可用于教育领域，辅助学生理解和掌握形式规约的编写方法。未来，AutoReSpec有望扩展到更多编程语言和应用场景，成为提升软件质量的重要工具。
📄 摘要（原文）
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.