数学界的"活体检测"：LemmaBench如何让大模型从刷榜冠军变回新手

一句话：ENS Rennes与IP Paris团队造了一台"数学命题收割机"——每周从arXiv最新论文里提取引理，自动补全散落的定义和假设，把它们变成自包含的独立命题。顶级大模型来解，pass@1准确率10%-15%。竞赛刷榜的神话，在研究级数学面前碎了一地。

🎯 问题的本质：静态题库是温水煮青蛙

数学推理benchmark的危机不是今天才有的。

GSM8K、MATH、AIME——这些名字曾经是大模型数学能力的试金石。但随着训练数据规模膨胀到万亿token，一个幽灵始终盘旋：数据污染。模型在预训练时可能见过GSM8K的题目，甚至见过解法。它在测试时的"高分"，到底是真懂，还是背诵？

更隐蔽的问题是分布偏移。竞赛题和教科书题有固定模式：条件给足、符号规范、答案唯一。真正的数学研究论文里，引理往往嵌在论证链条中间，前面散着定义，后面跟着引用，假设藏在脚注里。一个引理可能需要你读完论文前三节才能理解它在说什么。这和"解一道应用题"是两种心智活动。

LemmaBench直面这两个问题。它的设计理念很简单：如果模型能证明今天数学家刚写在arXiv上的引理，那它就不是在背题库——因为题库还没编好。

🏗️ 流水线四步：从论文到考题

第一步：收割

流水线从arXiv数学类别（math.AG、math.PR等）抓取最新预印本，用正则表达式提取lemma、theorem、proposition等LaTeX环境。第二轮迭代还加了过滤：丢弃带引用的引理——那些是"已知结果重述"，不是新证明。

harvested 的引理数量不小，但大部分还不能直接用。

第二步：补全

数学论文的引理很少自包含。一个典型场景："由前述讨论可知，对于满足条件(3.2)的函数f，我们有..."——条件(3.2)在第7页，定义"函数f"在第3节，引理在第9页。

论文设计了两种补全策略：

全上下文检索：把引理之前的整篇论文内容喂给一个LLM，让它找出所有缺少的定义D和假设H，使引理在D和H下成为独立可证的陈述。

向量检索：只给引理本身，用embedding在论文里检索最相关的段落，再让LLM从中提取依赖。

实验结果很干脆：全上下文碾压向量检索。GPT-5全上下文模式下78.5%的引理被判定为自包含，向量检索只有49.4%。原因不复杂——数学依赖常常是长距离的，embedding的局部相似性捕获不了"第3节的定义被第9节的引理隐性使用"这种结构。

第三步：守门

补全后的引理交给LLM-as-a-judge做二检：这些附加定义和假设是否足以让引理独立？输出二值判定+推理过程。

人类数学家抽查验证了这套守门机制。结果：被LLM判定为"自包含"的引理中，75.5%-96.5%确实自包含（取决于提取模型和模式）。GPT-5是最高精度的守门员——它保守，假阴性多，但假阳性极少。

论文最终选了GPT-5做默认提取器。

第四步：考试

自包含的引理变成考题。模型拿到引理陈述+补全的定义/假设，尝试给出证明。LLM-as-judge评估证明有效性。人类数学家再抽查一部分，给LLM judge的可靠性打分。

关键设计：历史版本的LemmaBench可以用来训练模型，不会影响未来版本的评估——因为arXiv每周都在产出新论文。这就切断了"训练集泄露到测试集"的链路。

📊 结果：10%-15%意味着什么

先澄清：这不是"模型做对了10%的数学题"。这是"模型成功证明了10%-15%的最新研究级引理"。

研究级引理什么概念？它们是数学家为了推进某个前沿定理而发明的辅助结果。通常需要：理解一个非标准定义、识别隐藏的结构模式、构造一个非平凡的辅助对象、或者把几个已知技巧以新颖方式组合。这和GSM8K的"小明有5个苹果"不在一个宇宙。

被测模型的表现：

• GPT-5、Gemini 2.5 Pro/3 Pro、Claude 4.5 Opus、DeepSeek-R——全部落在10%-15%区间
• 没有显著赢家。顶级模型在研究级数学面前拉不开差距

这个结果有三层解读：

第一层，乐观：模型确实能证明一些研究级引理。不是零。说明基础推理能力存在，只是不稳定、不系统。

第二层，悲观：10%-15%意味着85%-90%的失败率。一个需要证明五个引理才能推进的定理，模型按独立概率算，成功率不到10⁻⁵。这在实际研究中等于零。

第三层，方法论：LemmaBench暴露的是领域泛化的崩溃。模型在竞赛数学上能到90%+，因为竞赛题有固定模式、有限技巧集、明确的问题结构。研究级数学的模式是开放的、技巧是未知的、结构是需要发明的。从竞赛到研究，不是量的差距，是质的断层。

❓ 诚实说不清楚的事

LLM-as-judge的可靠性天花板：论文人类验证了自包含性判定，但对证明有效性的验证主要依赖LLM judge。人类只抽查了子集。如果LLM judge对复杂证明的误判率不是均匀的——比如对构造性证明容易认可，对反证法容易误判——那10%-15%的数字会有系统性偏差。

引理难度的方差极大：arXiv论文的引理有 trivial 的（"由定义直接可得"），也有艰深的（需要二十页铺垫）。论文没有报告难度分布。如果10%-15%主要来自 trivial 引理，那实际能力更低。

自包含性判定的文化依赖：什么算"标准或经典"（standard or classical）而无需额外定义？这取决于数学子领域和评审者的背景。一个代数几何学家认为"standard"的概念，数论学家可能从未见过。LLM judge的判定标准是否稳定？论文没讨论。

动态更新的真实频率：论文说"可每周更新"，但实际第二轮迭代是2026年2月。从启动到第二轮隔了多久？动态更新的基础设施成本（arXiv抓取、LLM调用、人类抽检）是否可持续？没说。

训练数据与评估的边界：历史版本可用于训练。但如果一个模型训练时用了LemmaBench v1-v10，然后v11评估时表现更好，这到底是泛化能力进步，还是过拟合到了LemmaBench的风格？需要更精细的ablation。

🪞 我的判断

LemmaBench的价值不在"10%-15%"这个数字本身。在方法论层面的拨乱反正。

过去两年，大模型数学能力被一连串高分不断推高：GSM8K 95%+、MATH 90%+、AIME 80%+。舆论场开始讨论"AI数学家"、"AI辅助证明"。LemmaBench像一盆冷水：这些高分是真实的，但它们测量的是数学推理的初级阶段——模式识别、符号操作、已知套路的复现。研究级数学需要的不是这些。

更深一层，LemmaBench回应了一个AI评估领域的元问题：当基准被污染，整个评估大厦的地基就塌了。 动态评估不是新idea（LiveCodeBench、DyVal、NPHardEval都在做），但LemmaBench把它落地到了一个传统上极难自动化的领域——研究级数学证明。这需要的不只是技术，还有对数学出版流程的理解（arXiv结构、LaTeX环境、引理依赖模式）。

但我要泼一盆冷水回去。

LemmaBench的"动态防污染"是一个工程解决方案，不是概念突破。它防的是已发布论文的污染——模型训练时没见过这篇论文，因为论文刚发。但它防不了作者风格的污染。如果一个数学家A十年来的工作都被模型训练过，模型可能学会了A的思维模式。A的新论文虽没直接进训练集，但A的推理风格已经被编码。模型证明A的新引理，可能是在"模仿A的风格"，而不是"理解数学"。

这是更深层的数据污染——不是文本级别的重复，而是认知级别的同质化。LemmaBench对此无能为力。

还有一个讽刺：论文用LLM-as-judge来验证LLM的证明。这是用狐狸看守鸡窝。论文说"评估证明比生成证明更容易"——这是真的，但"更容易"不等于"可靠"。如果两个LLM的误判模式相关（比如都对某种错误视而不见），交叉验证也救不了。

尽管如此，LemmaBench是我2026年见过的最有价值的数学评估工作之一。不是因为它的结果多惊人，而是因为它诚实。10%-15%是一个让人不舒服的数字，但它可能是真实的。

项目	内容
核心贡献	(1) 首个从arXiv自动提取研究级引理并自包含化的动态数学benchmark；(2) 全上下文检索显著优于向量检索（78.5% vs 49.4%自包含率）；(3) GPT-5是最高精度的自包含性守门员（假阳性极少）；(4) 顶级模型研究级引理证明pass@1仅10%-15%，揭示竞赛数学与研究数学的质性断层；(5) 历史版本可训练而不影响未来评估，切断数据污染链路
关键局限	LLM-as-judge的可靠性未完全人类验证；引理难度分布未报告；"标准/经典"定义的文化依赖未讨论；动态更新基础设施成本未量化；认知级别同质化污染无法防御

参考文献：

1. Peyronnet et al., "LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics", arXiv:2602.24173v1, 2026.
2. Jain et al., "LiveCodeBench", 2024 (动态评估灵感来源).
3. Patel et al., 2023; Alexander et al., 2026 (arXiv自动形式化挑战).

#大模型评估 #数学推理 #数据污染 #动态基准 #arXiv #定理证明 #智柴