研究者用 AI + 形式化验证挖出 NetHack 三个变形 bug
davidbau · x · 2026-09-27
MIT 研究者 David Bau 分享了用 AI 辅助学习形式化方法编码的实践成果:他在玩 NetHack 时遇到异常,借助 AI 在变形(polymorph)代码 src/polyself.c 中定位到三个可复现 bug——
- 删除从未创建的光源,触发 "Program in disorder!" 系统错误
- 一次变形执行两次清理,产生两次神器爆炸和两次伤害判定
- 变形后仍按旧形态规则做判定:人类因「蝾螈穿不了靴子」被剥夺水上行走靴,站在岩浆中致死
他还用形式化验证发现自己的第一版修复仍有漏洞(第二次形态变化未被正确处理),已提交 issue #1682 和配套 PR,并询问在检查假设时如何避免遗漏。这是一手展示 AI 辅助调试 + 形式化验证工作流的案例。
「编程与Agent」频道最新
- Gemini 可直连 Airtable、Linear 等 10 款应用，附实操工作流 — alifcoder · 2026-09-27
- 用户拒绝 Chrome 权限，Codex 转身改用内置浏览器绕过 — andimarafioti · 2026-09-27
- Opus 5.5 加四个开源 skill,可顶一个初级剪辑师 — lxfater · 2026-09-27
- OmO V5 发布成功,桌面版将内置自动模型选择器 — jasonkneen · 2026-09-27
- 创业公司砍掉 27 个 Agent 只留 3 个：维护成本逼出架构重构 — AmosBarJoseph · 2026-09-27
- 开发者实测:Opus 5.5 多智能体编排体验惊艳 — daniel_mac8 · 2026-09-27