AutoReSpec：使用 大语言模型 生成规范的框架

形式规范生成最近引起了软件工程的关注，作为一种无需手动注释即可提高程序正确性的方法。 大语言模型 (LLM) 在这一领域表现出了希望，但早期结果揭示了一些局限性。生成的规范经常由于语法错误、逻辑不准确或推理不完整而无法验证，特别是在具有循环或分支逻辑的程序中。像 SpecGen 和 FormalBench 这样的技术试图通过提示和基准测试来解决这个问题，但它们通常依赖于静态提示，并且不提供从故障中恢复或适应不同程序结构的机制。在本文中，我们提出了 AutoReSpec，这是一个结合了开源和闭源 LLM 的协作框架，用于生成可验证的规范。 AutoReSpec 根据输入程序的结构动态选择 LLM 对和提示配置。如果主 LLM 无法产生有效的输出，则会调用协作模型，使用验证器反馈来完善和纠正规范。这种两级设计可实现速度和稳健性。我们在 72 个真实世界和合成 Java 程序的新基准上评估 AutoReSpec。我们的结果表明，它在 72 次测试中通过了 67 次，在成功概率和完整性方面均优于 SpecGen 和 FormalBench。我们的实验评估取得了 58.2% 的成功概率和 69.2% 的完整性分数，同时与之前的方法相比，评估时间平均缩短了 26.89%。总之，这些结果表明 AutoReSpec 为基于 LLM 的正式规范生成提供了一种可扩展、高效且可靠的方法。