AI首次实现代码与证明协同生成，自动验证分布式系统正确性。
Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems
- 用增量式联合合成法，边写代码边构造证明
- 7个分布式存储规范全通过，平均耗时6.8小时
- 适合需形式化验证的高可靠系统开发
AI代理在代码生成、测试和优化方面表现优异，但在需要完整覆盖性形式保证的任务上仍显不足。以分布式系统为例，读写一致性必须在所有可能的事件交错下成立，仅靠测试无法保障。机械化形式验证虽可确保正确性，但通常需数月到数年专家投入。实证显示，即使是当前最先进的编码代理（Codex with GPT-5.4 和 Claude Code with Opus 4.6），也仅能成功处理7个分布式键值存储规范中的2个。本文提出首个有效解决方案——归纳演绎合成（Inductive Deductive Synthesis, IDS），该方法联合且增量地同步生成实现与证明，并从失败尝试中学习，系统性探索有效策略。作为基于智能体的LLM系统，IDS在约6.8小时、平均每规格106美元的成本下完成全部7个规范，速度比专家快约200倍，成本低17%于现有最优代理。此外，IDS还将性能反馈纳入同一闭环，生成的实现速度最高可达已发表验证系统的3倍。
原文摘要 · Abstract (English)
AI agents increasingly excel at generating, testing, and refining code. However, they fall short on tasks requiring formal guarantees of full coverage that testing alone cannot provide. Distributed systems are a prime example: properties such as consistency between reads and writes must hold under every possible interleaving of events. Mechanized formal verification can guarantee such correctness, but typically demands months to years of expert effort. As evidence, even SOTA coding agents (Codex with GPT-5.4 and Claude Code with Opus 4.6) succeed on only 2/7 distributed key-value-store specifications. In this paper, we present the first effective approach to addressing this gap, Inductive Deductive Synthesis (IDS), which jointly and incrementally synthesizes implementation and proof, and learns from failed attempts to systematically try promising strategies. Built as an agentic LLM system, IDS achieves 7/7 in about 6.8 hours and $106 per spec on average, roughly 200x faster than expert effort and 17% cheaper than SOTA agents. IDS further incorporates performance feedback into the same loop, yielding implementations up to 3x faster than published verified systems.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。