研究警示「氛围验证」：近六成形式化证明证错了目标
10 月 26 日，多位博主（@basedjensen、@burnytech、@adonissingh）转述本月一篇形式化验证研究论文，指出一种被 @adonissingh 命名为「vibe verification（氛围验证）」的现象：让 coding agent 同时编写形式化规约（spec）和证明，验证器每次都通过，但人类阅读规约后发现近 60% 的用例证明的根本不是作者真正想要证的性质。核心问题不在证明本身——验证器全部正确——而在于规约错了：机器验证通过并不等于证明了你想要的东西。
已确认
- 研究结论为：近 60% 的 AI 生成形式化证明所证性质与作者本意不符，错误源头是 AI 撰写的规约而非证明过程。
- @adonissingh 提出并传播了「vibe verification」这一概念，@basedjensen、@burnytech 以相近表述转发引述同一研究。
为什么重要
- @srchvrs 指出，当前不少公司和论文宣称 AI 辅助形式化验证取得突破：用 Rocq（原 Coq）等工具验证 AI 生成的代码，或用 Lean 检查 AI 产生的数学证明，这标志着 AI 能力评估从「能写代码」走向「可机器验证的正确性」。
- 但 @srchvrs 同时警示：形式化验证只保证证明被检查器验证通过，既不保证形式化定理真的捕获了原始数学命题或工程意图，也不保证代码实现了用户想要的功能。换言之，即便在「机器可验证」这一最强保证下，人类审读规约的环节仍不可省略，否则「验证通过」可能沦为一种新的错觉。
2026-10-26 ~ 2026-10-26 · 5 条相关
一手来源
- AI 写规格 AI 写证明:「vibe verification」近六成证明错了目标 — adonis_singh ·
- 形式化验证专家泼冷水:证明通过不等于代码实现了你想要的功能 — srchvrs ·
- 【源头】形式化验证专家泼冷水:证明通过不等于代码实现了你想要的功能 — srchvrs · 2026-10-26
- AI 辅助形式化验证宣称频出：Rocq 验证代码、Lean 验证明真成新前沿 — srchvrs · 2026-10-26
- 近60% AI形式化规约证明了「错误的东西」，验证器全程无误 — burny_tech · 2026-10-26
- 【源头】AI 写规格 AI 写证明:「vibe verification」近六成证明错了目标 — adonis_singh · 2026-10-26
- 「氛围验证」研究：近 60% 的形式化证明证明的不是作者本意 — basedjensen · 2026-10-26