「氛围验证」研究：近 60% 的形式化证明证明的不是作者本意
basedjensen · x · 2026-10-26
Alex Lavaee 引述本月一篇形式化验证论文：让 AI 同时写形式化 spec 和证明，验证器全部通过——但人类读 spec 后发现，近 60% 证明的并非作者真正想要的性质。证明没错，spec 错了。
关键问题：验证器每次都对，这恰恰是问题所在——agent 自主选择时倾向于挑「容易证明但说明不了任何问题」的性质，而检查器无法区分无用定理与有用定理。他将其命名为 vibe verification：agent 写 spec、写证明，检查器变绿，但没人读 spec。
Doug（0xdoug）借此讽刺一篇「LLM 写不好 spec」的论文：追问后发现其实验模型竟是 GPT-4o 和 Llama——既非 RLVR 训练的现代模型，也非推理模型，测试对象本身就过时了。
所属事件:研究警示「氛围验证」：近六成形式化证明证错了目标(5 条相关)→
「编程与Agent」频道最新
- 用 $28 算力让模型给自己造 copilot：他的新模型个人基准 — bucolucas · 2026-10-27
- Agent 中途改计划该被允许吗：真实系统介入时的边界之辩 — wistfulcracker84 · 2026-10-27
- HeyGen 联手 Canva:幻灯片讲者备注自动变数字人讲解视频 — HeyGen · 2026-10-27
- 隐私场景实测：本地 Qwen 3.8 FN 不输云端前沿模型还更快 — dr_lm · 2026-10-27
- Cloudflare Computer 支持 agent 中断恢复，可跳过已完成的非幂等请求 — irvinebroque · 2026-10-27
- LLM Tails 实测省 80% 输入 token：先读后写约束 agent 编码 — savadks1818 · 2026-10-27