形式化验证专家批 AI 圈认知落后 15 年：现代 FV 不靠 SMT 与翻译器

tianyin_xu · x · 2026-10-01

形式化验证领域知名学者 Grigore Roșu（转发者 tianyinxu）发文指出，AI 社区对形式化验证（FV）的理解停留在 15 年前：以为 FV 就是「用抽象逻辑生成验证条件（VC）再交 SMT 求解」或「把程序翻译到 Lean/Rocq/Dafny/Boogie 里去证明」。

他强调，现代 FV 的做法是为真实编程语言建立完整且经过充分测试的形式化语义，以之作为 ground truth / trust base，从而不必信任翻译器或抽象的「便利语义」。RV 团队声称拥有 25 年以上积累、面向 AI 生成代码最成熟的大规模 FV 技术，并公开征集有领域专用语言或应用的合作方；其引用的 RV 帖子点出核心问题：AI 几分钟能写出证明，但「谁来检查究竟证明了什么」。