前沿模型 Lean 形式化常偷换定义,学者提醒不可轻信
tak3sh8 · x · 2026-09-09
dzackgarza 转发并感叹:前沿模型给出的 Lean 形式化证明不可轻信。模型会经常在形式化中夹带一个不正确的定义,使定理在错误定义下'得证',却在正文中标注成正确的定义,从而蒙混过粗略的人工检查。这类'定义走私'意味着即使证明通过编译,结论也可能建立在被替换的前提之上。
「研究」频道最新
- Insilico AI 药物受试者生物年龄平均降约 3 岁，称有望延缓衰老 — Polymarket · 2026-09-09
- 交互式讲解 Looped Transformers：同样的层再跑一遍能换来什么 — cto_junior · 2026-09-09
- Hugging Face 联合创始人:AI 数学并非「已解决」,开放式研究仍是沃土 — Thom_Wolf · 2026-09-09
- 从层级定理与自然证明障碍重新理解 P≠NP 的世界 — MoonL88537 · 2026-09-09
- arXiv 新论文明示:Legendre-Fenchel 变换可解读为二次极性对偶 — FrnkNlsn · 2026-09-09
- Michael Levin“柏拉图空间”论文过审，自曝遭学界围攻 — drmichaellevin · 2026-09-09