数学与形式推理
突破级
有讲解视频
收录解读
- 分级：`突破性` - 正式标题：`LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics` - 原文：`2026-02-27-M2_LemmaBench-LemmaBench_A_Live_Research_Level_Benchmark_to_Evaluate_LLM_Capabilities_in_Mathe.pdf` - 抽取：`extracted.md`
## 重写摘要
LemmaBench 的核心想法很简单，但非常重要：如果数学 benchmark 总是静态题库，就迟早会被训练污染，最后失去评测意义。作者因此设计了一个“live benchmark”管线，从最新 arXiv 数学论文里自动抽取引理，并将其改写为自包含陈述，把隐含条件与依赖定义显式补全，从而得到可以持续更新的研究级数学评测集。
论文报告当前最强 LLM 在这类任务上的 pass@1 仍然大致落在 10% 到 15% 区间，说明在真实研究数学上，模型离可靠自动证明仍有很大距离。这一点本身就有价值，因为它把数学评测从竞赛题和教材题重新拉回到了研究前沿。
## 为什么重要
它修复了数学 benchmark 的两个老问题：`数据污染` 和 `题目竞赛化`。只要这条路线走通，未来数学模型的进步就更难靠记忆，而必须靠真正的形式推理和结构理解。
## 局限
自动补全定义与假设的管线本身可能引入微妙错误，因此它更适合作为趋势指示器，而不是毫无噪声的绝对标尺。