Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems¶
会议: NeurIPS 2026
arXiv: 2605.23109
OpenReview: https://openreview.net/forum?id=jp8UqwXlAw
代码: https://github.com/skydiscover-ai/skydiscover
领域: LLM Agent
关键词: 形式化验证, 归纳演绎综合, 分布式系统, 神经符号系统, LLM Agent
一句话总结¶
提出归纳演绎综合框架（IDS），通过演进式协同联合生成系统实现代码与机器可检查证明，并结合形式化证明检查器反馈与性能基准评测闭环优化，使 AI 智能体在数小时内自主生成具备形式化正确性证明且高性能的分布式键值存储系统。
研究背景与动机¶
近年来基于大语言模型（LLM）的编程智能体在代码生成、测试驱动修复和日常软件工程任务中取得了令人瞩目的进展。然而，测试只能覆盖抽样的输入轨迹，无法对系统的所有可能行为提供完备的正确性保障。在分布式系统等高并发、高容错的关键领域，读写一致性必须在所有可能的消息交错、节点故障和网络乱序下严格成立，一旦出现细微状态不一致，将引发分布式存储数据丢失、文件系统写丢失或安全凭据泄露等灾难性故障。机械化形式化验证虽然能提供绝对可靠的正确性证明，但传统上极度依赖人类专家的繁琐劳动，验证工业级系统往往耗费数月甚至数年的人力成本。
直接将形式化规约与验证工具链交给前沿编程智能体（如搭载 GPT-5.4 的 Codex 与搭载 Claude Opus 4.6 的 Claude Code）并不能解决问题：在分布式一致性规约基准测试中，SOTA 智能体仅能在 2/7 的简单规约上成功。其根本瓶颈在于人类开发者惯用的「先写完整代码，再后置补全证明」的结构性假设——这种模式迫使模型在最终步骤一次性输出庞大复杂的全量归纳模拟证明，且将形式化检查器的反馈推迟到了最末端，使智能体丧失了在早期搜索空间中及时止损和纠偏的向导信号。
针对这一困境，本文的核心洞见在于：不能将形式化验证作为后置的被动验收步骤，而应将其融入每一步系统构建与状态表示推演中，让代码与证明同步演进，并在证明受阻时自适应反思调整系统实现。本文的核心 idea 是：提出归纳演绎综合框架（IDS），以形式化检查器为部分证明 Oracle 联合递增合成实现代码与机器证明，由演绎智能体自顶向下递归解耦构造，并由归纳智能体在证明受阻时总结失败模式、自适应重构底层数据表示与战术引理，在单循环中同时实现形式化正确性保证与端到端性能调优。
方法详解¶
整体框架¶
IDS 系统将形式化规约（Specification）作为输入，目标是自动生成严格满足规约的分布式系统实现及其在定理证明器（如 Rocq / Coq）中完全闭合、无未证明假设（无 Admitted）的机器可检查证明，同时保证生成系统在真实分布式集群上的执行性能。
整个系统架构由协调器（Coordinator）统一调度，驱动演绎综合智能体（DSA）、归纳综合智能体（ISA）、形式化证明类型检查器 Oracle（Rocq Type-Checker）、分布式性能基准测试模块（Performance Benchmark Harness）以及非平凡性审计器（Non-vacuity Auditor）共同运作。其端到端执行流程如下图所示：
%%{init: {'flowchart': {'rankSpacing': 24, 'nodeSpacing': 28, 'padding': 6, 'wrappingWidth': 400}}}%%
flowchart TD
A["输入：形式化一致性规约<br/>Module Type (State, Update, Methods)"] --> B["联合递增综合流程<br/>DSA 演绎智能体递归解耦代码与证明"]
B --> C["形式化部分证明检查 Oracle<br/>Rocq 严格检查未完成证明占位符"]
C -->|类型检查错误 / 搜索停滞| D["双视界归纳干预机制<br/>ISA 智能体分析失败上下文"]
D -->|战术停滞：补全辅助引理| B
D -->|战略死胡同：重构底层数据结构| B
C -->|无错误推进| E["基准性能前置反馈闭环<br/>提取 OCaml 代码并在分布式集群压测"]
E -->|吞吐 / 延迟反馈指导结构选择| D
E -->|证明完全闭合 Qed| F["非平凡性与规约一致性审计<br/>排除恒真/空保护平凡解"]
F --> G["输出：通过机器严格验证的<br/>高性能分布式系统实现与完整证明"]关键设计¶
1. 联合递增综合与部分证明 Oracle：将代码演化与形式化证明在单步搜索中原子绑定
传统代码生成与验证割裂的流程中，代码完全写定后往往引入了极难归纳证明的全局交错状态。IDS 将代码和证明的演进完全同步：DSA 在引入或修改每一个数据结构、状态转换或消息处理逻辑时，必须同时配对声明对应的证明义务或将其分解为更局部的子引理。为了在综合未完成阶段评估搜索分支的健康度，系统利用现代证明助理（如 Rocq）的类型系统作为中间状态 Oracle：未完成的证明步骤用待定占位符（Admitted）显式标记，只要类型与命题签名结构自洽，Rocq 依然能对其进行无假阳性的严格类型检查。一旦中间形式化检查报错，智能体能立刻捕捉具体子目标、假设上下文及战术回溯栈，在产生偏差的最早节点实施局部修复或回滚，防止在无效甚至不可证的死胡同实现上浪费计算预算。
2. 归纳综合智能体（ISA）的双视界反思与表示重构：从失败中跳出局部极值 当 DSA 智能体在某个搜索路径上反复尝试仍无法闭合证明、陷入停滞时，单一的演绎推演无法自我突破。IDS 引入了基于全局历史反思的 ISA，将其解耦为两层决策视界： - 战术 Proposer 角色：当当前的系统整体架构合理但卡在具体的局部证明子目标时，Proposer 从全局证明状态出发，提出缺失的关键归纳引理或结构性子目标解耦方案，辅助 DSA 跨越战术难点； - 战略 Reloader 角色：当系统陷入根本性的战略死胡同（例如沿用规约默认的全局状态表示导致并发消息证明状态空间组合爆炸）时，Reloader 会强制中止该分支，总结既有失败经验并重新启动全新的高层架构设计。例如在因果一致性验证中，首个朴素设计将多副本状态存储为统一大对象导致证明无法拆分，Reloader 强制推翻并转为采用基于 Key 的局部哈希表/关联列表存储，使原本庞大的归纳模拟目标自然拆解为相互正交的单 Key 子引理集合。
3. 基准性能前置反馈与非平凡性审计：兼顾执行效率与形式化真理
形式化验证面临两大现实威胁：一是形式化证明可能通过逻辑漏洞或不合理守卫达成「平凡解（Vacuous Truth）」（例如智能体曾生成恒返回 false 的 Put-Guard，导致一致性定理在空前提下平凡成立）；二是形式化验证生成的纯函数式代码可能提取出效率极其低下的嵌套闭包。为此，IDS 设立了双重防线：首先，在证明仍在进行但单次候选实现成型时，协调器自动将其提取为原生 OCaml 可执行程序并在分布式集群测试床上执行真实负载压测，把吞吐量和 P99 尾延迟数据作为额外上下文反馈给 ISA，使 ISA 能主动放弃链式查找等低效结构并指导 DSA 选用平衡树或扁平列表；其次，当候选证明全部闭合（Qed）后，协调器执行非平凡性审计，验证其接口一致性与行为非空约束，确保最终交付的代码既是严格正确的，又是工程高效的。
一个完整示例：从规约到拆解证明¶
以因果一致性（Causal Consistency）规约为例： 1. 规约定义：规约要求若操作 \(A\) 因果先于操作 \(B\)，则任何观察到 \(B\) 的副本必须已观察到 \(A\)。规约层面自然地将所有副本状态描述为一个全局映射函数。 2. 初次尝试（全局状态）：DSA 按照规约形式直接构建全局多副本消息日志，在证明远程消息递送保持因果关系时，归纳不变式必须同时对网络中所有在途消息量化，DSA 连续尝试 15 轮辅助引理均告失败，触发协调器超时判定。 3. ISA Reloader 干预：ISA 识别出「全局状态导致消息与 Key 强耦合」的根本失败模式，向协调器发出重载指令，指导 DSA 改用「每 Key 独立条目 + 发送者向量钟」的分解存储表示。 4. 子引理拆分与证明闭合：在新的状态表示下，证明目标被自然拆分为三个相互解耦的引理类：单消息有效性、单 Key 存储条目保序性以及副本向量钟代数性质。DSA 针对每个子引理生成局部证明，Rocq 严格检查通过，最终输出 3,037 行、79 个引理的完整验证代码。 5. 性能回测：OCaml 提取产物在 5 节点 GCP 集群上实测吞吐量达 152 kops/s，相较于人类专家参考实现的函数闭包链提升了 3 倍吞吐。
实验关键数据¶
主实验¶
在分布式键值存储的 7 个代表性一致性规约上，对比 IDS 与前沿通用编程智能体 Codex（GPT-5.4）和 Claude Code（Opus 4.6），评估通过率（3 次独立运行中成功次数 \(\ge 2\) 为通过）、总耗时与推理成本。
| 规约名称 (Specification) | 难度类别 | Codex (GPT-5.4) 通过率 | Claude Code (Opus 4.6) 通过率 | IDS (本文) 通过率 | IDS 平均耗时 (小时) | IDS 平均成本 ($) |
|---|---|---|---|---|---|---|
| Chapar Causal Consistency | 复杂跨副本 | 0/3 (12h, $160) | 0/3 (11h, $165) | 3/3 | 10h | $148 |
| Read-Your-Writes (RYW) | 基础会话 | 3/3 (4h, $60) | 3/3 (3h, $70) | 3/3 | 2h | $52 |
| Monotonic Reads (MR) | 多分支会话 | 0/3 (12h, $130) | 0/3 (10h, $140) | 3/3 | 7h | $102 |
| Monotonic Writes (MW) | 基础会话 | 2/3 (5h, $65) | 3/3 (4h, $70) | 3/3 | 3h | $58 |
| RYW + MW (组合规约) | 多分支会话 | 0/3 (9h, $125) | 1/3 (6h, $110) | 3/3 | 5h | $93 |
| IDS Suite CC (显式依赖集) | 复杂跨副本 | 0/3 (12h, $160) | 0/3 (11h, $170) | 2/3 | 11h | $155 |
| Labeled CC (LCC, 标签过滤) | 复杂跨副本 | 0/3 (13h, $180) | 0/3 (11h, $160) | 3/3 | 10h | $136 |
| 总计 / 平均 (Total across specs) | 全集 (7 项) | 2/7 (67h, $880) | 2/7 (56h, $885) | 7/7 (48h, $744) | 6.8h/spec | $106/spec |
同时，在通用定理证明基准上，IDS 的 DSA 模块展现了跨语言通用性： - DafnyBench: 达到 88/100（Codex 为 78，Prior SOTA 为 52）； - miniCodeProps (Lean 4): 达到 100/100 满分（Codex 为 80，Prior SOTA 为 49）； - Verus-Bench (Rust): 达到 149/150（Prior SOTA 为 137）； - CoqStoq (Coq): 达到 97/100（Codex 为 46，Prior SOTA 为 28）； - VERINA (Lean 4 代码+证明): 达到 176/189（Prior SOTA 仅 38，提升 363%）。
消融实验¶
在 7 个分布式存储规约及 189 项 VERINA 任务上对核心组件进行消融分析：
| 配置 | 变动说明 | 7项分布式规约成功数 (每项3次) | VERINA 成功数 (/189) | 关键结论 |
|---|---|---|---|---|
| Full IDS | 完整系统 | 20 / 21 (7/7 均满足 \(\ge 2/3\)) | 176 | 保持高成功率基准 |
| w/o Joint (-J) | 去除联合综合，先生成代码后补证明 | 4 / 21 (仅 RYW 与 MW 部分成功) | 160 (-16) | 证明后置导致无法修正不宜证明的实现表示 |
| w/o Proposer (-P) | 去除 ISA 战术引理提议器 | 7 / 21 (MR、CC、LCC 全军覆没) | 150 (-26) | 复杂证明中缺乏全局视角辅助引理导致证明停滞 |
| w/o Reloader (-R) | 去除 ISA 战略重载器，不重构数据表示 | 9 / 21 (复杂规约全军覆没) | 167 (-9) | 无法从死胡同数据结构中跳出 |
| w/o Audit (-A) | 去除后置非平凡性审计 (统计实际有效解) | 7 / 21 | 176 | 证明器易接纳带空守卫的平凡真解 |
| w/o Verifier Feedback (-VF) | 去除富诊断，仅保留 Accept/Reject | 3 / 21 (所有规约最多 1/3) | 110 (-66) | 证明器上下文诊断是指导 LLM 探索的根本核心 |
| w/o Perf Feedback (-PF) | 去除性能前置基准反馈 | 20 / 21 (功能通过，但性能劣化) | - | 产出系统吞吐量下降 29.6%（平均仅为完整版 0.70×） |
关键发现¶
- 联合协同是打破复杂度诅咒的关键：去除联合递增综合（-J）后，系统在所有中高难度分布式规约（MR, RYW+MW, CC, LCC）上的通过率直接归零。这证明对于系统级的大规模证明，一旦先验固定了非最优的代码数据结构，证明空间将庞大到无法搜索。
- 形式化类型检查器反馈的不可替代性：去除详尽诊断信息（-VF）导致 VERINA 任务得分暴跌 66 题，分布式系统规约几近全面瘫痪。证明器给出的精确未完成子目标、局部假设及回溯信息构成了比测试用例更强大且绝对准确的搜索引导。
- 真实性能突破人类参考基线：在 Monotonic Reads 和 IDS Suite CC 上，IDS 生成的平衡树与扁平映射结构避免了人类专家在函数式提取中留下的深度闭包链（Closure Chain Walk），将 Get 操作开销从随负载线性递增优化为常数/对数级别，在 MW 和 RYW+MW 上成功规避了专家实现的超时崩溃。
亮点与洞察¶
- 将验证从后置门槛转化为前置搜索向导：传统认知认为形式化验证是软件开发的负担，IDS 证明通过把严格的类型检查器作为中间 Oracle，智能体反而能够借助形式化系统提供的即时确定性信号规避盲目搜索，将验证转化为生成有效系统的强力引擎。
- 计算换专家时间的范式转移：Chapar 因果一致性存储系统的形式化验证最初耗费了形式化领域专家 9 至 12 个月的繁重劳动，而 IDS 借助标准商用 API 在约 10 小时、148 美元的预算下全自动闭合了 3,037 行机器可检查证明，展示了通过算力自主突破高壁垒形式化工程的可行性。
- 数据表示驱动证明结构解耦：论文揭示了一个深刻的系统与证明共生规律——更易于形式化证明的状态表示往往具有更清晰的局部独立性，而这种局部独立性在系统工程上恰恰对应着更优的数据局部性与执行吞吐。
局限与展望¶
- 规约构建依然是人类瓶颈：IDS 依赖预先编写的精确形式化规约（如 Rocq Module Type）。撰写完整、严密且反映真实业务意图的形式化规约本身仍极具挑战，若规约存在漏洞，系统将无法察觉。
- 尚未覆盖生产级运行时运维面：当前规约集中于读写一致性安全属性，未涵盖分布式存储在生产环境所需的动态节点伸缩（Scale-out）、在线重配置（Reconfiguration）、故障容灾恢复（Crash Recovery）以及日志可观测性等运维接口。
- 未来方向：作者团队正探索基于多轮自然语言交互的人机对抗式规约综合（Adversarial Spec Synthesis），以及从既有复杂未验证系统中自动提取形式化规约并由 IDS 重新综合的逆向工程路径。
相关工作与启发¶
- vs 纯测试驱动的代码生成智能体 (如 SWE-agent, Reflexion, MetaGPT)：后者依赖执行测试用例获取反馈，对于极端并发交错与边界故障无法提供完备性保证，且易在未覆盖分支产生静默 Bug；IDS 引入形式化定理证明器作为绝对真理 Oracle，生成具备全输入空间数学保证的代码。
- vs 传统程序综合 (如 CEGIS, Sketch, Deductive Synthesis)：传统形式化综合由于状态爆炸通常局限在数十行的小型玩具函数；IDS 结合 LLM 的大模型先验知识与归纳演绎多智能体协同，首次将机器可检查综合扩展至多节点复杂分布式系统。
- vs 代码后置的自动化证明器 (如 CoqStoq, Baldur, Goedel-code-prover)：现有定理证明工作通常固定人类写好的代码，仅让模型填补证明；IDS 采用代码与证明联合推演，当证明卡壳时主动调整代码实现的数据布局以降低证明难度，从根本上重塑了证明可行性。
评分¶
- 新颖性: ⭐⭐⭐⭐⭐ (首次实现 LLM 驱动的大规模分布式系统代码与证明联合递增综合，突破了后置验证的传统范式)
- 实验充分度: ⭐⭐⭐⭐⭐ (覆盖 7 个分布式一致性规约、4 项跨语言证明基准及 3 项代码+证明基准，包含详尽消融与 GCP 分布式集群端到端压测)
- 写作质量: ⭐⭐⭐⭐⭐ (逻辑推演严密，架构清晰，深入剖析了失败案例与状态表示重构机制)
- 价值: ⭐⭐⭐⭐⭐ (为高可靠关键基础设施软件的自动化开发树立了新里程碑，有力推动了形式化验证走向实用化落地)