An Empirical Study of LLM-Generated Specifications for VeriFast
本文通过对十个大语言模型在八种提示策略下生成 303 个 C 函数的 VeriFast 规范进行实证评估，揭示了尽管大语言模型能够保留功能行为，但由于在特定领域分离逻辑知识方面的错误，其验证成功率仅为 31.4%，表现出有限的有效性。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你拥有一个非常严格、超级聪明的机器人检查员——VeriFast。它的职责是检查计算机代码，确保代码永远不会崩溃、永远不会丢失数据，并且其行为完全符合承诺。但问题在于，VeriFast 不说人类语言。它说的是一种非常复杂的数学方言，叫做分离逻辑（Separation Logic）。为了让 VeriFast 执行任务，人类必须编写一份庞大的“说明书”（规范），详细解释代码如何处理内存，就像绘制一份关于城市交通规则的详细地图一样。
编写这些说明书极其困难且耗时。这就像是试图为司机在公路旅行中每一次转弯都写一份法律合同。
核心问题
研究人员在论文中提出了这样一个问题：人工智能（特别是大语言模型，即 LLMs）能否编写这些复杂的说明书来供 VeriFast 使用？
他们将 LLM 视为一名懂得编写代码但需要学习 VeriFast 严苛方言的新学徒。他们测试了 10 种不同的 AI 模型和 303 个不同的计算机函数（代码的小片段），以观察 AI 是否能编写出这份说明书，以及 VeriFast 是否会接受它。
实验：“三步走”测试
研究人员设置了一场大规模的实测演练：
- 输入内容： 他们为每个任务提供了三种类型的“简报”：
- 自然语言： 仅仅是纯英文描述（例如：“这个函数将一个节点添加到列表末尾”）。
- 形式化行为： 代码与一些数学符号的混合体。
- 形式化增强版： 代码加上一份非常详细、几乎完整的数学说明书。
- 提示词： 他们尝试了 8 种不同的提问方式（例如：是像给出一个分步食谱，还是仅仅说“去做”）。
- 模型： 他们测试了 10 个不同的 AI 大脑，从 GPT-4o 到 Gemini 2.5 Pro。
结果：好消息、坏消息与“差一点”
好消息（学徒很诚实）：
AI 在理解代码的意图方面表现得惊人地好。在超过 91% 的案例中，AI 没有意外改变代码原本应有的功能。它没有试图通过让代码变得更容易证明来欺骗检查员。它始终忠于原始的任务描述。坏消息（学徒对规则一窍不通）：
尽管 AI 理解这项工作，但它无法编写出一份能让 VeriFast 接受的说明书。只有大约 31% 的 AI 生成的说明书通过了检查。这大约是每 3 次尝试中仅有 1 次成功。“为什么”（不是逻辑问题，而是语法问题）：
当 AI 失败时，通常并不是因为它“笨”或者不会做数学题，而是因为它不知道 VeriFast 特有的语法和规则。- 类比： 想象一位才华横溢的大厨，他知道如何烹饪出一块完美的牛排。但 VeriFast 是一位卫生检查员，它只接受用一种特定的、晦涩的法语方言编写的食谱。大厨一直在用英语或西班牙语写食谱。食物很棒，但检查员拒绝了它，因为格式不对。
- 研究发现，94% 的错误都与这些特定规则有关（比如忘记“打开”或“关闭”某个内存块，或者缺少特定的关键词），而不是程序本身的逻辑问题。
谁赢了？
- 最强的 AI： Gemini 2.5 Pro 是明显的赢家。它犯的错误更少，通过的检查也更多。
- 最好的输入： 当研究人员给 AI 提供“形式化增强版”简报（一个非常详细的起点）时，成功率上升了。当只给它一段纯英文描述时，AI 的表现最为挣扎。
总结
论文的结论是：虽然 AI 非常擅长理解代码应该做什么，但目前它并不擅长编写像 VeriFast 这样先进的验证工具所要求的特定、僵化的指令。
AI 的失败并非因为它无法进行推理，而是因为它不懂这个工具的“方言”。要解决这个问题，研究人员建议我们需要：
- 更好地教导 AI 关于 VeriFast 的特定规则；
- 给 AI 提供更好的反馈（例如，像老师纠正语法错误一样进行纠错，而不仅仅是说“错了”）；
- 使用 AI 与传统工具相结合的方法来填补空白。
简而言之：AI 学徒很有天赋也很诚实，但在它能独立工作之前，还需要在针对机器人检查员的特定“语言”方面接受更多的训练。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。