MathAdv 基准开源:证明通过不等于评估结束,考察定理证明器四大能力
furongh · x · 2026-09-13
研究团队发布 MathAdv 基准（GitHub: margotyjx/MathAdv），主张「证明应确立定理，而不应终结评估」——一个证明通过不代表模型真正推进了数学理解。
要点：
- 基准同时用自然语言和 Lean 4 评估高级数学推理，仓库含 JSONL 数据、Lean 验证工具、API 与本地模型任务运行脚本及结果汇总工具。
- 数据目录含 fullproblems、proverproblems 与 combinedproverproblems 等集合。
- 除能力评估外，还包含 junktheorem 等探针实验，考察模型行为。
- 团队指出需要两类证据：可迁移的能力，以及人们能学习并在此基础上构建的想法；MathAdv 不衡量一个结果是否推进了人类数学理解。
所属事件:马里兰团队发布 MathAdv 基准：定理证明器难敌等价改写(2 条相关)→
「研究」频道最新
- MIT CSAIL 提出「机器学习与温习」范式:Agent 提前研究语料而非临时检索 — eshorten300 · 2026-10-31
- ARC Prize 2026 截止倒计时3天,Yi-Chia Chen 以 75.56% 登顶 ARC-AGI-3 — GregKamradt · 2026-10-31
- NVIDIA Nemotron 3.5 用 LLM 自验证:agentic 基准提升 9-10 个点 — sarahcat21 · 2026-10-31
- OpenTargets 非官方 MCP 服务器上线，可查询基因-药物-疾病关联 — modelcontextprotocol · 2026-10-31
- 研究者在模型权重空间找到 5 种人格结构,可类比人类大五人格 — luke_drago_ · 2026-10-31
- 单视图新视角合成基准被指错位，测试时优化对齐会误导评测 — kwangmoo_yi · 2026-10-31