Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability
本文介绍了 Diversify2Verify，这是一个基于大语言模型（LLM）的流水线，它展示了生成多样化的、任务等效的程序实现如何通过识别更易于进行形式化证明的变体，从而显著提高自动化验证的成功率。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你正试图制造一个能够解决数学谜题的机器人。你有一个超级聪明的 AI 助手（大型语言模型），它非常擅长编写代码。通常情况下，我们会问 AI：“写一段能解决这个谜题的代码”，然后检查机器人是否通过了几次测试运行。如果通过了，我们就说：“做得好！”
但在**形式化验证（formal verification）**的世界里，通过几次测试是不够的。这就像建造一座桥梁，仅仅用玩具车在上面跑几圈是不够的。为了确保真正的安全，你需要一个数学证明，证明这座桥在任何时间、任何条件下都能承载任何车辆。这就是论文中所说的“演绎验证（deductive verification）”。
问题在于，让 AI 编写出不仅正确而且易于证明的代码是非常困难的。有时 AI 写的解决方案虽然运行完美，但结构过于混乱或奇特，以至于“证明检查器”（一个名为 Why3 的工具）会感到困惑并无法完成验证。
核心理念：不要只尝试一种方法
作者 Shirley Yu 和 Ruben Martins 提出了一个简单的问题：如果我们不只是索要一个解法，而是索要许多个相同解法的不同版本，会怎样？
这就像是在尝试打开一个顽固的罐头盖：
- 版本 A： 你尝试用右手拧开盖子。
- 版本 B： 你尝试用左手拧开盖子。
- 版本 C： 你尝试用勺子敲击盖子。
- 版本 D： 你尝试用热水冲洗盖子。
也许“右手拧”这种方式（AI 写的第一个代码）对于证明检查器来说太滑了，抓不住逻辑。但“左手拧”可能具有一种能完美契合检查器逻辑的形状。论文将此称为 Diversify2Verify。与其寄希望于一个完美的代码，不如生成四种不同“口味”的任务版本：
- 数组 + 命令式（Array + Imperative）： 就像一个人接一个人地走过一排人，逐一检查他们的名字。
- 数组 + 递归（Array + Recursive）： 像是一个“传声筒”游戏，你把任务传递给下一行的一系列助手。
- 列表 + 命令式（List + Imperative）： 像是翻阅一叠索引卡片。
- 列表 + 递归（List + Recursive）： 像是一个俄罗斯套娃，每个娃娃里面都包含着下一步。
实验：73 个谜题，292 次尝试
团队建立了一个特殊的游乐场，其中包含 73 个不同的编程谜题（主要涉及数字、列表和数组）。对于每个谜题，他们要求 AI 生成所有四种上述“口味”的代码。这总共产生了 292 个不同的代码尝试来进行测试。
他们不仅仅是让 AI 写代码，还设置了一个严格的三阶段流程：
- 第一阶段（契约/Contract）： 首先，他们让 AI 编写一份“契约”（一套正式的规则手册），描述代码必须做什么，而不必担心它如何实现。他们根据示例检查了这份规则手册，以确保其逻辑合理。一旦规则手册被接受，它就会被冻结。不再允许修改规则！
- 第二阶段（代码/Code）： 接下来，他们要求 AI 为每种口味编写实际代码，并确保这些代码能通过一些基础的测试运行。
- 第三阶段（证明/Proof）： 最后，他们尝试证明每个代码版本都满足那份被冻结的契约。如果证明失败，他们会给 AI 一个提示（“修复/repair”）来修正证明，但仅限于修正证明本身，而不是修改代码或规则。
结果：多样性胜出
以下是运行数据后的情况：
- “单次尝试”的失败： 如果你直接采用 AI 写的第一个代码并尝试证明它，只有 96 出 292（约 32.9%）成功了。这甚至不到三分之一！
- “修复”的力量： 当他们允许 AI 尝试两次修复证明时，成功数量跃升至 154 出 292（约 52.7%）。
- “多样性”的力量（真正的赢家）： 当他们从整体上看这 73 个谜题时，他们发现对于其中的 49 个（成功率为 67.1%），至少有一个版本可以被证明是正确的。
这是主要的发现：任务等效的实现方式在可验证性上存在显著差异。 换句话说，两个执行相同任务的代码，在证明难度上可能天差地别。
他们排除了什么（它不是什么）
论文非常谨慎地说明了它没有声称的内容：
- 它不是关于更好的代码： 他们并没有发现“数组比列表更好”或“递归比循环更好”。事实上，结果是混合的。递归代码通常比命令式（基于循环）代码更容易证明，但数组和列表在整体表现上相似。关键不在于选择哪种“最佳”风格，而在于拥有选项。
- 它不是关于改变规则： 他们严格禁止 AI 在“修复”阶段修改“契约”（目标）。如果 AI 试图通过改变目标来使证明变得更容易，那将被视为失败。他们想要证明的是原始目标，而不是一个更弱的目标。
- 它不是解决所有问题的万灵药： 该研究仅针对涉及整数、数组和列表的谜题。他们并不声称这适用于浮点数、复杂的 3D 图形或与互联网交互的程序。
他们有多确定？
作者对他们的测量结果很有信心，但对宏观图景保持谨慎。
- 已测量： 他们拥有确凿的数据。他们运行了工具，统计了成功次数，并观察到多样性将单个人工制品的成功率从 32.9% 提高到了 52.7%，并将任务整体的成功率提升到了 67.1%。
- 已推测： 他们认为命令式代码（循环）更难证明的原因在于，它需要“循环不变式”（关于循环内部发生情况的规则），而这些规则很难由 AI 自动发明。他们怀疑，如果你给 AI 提供更好的工具来猜测这些规则，这种差距可能会缩小。
- 尚未证实（尚待研究）： 他们承认并没有证明“数组契约”和“列表契约”在数学上是完全等同的。他们只是根据任务描述假设它们意思相同。他们还指出，他们的“评判者”（一个检查规则是否符合谜题的 AI）并不是完美的专家，因此可能会有极少数细微的错误溜过去。
总结
这篇论文表明，当我们要求 AI 编写“经过验证”的软件时，我们不应该只索要一个答案并祈祷好运。相反，我们应该索要一份选项菜单。通过生成解决同一问题的不同方式，我们增加了找到那个能被证明检查器理解的版本之机会。
这就像是在寻找一把能打开锁的钥匙。如果你只有一把钥匙，你可能会陷入僵局。但如果你有一整串钥匙，即使它们打开的是同一扇门，其中一把几乎肯定能完美契合锁芯。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。