深耕形式化验证 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 发展节奏之争，形式化验证看似很有吸引力；作者认同其价值，但基于亲身经验，对它究竟能提供多少安全保障持更谨慎的态度——更关注「能证明的」与「需要信任的」之间的鸿沟。
所属事件:形式化验证研究者长文反思：形式化变廉价之后(2 条相关)→
「漫话AGI」频道最新
- Not Boring 长文：AI 具备泡沫三大特征，恰是泡沫形成的经典剧本 — Not Boring (Packy McCormick) · 2026-11-11
- 热帖：五年「再等等」之后，2026 年公司终于摊牌 — hey_abusiddik · 2026-11-11
- Jeremy Howard：LLM 是在「扮演」理解，如中文屋里的那个人 — Machine Learning Street Talk · 2026-11-11
- OpenAI 董事 Christiano：在座大多数人最可能的死因是 AI 事故 — notkilleveryoneist · 2026-11-11
- 「和你的数据聊天」是伪需求？关键差异在聪明的同事 — vboykis · 2026-11-11
- Ben Todd:AI 任务时长随能力呈超指数增长,不止营收 — ben_j_todd · 2026-11-11