MathAdv 基准:定理证明器解原题却在等价改写上全军覆没
furongh · x · 2026-09-13
马里兰大学 Furong Huang 团队发布诊断性基准 MathAdv(arXiv:2608.25449),覆盖 13 个本硕数学领域,从四个维度评估定理证明器:Know(知识,选择题)、Reason(非形式推理,填空)、Formalize(Lean 4 形式化证明)、Generalize(专家设计的等价改写)。
核心发现:
- 脆弱性实锤:配对测试中 Goedel-Prover-V2 解出了六道原题,却在数学等价的改写版上全部失败,反向情况零次——说明脆性,虽不能直接证明记忆化;
- 形式化仍是主要瓶颈,且成绩在不同数学领域间差异巨大;
- 自然语言提示对通用 LLM 有帮助,反而会妨碍专精证明的模型;
- 聚合证明准确率掩盖了组件级评估才能暴露的能力与失效模式。
作者强调:该基准测的是模型行为,不等于结果推动了人类数学理解;对自我改进 agent 而言,「在什么上改进」需要另行检验。数据集与评估脚本已开源。
所属事件:马里兰团队发布 MathAdv 基准：定理证明器难敌等价改写(2 条相关)→
「模型」频道最新
- 用户吐槽 Linux 版 Codex 应用像没人管的养子,体验糟糕 — eigenron · 2026-10-31
- Kimi 支持俄罗斯 Mir 卡直接付款，订阅 Pro 无需中介 — teortaxesTex · 2026-10-31
- Nat Lambert：开源模型或是维系 AI 生态的关键粘合剂 — natolambert · 2026-10-31
- Gemini 4 Carbon 登顶 APEX-Agents 榜首,唯一均值破 90% 的模型 — Swarooprm7 · 2026-10-31
- Sarvam 为印度开发本地推理版 opencode,遭网友吐槽「本地」定义 — kingslyj · 2026-10-31
- MiniCPM-OCR 1.3B 模型每分钟可处理 128 页，2B 校验模型接近 397B 巨兽 — haider1 · 2026-10-31