形式化验证大佬泼冷水:没有形式语义,Lean 证明≠代码正确
JiaweiLiu_ · x · 2026-09-20
知名形式化验证专家 RosuGrigore 转发并警告拥抱「用 Lean 证明即正确」的新一代 AI 计算机科学家:脱离程序语言的形式语义,根本无法定义「正确性」。
他给出一个简单例子:同一段程序在 gcc 和 clang 不同优化级别下结果不同,先跑一遍再尝试在 Lean 里证明。结论是:形式语义才是真正的难点,它既需要人的判断也需要合适的语言框架,与 Lean 无关——Lean 只是在你有了形式语义之后才开始发挥作用。
这条观点对当下「AI + Lean 自动证明」热潮是有力的技术性纠偏。
所属事件:形式验证专家警告：Lean 证明不等于代码正确(2 条相关)→
「研究」频道最新
- 菲尔兹奖得主Villani谈OpenAI解千禧年难题:如数学史的末日浩劫 — GregCook2011 · 2026-09-20
- lateinteraction:论文只是时间戳格式,真正的项目「住」在别处 — lateinteraction · 2026-09-20
- 两名高中生借 AI 在菲尔兹奖得主研究问题上取得进展 — IgorCarron · 2026-09-20
- GPU 编程学习日志:精读 CUDA matmul 优化经典与 MIT 稀疏性课程 — NandoDF · 2026-09-20
- 新论文发现 grokking 第三阶段:训练后期泛化会崩溃回随机水平 — sytelus · 2026-09-20
- ICLR 投稿超 5 万篇，研究者提议人类与 LLM 混合编排评审 — HamedSHassani · 2026-09-20