Gary Marcus 质疑数学 AI 成绩：Lean 验证究竟试了多少解、怎么运作
GaryMarcus · x · 2026-10-07
Gary Marcus 追问某数学 AI 系统的验证细节：系统到底尝试并通过 Lean 形式化验证的解有多少？系统本身的运作机制是否有公开说明？
回复者 altryne 解释称，Lean 证明是独立运行的一道流程，用来「验证」非 Lean 的 agentic loop 产出的结果。Marcus 的追问指向一个关键问题：在最终成绩的宣称中，搜索空间规模与通过率等核心数据并未披露，外部难以评估其真实水平。
所属事件:Gary Marcus 与 altryne 激辩数学 AI 验证细节(2 条相关)→
「研究」频道最新
- Ofir Press：超人类阶段下，好的编程基准会越来越难做 — OfirPress · 2026-10-07
- 一线研究者：用 AI 做预训练研究仍需人类精确定义方向 — menhguin · 2026-10-07
- AI 投稿期刊数量一年增 5-10 倍,90% 不值得人工审阅 — menhguin · 2026-10-07
- COLM 论文:训练模型按情境切换提问、多答或直接猜 — JonathanBerant · 2026-10-07
- Google 团队 COLM 展示:可量化引导模型行为的研究 — JonathanBerant · 2026-10-07
- AI agent 一周完成顶尖 Lean 形式化,耗约 30 亿 token、13.5 万美元 — geoffreyirving · 2026-10-07