验证器也有 bug：QED 与 RISC-V Lean 模型接连被挑出漏洞
xennygrimmato_ · x · 2026-10-28
一串技术讨论揭示了「形式化验证工具本身也不可靠」的现实：
- 有人指出 QED SQL 等价性证明器存在多个 bug（GitHub issue：它把所有实数常量按 f32 解析再压成 i32/i32 分数，导致 16777217.0 与 16777216.0 等不同字面量被证为相等——不等价的查询被证明等价，超出范围的常量直接 panic）。
- 另一位开发者在把 Theorem Labs 的 RISC-V 模型从 Rocq 移植到 Lean 时发现两处 bug：解码器与规范在 5 条指令编码上不一致（拒绝 4 条合法指令、执行 1 条硬件会 trap 的保留指令）；fdiv 在极小结果向上舍入到最小规格化数时未置 underflow 标志。据其判断均不影响 Anthropic 已发表的结果，Theorem Labs 两天内确认并修复。
「编程与Agent」频道最新
- 用 logprobs 把 LLM 从硬分类器升级为可调阈值的软分类器 — JnBrymn · 2026-10-28
- Codex 团队日更系列第 23 天：跳过 iCloud 插件，进行一次重置 — dotey · 2026-10-28
- Cloudflare Access 支持 HTML+Liquid 自定义登录与拒绝页 — dinasaur_404 · 2026-10-28
- 查内存泄漏时 Opus 重试同一会话 2060 万次，开发者晒翻车现场 — johnlindquist · 2026-10-28
- 开源视频设计 Skill：让 AI Agent 按方法论做视频 — songguoxiansen · 2026-10-28
- 不是所有流程都需要 Agent:固定步骤用配方,别用 Token 跑 if 语句 — adamse · 2026-10-28