OpenAI 内部模型协助发现 Lean 内核缺陷并已修复
RexDouglass · x · 2026-08-24
Lean 团队发布了关于利用 OpenAI 内部模型进行内核健全性(Bug)狩猎的复盘。在 OpenAI 研究员 Daniel Selsam 的协助下，AI 模型发现了官方 Lean 内核和运行时的多个新缺陷，现已在 v4.33.1 中修复。文档详细描述了如何指导 AI 模型使用 comparator 和 external checkers 等工具来发现潜在的对抗性证明漏洞，以提升对 AI 生成证明的信任度。
「安全」频道最新
- Anthropic 红队两年来首次“抹除”模型，GLM-5.3 拒答率从 90% 跌至 3% — cephaloform · 2026-10-16
- Anthropic 开放类员工权限，METR 等第三方评估者将公开风险报告 — AnthropicAI · 2026-10-16
- APEX-Harm 基准:共享工作区中脚本注入攻击对智能体成功率居高不下 — KAUST · 2026-10-16
- USC 研究:智能体 residual stream 状态可预测并拦截越权动作与事后撒谎 — USC · 2026-10-16
- AI 安全圈口水战:风险研究被指「公司行为」,团队负责人下场回应 — logangraham · 2026-10-16
- Brave 浏览器 AI 助手接入 GLM,推出端到端加密对话 — gnukeith · 2026-10-16