LemmaBench:一个评估LLM数学能力的动态研究级基准

摘要

我们提出一种评估大语言模型（LLM）研究级数学能力的新基准方法。现有基准大多依赖静态、人工精选的竞赛或教科书式问题集来代理数学研究。相反，我们建立一个可更新的基准，直接用最新的数学研究成果评估模型。它包含一个自动流水线，从arXiv提取引理，并通过显式化所有假设与所需定义把引理改写为自包含的命题。由此得到的基准可以定期用直接取自人类数学研究的新问题更新，同时既往实例可用于训练而不损害未来评估。我们对当前最先进的LLM进行了基准测试，其定理证明（pass@1）准确率依模型而定约为10-15%，表明LLM要达到研究情境中人类水平的证明能力，目前仍有很大的进步空间。

LemmaBench:一个评估LLM数学能力的动态研究级基准 — 图1：流水线一览：该流水线从 arXiv 检索论文，抽取陈述并使其自包含。随后，外部证明器（prover）可以尝试逐步证明这些陈述，每个证明由评判者（judge）检查。最终分数是有效证明所占的比例。我们使用 GPT-5、Gemini 2.5 pro、Gemini 3 pro、Claude 4.5 Opus 与 Deepseek-R 作为证明器的基线。