LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics

📄 arXiv: 2602.24173v1 📥 PDF

作者: Antoine Peyronnet, Fabian Gloeckle, Amaury Hayat

分类: cs.AI

发布日期: 2026-02-27

备注: 15 pages, 3 figures, 5 Tables

💡 一句话要点

提出LemmaBench，一个评估LLM数学能力的实时研究级基准

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 数学推理 定理证明 基准测试 自动化评估

📋 核心要点

  1. 现有数学LLM基准依赖静态数据集，无法反映最新研究进展，限制了模型在实际科研场景中的评估。
  2. LemmaBench通过自动提取arXiv引理并重写为自包含陈述，构建可更新的、基于最新研究成果的基准。
  3. 实验表明，当前SOTA LLM在LemmaBench上的定理证明准确率仅为10-15%，提升空间巨大。

📝 摘要（中文）

本文提出了一种新的方法，用于评估大型语言模型（LLM）在研究级别数学上的能力。现有的基准主要依赖于静态的、手工整理的竞赛或教科书式的问题集，作为数学研究的替代品。相反，我们建立了一个可更新的基准，直接根据最新的数学研究成果评估模型。该基准包含一个自动化的流程，从arXiv中提取引理，并通过明确所有假设和所需的定义，将它们重写为独立的陈述。这使得基准可以定期更新，使用直接来自人类数学研究的新问题，而之前的实例可以用于训练，而不会影响未来的评估。我们对当前最先进的LLM进行了基准测试，结果表明，根据模型不同，定理证明的准确率约为10-15%（pass@1），表明LLM在研究环境中达到人类水平的证明能力还有很大的进步空间。

🔬 方法详解

问题定义：现有的大型语言模型（LLM）数学能力评估基准，如竞赛题或教科书习题，与实际数学研究存在较大差距，无法有效评估LLM在科研场景下的能力。这些基准通常是静态的、手工整理的，难以反映数学研究的最新进展，并且容易被模型记忆，导致评估结果失真。因此，需要一种能够动态更新、基于最新研究成果的基准来更准确地评估LLM的数学能力。

核心思路：LemmaBench的核心思路是直接从arXiv等预印本平台上提取最新的数学引理，并将其转化为适合LLM处理的自包含陈述。通过自动化流程，可以定期更新基准，使其始终与最新的数学研究保持同步。这种方法避免了手工整理数据集的局限性，并能够更真实地反映LLM在实际科研场景中的表现。

技术框架：LemmaBench的整体框架包含以下几个主要模块：1) 引理提取：从arXiv等平台抓取数学论文，并从中提取引理；2) 重写模块：将提取的引理重写为自包含的陈述，明确所有假设和所需的定义，使其可以在没有上下文的情况下被LLM理解和处理；3) 基准管理：维护一个可更新的基准数据集，并提供评估LLM性能的工具；4) 评估模块：使用不同的LLM对基准数据集进行测试，并评估其定理证明的准确率。

关键创新：LemmaBench最重要的技术创新在于其自动化构建和更新基准数据集的能力。与传统的静态基准相比，LemmaBench可以定期从最新的数学研究中提取问题，从而保持基准的新鲜度和挑战性。此外，LemmaBench通过将引理重写为自包含陈述，降低了LLM理解问题的难度，使其能够更专注于定理证明本身。

关键设计：LemmaBench的关键设计包括：1) 引理提取算法：使用自然语言处理技术从数学论文中识别和提取引理；2) 重写规则：定义一套规则，用于将引理重写为自包含陈述，包括明确所有假设和所需的定义；3) 评估指标：使用pass@k等指标来评估LLM的定理证明准确率，其中pass@k表示在k次尝试中至少有一次成功的概率。

🖼️ 关键图片

fig_0

📊 实验亮点

实验结果表明，当前最先进的LLM在LemmaBench上的定理证明准确率仅为10-15%（pass@1），远低于人类数学家的水平。这表明LLM在研究级别的数学问题上仍面临巨大挑战，LemmaBench提供了一个有价值的平台，用于跟踪和评估LLM在这一领域的进展。

🎯 应用场景

LemmaBench可用于评估和改进LLM在数学研究领域的应用，例如辅助数学家进行定理证明、自动生成数学证明、以及发现新的数学规律。该基准的实时更新特性使其能够持续推动LLM在数学领域的进步，并最终促进数学研究的自动化和智能化。

📄 摘要（原文）

We present a new approach for benchmarking Large Language Model (LLM) capabilities on research-level mathematics. Existing benchmarks largely rely on static, hand-curated sets of contest or textbook-style problems as proxies for mathematical research. Instead, we establish an updatable benchmark evaluating models directly on the latest research results in mathematics. This consists of an automatic pipeline that extracts lemmas from arXiv and rewrites them into self-contained statements by making all assumptions and required definitions explicit. It results in a benchmark that can be updated regularly with new problems taken directly from human mathematical research, while previous instances can be used for training without compromising future evaluations. We benchmark current state-of-the-art LLMs, which obtain around 10-15$\%$ accuracy in theorem proving (pass@1) depending on the model, showing that there is currently a large margin of progression for LLMs to reach human-level proving capabilities in a research context.