Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems
本文介绍了归纳演绎合成（IDS），这是一种智能体大语言模型系统，能够联合合成分布式系统的实现与形式化证明，在键值存储规范上实现了100%的成功率，且相较于人类专家和最先进的编码智能体，显著降低了时间和成本。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你正在构建一个复杂的分布式系统，比如一个数字银行或一个多人同时使用的共享笔记本。你需要确保：如果 A 写了一条笔记，B 能立即看到它；无论网络变得多么混乱，数据永远不会丢失或混淆。
传统上，构建此类系统有两种方法：
- “猜测与检查”方式（当前 AI）：你请一个聪明的 AI 来编写代码。它编写代码，运行几次测试，然后说：“看起来不错！”但这就像只开一辆车过桥来检查桥梁是否安全。它可能能承受那辆车，但在卡车经过时可能会坍塌。它无法保证在所有可能的场景下都是安全的。
- “数学证明”方式（传统专家）：你雇佣一支由人类数学家和工程师组成的团队。他们不只是测试代码；他们会编写一个形式化的数学证明，证明代码不可能失败，无论发生什么情况。这极其安全，但需要数年的人力投入，且成本高昂。
问题所在：
论文指出，即使是最聪明的当前 AI 代理（如 Codex 或 Claude），也无法胜任“数学证明”这种方式。它们试图先编写代码，然后再尝试证明其正确性。这就像先建好房子，然后才请建筑师证明它不会倒塌，而此时砖块早已砌好。这太难了，它们因此陷入困境。
解决方案：归纳演绎合成（IDS）
作者创建了一种名为IDS（归纳演绎合成）的新 AI 系统。请将 IDS 想象成不是一个单一工人，而是一支在紧密循环中协作的专门建筑师与检查员团队。
以下是其工作原理，使用一个简单的类比：
“构建与检查”循环
IDS 不是先建好整栋房子再进行检查，而是构建房子的一小部分，并立即检查这一小部分在数学上是否可靠。
- 演绎团队（构建者）：这些 AI 代理尝试编写一小段代码（比如门框）和一小段证明（一句数学陈述，说明“这个门框是坚固的”）。
- 检查员（证明助手）：一位严格、目不转睛的机器人检查员（称为 Rocq）立即检查工作。
- 如果数学推导不成立，检查员会说：“不，这个门框很脆弱”，团队立即停止。他们不会在薄弱的基础上浪费时间去建造房子的其余部分。
- 如果通过，他们便进入下一个微小部分。
- 归纳团队（战略家）：有时，构建者会陷入困境。他们不断尝试构建同一种类型的门，但数学推导始终无法成立。这时，“归纳”部分就发挥作用了。
- 提议者：一位战略家 AI 审视卡住的地方，说道：“嘿，也许我们不该建木门；让我们试试钢门。”它提出一个新的局部解决方案。
- 重载者：如果整个策略都是错误的（比如试图在沼泽上建房），这位战略家会说：“废弃这个设计。让我们用完全不同的蓝图重新开始。”
为何这是一项重大突破
论文声称，该系统在三个方面具有变革性：
- 速度：它在约6.8 小时内解决了 7 个不同的复杂分布式系统问题。而人类专家团队完成同样的工作需要数月甚至数年。这大约快了200 倍。
- 成功率：现有最好的 AI 代理只能解决这 7 个问题中的 2 个。而 IDS 解决了全部 7 个。
- 性能：不仅代码正确，而且运行速度快。在某些情况下，IDS 生成的代码运行速度比最佳人类编写的版本快3 倍。这是因为 AI 探索了比人类通常更多的设计选项，找到了人类未曾发现的“最佳平衡点”。
局限性（注意事项）
论文非常诚实地指出了 IDS 目前尚不能做到的事情：
- 它需要完美的配方：你仍然需要一位人类专家来编写初始的“规范”（即系统应遵循的数学规则）。如果配方错误，AI 将建造一座完美的房子，但它不符合你的需求。
- 它目前还不是万能的魔法棒：他们专门在“键值存储”（一种数据库类型）上测试了该系统。虽然他们相信它可能适用于其他领域（如操作系统或加密），但尚未得到证实。
核心结论
这篇论文提出了一种使用 AI 的新方法，将构建与检查同时结合。它不再要求 AI“编写代码并希望它能运行”，而是要求 AI“编写代码并逐步证明它能运行”。
它将创建“完全安全”软件的过程，从一场缓慢、昂贵的人类马拉松，转变为一场快速、自动化的短跑，从而有可能使我们所依赖的软件（如银行应用或云存储）变得更加安全和可靠。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。