[AI]《Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems》S Agarwal, A Krentsel, S Liu, M Cemri… [UC Berkeley] (2026)
在AI生成系统领域，测试无法覆盖分布式并发的所有交错。现有编码代理受困于“先写代码、再补证明”，一旦设计走错，证明才暴露死路。
本文的核心洞见是：把系统生成重新看作代码与证明的同步搜索。由此，每次实现改动都配套局部证明，并由Rocq即时判定可行。
这项工作留下的遗产是把验证系统构造从专家月级劳动压缩到小时级搜索。它打开的新门是机器检查的“可信编码”；门槛是仍依赖人工写好形式化规格。
arxiv.org/abs/2605.23109 机器学习 人工智能 论文 AI创造营
