KBSpec：使用不断发展的领域知识库生成 LLM 驱动的形式化规范

自动形式化规范生成是实现程序理解和形式化验证的关键一步。最近，由于大语言模型（LLM）在代码生成方面的成功，研究人员已经开始尝试采用LLM来生成形式化规范。然而，缺乏正式的规范语言语料库常常导致 LLM 无法生成语法正确且语义可验证的规范。为了弥补这一差距，我们提出了 KBSpec，它通过正式规范语言的双源知识来增强 LLM：来自官方文档的外部知识，以及从 LLM 生成的规范的验证者反馈中提取的内部知识。 KBSpec 维护着一个自我进化的知识库，该知识库从成功的生成和修复轨迹中不断更新，无需任何 LLM 参数调整或标记的训练数据。我们使用三个 LLM 后端对 Java 建模语言 (JML) 规范生成的 KBSpec 进行了评估，结果表明，与最先进的基于 LLM 的方法相比，KBSpec 将验证通过率提高了 14-32%，同时生成了最大数量的高完整性规范。