Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification
本文介绍了 Cobblestone，一种利用大语言模型通过分治策略将复杂证明任务拆解为子问题并迭代求解的自动化形式验证方法，该方法在确保证明可靠性的同时显著提升了定理证明率并降低了成本。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
这篇论文介绍了一个名为 Cobblestone（鹅卵石） 的新工具，它的任务是帮助计算机自动证明复杂的数学定理，从而确保软件没有漏洞。
为了让你轻松理解，我们可以把“形式化验证”（Formal Verification）想象成建造一座极其坚固的摩天大楼，而“证明定理”就是确保大楼每一块砖、每一根钢筋都符合安全标准。
1. 背景：为什么我们需要 Cobblestone？
- 传统方法（人工证明）： 就像让一位超级建筑师（数学家）亲自去检查每一块砖。这非常安全，但太慢、太贵、太累了。很多软件因为没时间检查，所以带病运行。
- 旧版 AI 方法（大语言模型）： 就像让一个很有才华但有点“幻觉”的实习生（AI）一次性写出整份检查报告。
- 问题： 实习生可能写得很像那么回事，但中间藏着一个致命的错误。一旦出错，整份报告作废，之前的努力全白费。
- 现状： 以前的 AI 工具只能证明大约三分之一的定理，剩下的都搞不定。
2. Cobblestone 的核心魔法：分而治之（Divide-and-Conquer）
Cobblestone 不要求 AI 一次性写出完美的整份报告。它采用了一种**“拆积木”**的策略。
想象一下，你要拼一个巨大的、复杂的乐高城堡（证明一个大定理）。
- 以前的做法： 让 AI 闭着眼睛，一口气把几百块积木拼好。如果拼错了一块，整个城堡塌了，AI 只能重头再来。
- Cobblestone 的做法：
- 先试一把： 让 AI 试着拼一下整个城堡。
- 智能检查（Fail-Safe Mode）： 即使城堡没拼好，Cobblestone 也不会直接扔掉。它会像一位超级质检员一样，拿着放大镜仔细检查：
- “嘿，左边这面墙（子证明）拼得完美无缺！” -> 保留！
- “右边这扇窗户（子证明）拼错了，卡住了。” -> 标记出来，暂时用胶带（admit）粘住，先不管它。
- 逐个击破： 现在，问题变小了！Cobblestone 不再纠结整个城堡，而是专门盯着那个“卡住的窗户”，再次让 AI 尝试拼好它。
- 循环往复： 如果拼窗户又失败了，Cobblestone 就把窗户拆成更小的零件（子子证明），继续让 AI 尝试，直到拼好为止。
- 最终组装： 最后，把之前保留的完美墙壁、新拼好的窗户，还有用其他工具（CoqHammer，一种传统的数学计算器）算出来的部分，全部拼在一起。
比喻总结： Cobblestone 就像一个聪明的项目经理。它不指望员工（AI）一次就做出完美的产品，而是把大项目拆成无数个小任务。只要员工完成了其中一部分，就把它存起来；剩下的部分，继续拆分、继续尝试，直到所有小任务都完成，最后组装成一个完美的整体。
3. 它是怎么工作的？（三个关键步骤）
- 大试身手： 先让 AI 尝试一次性搞定。
- 故障隔离（Fail-Safe Mode）： 这是 Cobblestone 的独门绝技。如果 AI 搞砸了，它能精准地指出：“哪里是对的，哪里是错的”。它不会让错误把整个证明过程“污染”掉，而是把正确的部分“抢救”出来。
- 递归修补： 对于搞砸的部分，它不是放弃，而是递归（自己调用自己）去解决更小的问题。就像你修车，如果引擎坏了，你不会把整辆车扔了，而是把引擎拆下来，再拆成零件，修好零件再装回去。
4. 效果如何？
- 更强大： 在四个不同的测试集（包括一些 AI 训练时没见过的最新代码）上，Cobblestone 证明的定理数量远超以前的工具。
- 更省钱： 虽然用了昂贵的 AI，但因为策略聪明，平均每个证明只花 1.25 美元，耗时约 15 分钟。
- 互补性： 它不仅能自己干，还能和人类专家或其他工具配合。如果人类给一点提示（比如“用这个定理”或“先拆成这三步”），它的成功率能飙升到 58%。
5. 为什么这很重要？
这就好比以前我们要检查一座大桥是否安全，必须请一群专家花几年时间手算。现在，Cobblestone 就像是一个不知疲倦、极其聪明的工程团队。它虽然偶尔也会犯错，但它懂得如何把大错误拆解成小错误，并且能利用所有正确的碎片，最终拼出一个绝对安全的结论。
一句话总结：
Cobblestone 不再强求 AI“一步登天”，而是教它“积少成多”。通过把大难题拆成小碎片，保留正确的，修补错误的，它让自动证明软件安全变得既高效又可靠。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。