💻 computer science

KBSpec: LLM-driven Formal Specification Generation with Evolving Domain Knowledge Base

KBSpec 是一个由大语言模型驱动的框架，它通过利用包含外部文档和内部验证器反馈的自演进知识库来生成形式化规范，在无需参数调优或标注训练数据的情况下，实现了验证通过率的显著提升。

原作者： Wenhan Wang, Zeyu Sun

发布于 2026-06-23

📖 1 分钟阅读☕ 轻松阅读

原作者： Wenhan Wang, Zeyu Sun

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

核心理念：教机器人编写代码的法律合同

想象一下，你有一个非常聪明、富有创造力的机器人（大语言模型，简称 LLM），它非常擅长写故事和写代码。然而，你希望这个机器人能编写形式化规范（Formal Specifications）——这就像是严格的数学法律合同，用以证明一段软件永远不会崩溃或表现异常。

问题在于，这个机器人以前没怎么读过这些“法律合同”。在现实世界中，大多数程序员并不编写这些合同，他们只写代码。因此，当你要求机器人编写一个规范时，它经常会出错：它会使用错误的语法，忘记重要的安全规则，或者写出一些听起来不错但在数学上无法证明的东西。

KBSpec 是一个旨在解决这一问题的全新系统。它为机器人提供了一个“智能笔记本”，帮助它学习如何正确地编写这些合同，而无需重新训练机器人的大脑。

双源知识系统

论文指出，要修复这个机器人，你需要两种类型的信息，就像学生为一场困难的考试做准备一样：

教科书（外部知识）： 这是由创建该语言的专家编写的官方手册。它告诉机器人基本的规则和语法。
- 类比： 想象给机器人一本字典和一本语法书。它认识这些词汇，但不知道如何在复杂的场景中使用它们。
教练笔记（内部知识）： 这是 KBSpec 最独特的部分。它来自于观察机器人尝试、失败、被纠正并再次尝试的过程。
- 类比： 想象机器人尝试编写一份合同，然后一位严格的裁判（形式化验证器）吹响了哨子说：“错误！你不能那样做！”随后机器人再次尝试，修复了错误，并成功了。KBSpec 会将这个“成功案例”记录在笔记本中。下次，机器人可以查看笔记本并说：“噢，我记起来了！当我尝试做 X 时，裁判很生气，但如果我改做 Y，它就成功了。”

KBSpec 的工作原理（三步流水线）

论文描述了构建该系统的三个步骤：

第 1 步：初始设置（填充笔记本）
研究人员首先将官方手册和示例放入机器人的“笔记本”（知识库）中。这为机器人提供了一个基础的起点。

第 2 步：训练循环（在实践中学习）
这是见证奇迹的时刻。系统会多次运行一个循环：

机器人尝试为一段代码编写规范。
验证器（裁判）对其进行检查。
如果通过： 系统会将成功的“配方”保存到笔记本中。
如果失败： 系统会查看错误信息，向笔记本寻求帮助，并尝试修复错误。如果修复成功，这个“修复配方”也会被保存下来。
过滤器： 笔记本不仅仅是纸张的堆砌。系统会不断检查：“这条建议真的帮我们通过测试了吗？”如果官方手册中的某条建议导致了失败，它的权重就会降低。如果从修复过程中学到的新技巧奏效了，它就会获得提升。

第 3 步：期末考试（推理）
当机器人面对一段全新的、未见过的代码时，它不会仅仅靠猜测。它会查找其不断进化的笔记本中最相关的“配方”，以帮助它编写规范。它利用过去失败的教训来避免重蹈覆辙。

为什么这很特别

论文强调了几个关键点，使 KBSpec 区别于其他方法：

无需“脑部手术”： 通常，为了让 AI 变得更好，你必须进行“微调”，这就像是对模型进行昂贵的脑部手术。KBSpec 完全没有触碰机器人的大脑，它只是更新了笔记本。这使得它成本低廉，且易于与任何机器人配合使用。
“自我进化”的笔记本： 笔记本不是静态的。每当机器人进行练习时，它都会变得更加聪明。它能学习哪些来自官方手册的规则是真正有用的，哪些规则对于裁判来说过于复杂。
更好的结果： 当他们在 Java 代码上进行测试（使用名为 FormalBench 的基准测试）时，KBSpec 帮助机器人通过验证测试的频率比以往最好的方法高出了 10% 到 25%。它生成的规范不仅是“正确的”，而且更加“完备”（覆盖了所有必要的细节）。

潜在的问题（论文发现）

研究人员注意到关于合同“完备性”的一个有趣现象。有时，为了让机器人通过测试，系统不得不使合同的约束稍微放宽（例如，“这适用于大多数数字”而不是“这适用于每一个数字”）。

类比： 这就像律师意识到：“如果我向客户承诺月亮，我会被告。但如果我承诺一个非常大且安全的花园，我就能证明这是真的。”
论文发现，虽然平均严格程度略有下降，但系统生成的更具用处且可验证的合同数量增加了。它用极小的完美度损失换取了大量的成功。

总结

KBSpec 就像是给一个学生一本教科书，同时还配备了一位私人导师，这位导师会记录下每一次考试中的错误以及是如何被修复的。通过根据严格评分者的反馈不断更新这份日记，学生学会了如何更频繁地通过考试，而无需改变他们的思考方式——只需给他们更好的笔记来学习即可。

技术摘要：KBSpec

问题陈述

自动化形式化规范生成是程序理解和形式化验证的关键步骤。尽管大语言模型（LLMs）在代码生成方面已展现出潜力，但其在形式化规范（例如 Java Modeling Language, JML）方面的应用面临着一个重大障碍：训练数据中形式化规范语料库的匮乏。这种“低资源”状态导致了频繁的语法错误和语义失败（例如缺失边界检查、不正确的属性约束）。

现有的增强 LLM 外部知识（如官方文档）的尝试并不充分，因为形式化规范资源通常是不完整的，缺乏对多样化验证模式的覆盖，或者包含尚未被验证器完全支持的实验性特性。此外，仅依赖静态外部知识无法捕捉到成功验证所需的细微且特定于验证器的约束。

方法论：KBSpec

作者提出了 KBSpec（基于知识库增强的规范生成），这是一个通过双源、自进化知识库来增强 LLM 的框架。该系统无需修改 LLM 参数，也不需要标注的地面真值（ground-truth）数据，而是依赖于来自形式化验证器的反馈进行运行。

KBSpec 流水线由三个主要阶段组成：

1. 知识库初始化

系统使用源自外部知识（如 OpenJML 教程、示例和练习等官方文档）和人工编写的修复指南来初始化形式化规范知识库 ( $M$ )。每个知识项被结构化为一个三元组：原始内容 ( $c_i$ )、摘要 ( $s_i$ ) 和关键词 ( $k_i$ )，这些内容由 LLM 生成以方便检索。

2. 知识库进化（训练阶段）

这是核心创新点。知识库通过在“训练”语料库（Java 程序）上运行生成与修复流水线来进行动态更新。

生成： 对于给定的程序，LL模型生成一个基准规范。随后，它检索相关的知识项，并基于检索到的不同知识组合生成新的规范。
验证与评分： 生成的规范使用形式化验证器（OpenJML）进行验证。根据检索到的知识项是否帮助 LLM 在此前失败的情况下通过了验证，或者在此前通过的情况下导致了失败，为其分配一个帮助度得分（helpfulness score）。
迭代修复： 对于失败的规范，系统执行最多三轮修复。LLM 使用原始规范、验证器错误信息以及检索到的知识来生成修复后的版本。检索项的帮助度根据错误数量的减少或验证的成功与否进行更新。
更新与过滤： 在每个周期（epoch）结束后，知识库会进行更新。帮助度得分较低的项会被过滤掉，而新的成功轨迹（生成或修复）会被添加进来。冗余通过相似性检查进行管理。

3. 知识增强推理

在评估阶段，KBSpec 使用进化的知识库来辅助规范生成。与训练阶段使用知识组的随机采样不同，推理阶段采用基于 LLM 的选择器。LLM 会从检索到的集合中自主选择最相关的知识项（最多 3 个），以引导规范的生成及随后的修复。

核心贡献

KBSpec 框架： 一种新型的、无参数的形式化规范生成方法，它集成了一个由验证器反馈驱动的自进化知识库。
双源知识： 识别并验证了结合外部文档（用于初始语言理解）与内部知识（从生成/修复轨迹中提取的验证器反馈）对于克服 LLM 在形式化规范领域局限性的重要性。
实证验证： 在 FormalBench 基准测试（JML 规范生成）上进行了全面的评估，结果表明 KBSpec 显著优于最先进的基准方法，包括 SpecGen 以及各种提示策略（Few-shot, Least-to-Most, Self-repair）。

结果

实验使用了三种 LLM 后端：GPT-5.2、GPT-5-mini 和 DeepSeek-v3.2。

通过率提升： KBSpec 比最先进的基于 LLM 的方法（如 SpecGen）将验证通过率提高了 10–25%。在 GPT-5.2 上，通过率从 43.35% (SpecGen) 提升至 58.94%。
失败率降低： 该框架大幅降低了失败率（例如，将 GPT-5.2 的失败率降至 20.6%）。
完备性： 虽然平均完备性得分表现出一定的波动，但 KBSpec 产生了数量最多的高完备性规范（完备性 $\ge$ 0.5）。对相互验证程序的分析显示，与 SpecGen 相比，KBSpec 保持或提高了完备性，这表明通过率的提升并非通过生成过于简单的弱契约来实现。
消融实验： 研究证实，知识库进化机制（内部知识）是最关键的组件，其对性能的贡献超过了初始的外部文档。迭代修复也被确定为成功的关键驱动因素。

意义与主张

论文声称 KBSpec 通过创建一个自改进循环解决了形式化规范语言的“低资源”问题，在该循环中，系统通过验证器反馈从自身的成功与失败中学习。

模型无关性： 该方法是轻量级的，可以应用于任何 LLM 而无需微调。
泛化性： 虽然是在 JML 上进行的评估，但作者声称该设计是语言无关的，可以适配于任何带有自动化验证器的形式化语言。
工程实用性： 对学习到的知识的分析表明，该系统有效地学习了实用的修复策略（例如，处理算术溢出、移除不支持的结构），而不仅仅是通过削弱规范来通过验证。

作者总结道，将文档衍生的知识与基于验证器落地的记忆进化相结合，能显著增强 LLM 生成语法正确且语义可验证的形式化规范的能力。