OpenAI Lean 形式化题库曝漏洞：8 题可用错误证明绕过
gklambauer · x · 2026-10-09
博主 Timeroot 指出，OpenAI 的 Lean 形式化验证仓库中至少 8 个 comparator 挑战题存在可被破解的缺陷，并发布博客详细说明。
核心问题在于：许多本应固定的定义被错误地列在 . 的 definitionnames 字段里，意味着这些定义可以被自由改写而不影响 Comparator 的接受判定。作者以 EuclideanFiveColor.lean 为例，把 ProperColoring 定义改成 False 后，定理退化为平凡可证，仍能通过验证。
受影响的题目包括 Bernier、LogspaceEquality（即 L=RL=BPL）、KServer、Naimark、OccupiedOverlap、Rokhlin、SpinAngle 等。作者指出这比表面更危险：部分题目文件较短尚可人工核对，但另一些案例中定义可被篡改且不易察觉。据作者所知此前无人公开讨论过该问题。
「研究」频道最新
- U-Space:用机制可解释性找到 LLM 内部「不确定子空间」,无需训练可测信心 — Tobias Braun · 2026-10-09
- CARE:带统计保证的 VLA 推理加速认证,OpenVLA-OFT 提速 9-10.8 倍 — UMCP · 2026-10-09
- 评测文本扩散模型太难?新方法 SOL 用样本分布距离破局 — NandoDF · 2026-10-09
- MaRN 库用低维参数映射压缩网络:MNIST CNN 参数减 57.7 倍 — Less_Dream_6331 · 2026-10-09
- AI 进塔木德研讨会：专家意见分歧时如何评测 AI 成了难题 — EhudReiter · 2026-10-09
- TRL v1.15 融合 LM head，峰值显存省 82%、序列长 7 倍 — QGallouedec · 2026-10-09