归纳演绎综合：让AI生成形式化验证的系统

AI智能体在生成、测试与精炼代码方面日益出色。然而，在需要测试本身无法提供的形式化全覆盖保证的任务上，它们力有不逮。分布式系统是典型例子：读写一致性等性质必须在事件的每一种可能交错下都成立。机械化形式验证可以保证这种正确性，但通常需要数月至数年的专家投入。作为证据，即使是最先进的编码智能体（搭载GPT-5.4的Codex与搭载Opus 4.6的Claude Code）也仅在7个分布式键值存储规约中的2个上成功。本文提出首个弥合这一差距的有效方法——归纳演绎综合（Inductive Deductive Synthesis, IDS），它联合且增量地综合实现与证明，并从失败尝试中学习以系统地尝试有前景的策略。作为一个智能体化LLM系统，IDS以约6.8小时、平均每规约106美元的成本实现7/7全解，比专家投入快约200倍，比SOTA智能体便宜17%。IDS还将性能反馈纳入同一循环，产出的实现比已发表的已验证系统最快快3倍。