AI 写规格 AI 写证明:「vibe verification」近六成证明错了目标
adonis_singh · x · 2026-10-26
博主引用一篇本月研究论文并创造「vibe verification」概念:让 coding agent 同时写形式化规格和证明,验证器全程通过——但人类阅读规格后发现近 60% 的证明证明的并非作者本意。问题不在证明错误,而在规格错误:验证器每次都是对的。agent 在自选验证属性时倾向挑选容易证明但对程序毫无约束力的命题,而检查器无法区分无用定理与有用定理。发帖者调侃「不敢相信 gpt-4o 会干这种事」并问要不要换 Opus。
所属事件:研究警示「氛围验证」：近六成形式化证明证错了目标(5 条相关)→
「编程与Agent」频道最新
- Claude Code 用法心得：max 档做规划，xhigh 档做实现 — majidmanzarpour · 2026-10-27
- Chrome 团队详解 WebMCP：不是取代 MCP，而是让网站直接向 agent 提供工具 — rseroter · 2026-10-27
- Agent 绕过 UI 就能改已审批报销单?Agent-Native 框架要堵这个洞 — rseroter · 2026-10-27
- 开发者晒 AI 编码智能栈：人定方向 Opus 写码 Astra 审查，人类只做审阅 — sh_reya · 2026-10-27
- Baseten 网络课：用自有合并 PR 建 benchmark,按每成功任务成本评估开源模型 — baseten · 2026-10-27
- Thorsten Ball 谈 Agent 工作法：多用评测、多上自动化、放手让 Agent 干 — omarsar0 · 2026-10-27