归纳演绎综合：使AI生成形式化验证系统
人工智能
2026-05-25 v1 分布式、并行与集群计算
计算机科学中的逻辑
编程语言
摘要
AI智能体在生成、测试和改进代码方面日益出色。然而，在需要测试无法提供的全覆盖形式化保证的任务上，它们表现不佳。分布式系统就是一个典型例子：读写之间的一致性等属性必须在事件的每一种可能交错下均成立。机械化形式化验证可以保证这种正确性，但通常需要数月至数年的专家工作量。作为证据，即使是SOTA编码智能体（配备GPT-5.4的Codex和配备Opus 4.6的Claude Code）在7个分布式键值存储规范中也仅成功完成2个。在本文中，我们提出了解决这一差距的首个有效方法——归纳演绎综合（Inductive Deductive Synthesis, IDS），该方法联合且增量地综合实现与证明，并从失败的尝试中学习以系统性地尝试有前景的策略。作为基于智能体的LLM系统构建，IDS在约6.8小时内实现了7/7的成功率，平均每个规范花费106美元，比专家快约200倍，比SOTA智能体便宜17%。IDS进一步将性能反馈纳入同一循环，生成的实现比已发表的已验证系统快达3倍。
引用
@article{arxiv.2605.23109,
title = {Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems},
author = {Shubham Agarwal and Alexander Krentsel and Shu Liu and Mert Cemri and Audrey Cheng and Rui Meng and Tomas Pfister and Chun-Liang Li and Sylvia Ratnasamy and Aditya Parameswaran and Matei Zaharia and Ion Stoica and Mohsen Lesani},
journal= {arXiv preprint arXiv:2605.23109},
year = {2026}
}