形式验证老兵批 AI 圈:垃圾语义进,垃圾验证出
tianyin_xu · x · 2026-09-20
形式验证（formal verification）专家 Grigore Rosu 指出，这个始于 1960 年代的计算机科学老领域正在被热门新领域反复"重新发现"——前几年是区块链，如今是 AI，而且每次都能看到新来者的无知与傲慢。
他批评的典型对话模式是：新人声称"用 Lean 形式验证就能保证代码正确"，却答不上"你的信任基础是什么""语言有没有形式语义"这类根本问题。他的结论是：垃圾（形式语义）进，垃圾（形式验证）出——Lean 只能保证代码符合你写的形式语义，语义本身错了，证明再漂亮也没用。
文末推荐 Runtime Verification 的博客学习如何正确做 FV，博客内容涵盖 AI 辅助 fuzzing 找到 WebAssembly 运行时 WAMR 的真实 bug、Linux C 代码的 Rust 重写与 Lean 证明验证流程、以及 Android Binder 驱动反序列化器的端到端 Lean 4 机器验证等案例。
所属事件:形式验证专家警告：Lean 证明不等于代码正确(2 条相关)→
「研究」频道最新
- 亿级规模 arXiv 完整数据集登 Hugging Face 热门榜 — secemp9 · 2026-09-20
- 谷歌 ScientistTwo 自主改进 86/107 个 ML 问题，成功率 80.4% — rohanpaul_ai · 2026-09-20
- 谷歌 ScientistTwo 论文：全自主多智能体框架产出可发表级研究 — rohanpaul_ai · 2026-09-20
- Gated Recurrent Transformer:3层循环深度模型打平12层GPT-2 — burny_tech · 2026-09-20
- 斯坦福造出 3.7 万 AI 科学家智能体虚拟药企 — Dr_Singularity · 2026-09-20
- 理论计算机学者自嘲：一年前质疑 LLM 证明猜想，如今已被打脸 — burny_tech · 2026-09-20