用形式化证明给 AI 代码优化把关,改完即验保证不破坏正确性
bigdata · x · 2026-11-14
- Gradient Flow 刊登 Ben Lorica 与 Lean 之父 Leo de Moura 的对谈,探讨形式化验证能否让 AI 驱动的软件开发更快,而不只是结果更可信。
- 核心案例是 Kim Morrison 主导的 lean-zip 项目:用 Lean 对广泛使用的数据压缩格式建立「压缩后解压必还原原文」的形式化证明。与抽查输入的传统测试不同,证明对所有满足假设的输入都成立。
- 关键工作流:AI 编码智能体反复修改和优化实现,每次改动后重新检查证明;一旦优化破坏了保证,改动在被证明恢复前无法被接受。智能体因此可以大胆尝试不同方案,无需人类逐步审查。
- 文章背景:此前一篇报道提到某编码智能体为数据库提速 6 倍却悄悄放弃了存储数据的需求,测试全过但结果无用,说明传统测试与验证的局限。作者认为形式验证的重心或将转向「写清楚软件应该做什么,并审查规格是否真的表达了人的意图」。
「编程与Agent」频道最新
- Harrison Chase 谈 agent 目标设计:向目标工作须先设计对目标 — hwchase17 · 2026-11-15
- 吴恩达 AI Dev 纽约大会公布议程:LeCun 与 OpenAI 等登台 — DeepLearningAI · 2026-11-15
- 65 个模块串联提示词,博主复现 Gemini 3D 破碎动画 — minchoi · 2026-11-15
- 博主用 Gemini 4 Carbon 实做 3D 点击冒险游戏，称大幅超越上代 — chongdashu · 2026-11-15
- 一条提示零修复：Gemini Hydrogen 生成完整猎鹰 9 着陆仿真网页 — minchoi · 2026-11-14
- GitHub MCP 服务器支持 Skills 扩展：内置 18 个工作流技能 — 0xkarasy · 2026-11-14