Neural Theorem Proving for Verification Conditions: A Real-World Benchmark
本文介绍了 NTP4VC，这是首个针对源自 Linux 和 Contiki-OS 等工业项目的验证条件的神经定理证明多语言真实世界基准测试，揭示了大语言模型在自动化程序验证方面的潜力与当前的局限性。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
以下是关于论文 "Neural Theorem Proving for Verification Conditions: A Real-World Benchmark" 的解释，采用了通俗易懂的语言和富有创意的类比。
大局观： “证明瓶颈”
想象一下你正在建造一台庞大且复杂的机器（比如汽车发动机或计算机操作系统）。你希望 100% 确定在转动钥匙时，它不会爆炸或损坏。在软件世界中，这被称为 程序验证 (Program Verification)。
为了实现这一点，数学家和计算机科学家将代码转化为一个巨大的、复杂的逻辑谜题。他们会问：“如果我给这台机器这些输入，它是否始终表现得如其承诺的那样？”
这篇论文关注的是这个过程中一个特定的、令人痛苦的步骤，叫做生成 验证条件 (Verification Conditions, 简称 VCs)。你可以把 VC 理解为一个特定的、高风险的数学问题，计算机必须解决这个问题才能证明代码是安全的。
问题所在：
目前，计算机在独立解决这些特定数学问题方面表现得很糟糕。它们就像是一个天才棋手，能用 10 秒钟解开一个谜题，但如果你给它一个稍微不同的、现实世界的谜题，它就会卡住。
因为计算机会卡住，人类专家不得不介入并手动编写解决方案。这既缓慢又昂贵，阻碍了公司在所有环节都使用这些安全检查。
新思路：教 AI 解开谜题
作者们问道：“我们能否教人工智能（特别是大语言模型或 LLM）自动解决这些逻辑谜题？”
这个领域被称为 神经定理证明 (Neural Theorem Proving, NTP)。这就像是在训练一个机器人成为数学家。虽然这些机器人已经在解决抽象数学竞赛题目（如 Putnam 竞赛）方面取得了很大进步，但没人知道它们是否能处理来自实际软件代码的、杂乱的现实世界逻辑谜题。
解决方案：为 AI 建造一个“健身房”（基准测试）
为了测试 AI 是否能胜任，研究人员建造了一个新的“健身房”（基准测试数据集），名为 NTP4VC。
1. 这些谜题从何而来？
他们没有凭空捏造谜题，而是转向了现实世界的工业项目。他们查看了著名系统的源代码，如 Linux 内核（你电脑的大脑）、Contiki-OS（用于微型互联网设备的系统）以及各种 C 标准库。
2. 他们是如何获取这些谜题的？
他们使用了一个“翻译器”流水线。
- 第一步： 他们提取真实的程序代码，并通过工业工具（如 Frama-C 和 Why3）自动生成逻辑谜题 (VCs)。
- 第二步： 由于 AI 模型使用不同的“语言”（Isabelle, Lean, Rocq），他们构建了一个包含 800 多个专家编写的规则 的庞大库，用于将这些谜题从工业工具翻译成 AI 能理解的语言。
- 关键细节： 他们并没有直接复制谜题。原始谜题太容易了，因为人类工程师已经添加了“提示”（annotations）来帮助计算机求解。研究人员 移除了这些提示，从而增加了谜题的难度，从而对 AI 的能力进行了真正的测试。
3. 数据集：
他们创建了一组 600 个具有挑战性的谜题，分为两组：
- “程序的珍珠” (Pearls of Programs)： 经典的、困难的算法谜题（如排序数据或管理内存树）。
- “真实 C 验证” (Real C Verification)： 从实际、杂乱的工业代码中提取的谜题（如内存分配器或链表）。
实验：谁赢得了比赛？
研究人员在新的“健身房”上，让最优秀的 AI 模型与最优秀的传统计算机求解器（称为 “Hammer” 证明器）展开了对决。
结果：
- AI 模型 (LLMs)： 它们表现得非常吃力。即使是最聪明的模型，在第一次尝试时也只能解决大约 2% 到 5% 的谜题。
- 传统求解器 (Hammer)： 这些老派的、专门化的工具表现得更好，解决了约 18% 到 27% 的谜题。
- 差距： AI 模型明显逊色于传统的工具。
为什么 AI 会失败？（尸检报告）
研究人员分析了 AI 失败的原因，并利用了一些精彩的比喻总结出了三个主要原因：
语法错误（“拼写错误”问题）：
逻辑谜题极其冗长且嵌套深，就像一个带有 50 个括号的句子。AI 总是会忘记闭合括号或者多加一个括号。这就像一个学生虽然懂得数学，但总是在书写时出现拼写错误，导致老师无法读懂答案。- 统计数据： 超过 24% 的 AI 尝试仅仅因为这些语法错误而失败。
语义混乱（“冒充者”问题）：
AI 会写出看起来像证明、但实际上毫无意义的代码。它会重复同一个步骤（“我有一个事实，所以我有一个事实……”）或者使用错误的逻辑类型（比如用锤子去拧螺丝）。它是在没有理解游戏规则的情况下，在幻觉出一个解决方案。- 统计数据： 其中一个顶尖模型的超过 64% 的尝试都退化成了这种重复性的废话。
幻觉（“假事实”问题）：
AI 会发明不存在的工具或事实。它可能会说：“我将使用why3策略来解决这个问题”，但该策略在它所使用的语言中并不存在。这就像一个学生说：“我使用了微积分的魔杖”，而魔杖根本不存在。- 统计数据： 大约 9% 的失败是由于发明了不存在的工具。
结论
论文得出结论：尽管 AI 在数学竞赛领域取得了巨大进步，但 它尚未准备好取代人类专家来进行现实世界软件的验证。
他们建造的这个“健身房” (NTP4VC) 表明，目前的 AI 能力与实现软件验证全自动化之间仍存在巨大的鸿沟。AI 需要在以下方面做得更好：
- 遵循严格的语法规则（不再有拼写错误）。
- 理解工业代码的深层逻辑（而不只是抽象数学）。
- 保持与现实的联系（不再编造事实）。
在此之前，“人工参与”（即由专家编写提示）对于保障我们的软件安全仍然至关重要。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。