IDS 论文入选 NeurIPS Oral:代码与形式化证明协同演化,成功率 3 倍于 Claude Code
adityagp · x · 2026-09-25
- 团队的研究 IDS(Inductive Deductive Synthesis)被 NeurIPS 2026 选为 Oral(据称 top 0.34%),论文与代码均已开源。
- 核心思路:不再让 agent 生成代码后祈祷测试通过,而是给定 Lean/Rocq 形式化规格后,增量式地协同合成「证明 + 代码」,用证明约束代码正确性。
- 在分布式系统规格上,IDS 的成功率约为直接用 Claude Code 生成代码的 3 倍,超过现有 SOTA 编码 agent。
- 团队还预告了下一步挑战:确保形式化规格本身能准确捕捉人类意图。
所属事件:IDS 论文入选 NeurIPS Oral,可自动合成带证明的代码(3 条相关)→
「编程与Agent」频道最新
- Quail 深度解析:自研调度器与 vLLM 内核如何炼成 1B token/分钟 — sh_reya · 2026-09-25
- Modal 联手开源 Quail:AI-SQL 引擎单 H100 每分钟跑 10 亿 token — sh_reya · 2026-09-25
- Agent 代码淹没 CI：Anthropic 六个月 CI 任务量暴涨 25 倍的应对 — JeremyCMorgan · 2026-09-25
- Perplexity Fast Search 入驻 Hermes Agent,p50 延迟 160ms 且免费 — denisyarats · 2026-09-25
- Cursor 发布 Projects:一个协调者指挥数千子智能体,重度用户 PR 合并量提升 6 倍 — gaganghotra_ · 2026-09-25
- NetworkChuck 演示 Paperclip：让任意 AI Agent 当「员工」协作干活 — AIFlow_ML · 2026-09-25