深耕形式化验证 8 年，Kaiyu Yang 反思形式化变廉价后能解决什么
KaiyuYang4 · x · 2026-09-25
- 作者 Kaiyu Yang 自 2018 年起研究机器学习用于形式化定理证明，开发过 CoqGym、LeanDojo 并参与 Goedel-Prover。这篇 25 分钟长文是他八年历程的个人反思。
- 当年的愿景是：AI 负责创造性工作，Lean 这样的严格形式系统负责验证。主要障碍是用 Lean 精确表达一切的成本太高。
- Codex、Claude Code 等编码智能体正在大幅降低这个成本：如今已能形式化费马大定理这类重大结果，并用规格与正确性证明构建大型软件项目。
- 但这引出一个更难忽视的问题：把命题形式化并在 Lean 中证明之后，我们到底解决了原始问题的多少？有时解决了很多，有时核心问题依然悬而未决。
- 结合近期 AI 智能体安全事件与前沿 AI 发展节奏之争，形式化验证看似很有吸引力；作者认同其价值，但基于亲身经验，对它究竟能提供多少安全保障持更谨慎的态度——更关注「能证明的」与「需要信任的」之间的鸿沟。
「漫话AGI」频道最新
- ICLR 投稿量激增被讽「Slopocene」：AI 垃圾论文 flooding 时代来临 — charles_irl · 2026-09-25
- 马斯克谈机器人终局:满足人类需求后,机器人将为自己干活 — XFreeze · 2026-09-25
- Index Ventures 合伙人：AI 攻击更快更便宜，人机协同防御模式或将失效 — RebeccaBellan · 2026-09-25
- Bengio 在联合国安理会警告：失控前沿 AI 智能体的空前威胁 — AnnaCiaunica · 2026-09-25
- 卡内基报告：韩国人才留存率 77% 居第二，KAIST 升至全球第三 — sehoonkim418 · 2026-09-25
- 从柠檬市场到夸赞之死：AI 如何摧毁「可验证的努力」 — aakashgupta · 2026-09-25