MathAdv：定理证明器的知识、推理、形式化与泛化

# MathAdv：定理证明器如何理解、推理、形式化与泛化  
来源：https://arxiv.org/html/2608.25449  
Jiaxin Yuan1jyuan98@umd\.eduConnor Martinez Lockhart1connorl@umd\.eduXiaoyu Liu1xiaoyu\.liu1231@gmail\.comJiaqi Wang3jwang3737@gatech\.eduChenghao Deng1dengch16@umd\.eduXiayimei Han1xhan1115@umd\.eduVlasios Mastrantonis4vm429@cornell\.eduDmitrii Gudin1dgudin@umd\.eduShaopeng Zhu2szhu@terpmail\.umd\.eduAbdirisak Abdullahi Mohamed1amoham70@umd\.eduBilal Hamdi Aytekin1baytekin@umd\.eduJiewen Lang2jiewenlang@gmail\.comZezheng Song1zsong2019@gmail\.comFurong Huang1,5furongh@umd\.edu1马里兰大学帕克分校2独立研究员3佐治亚理工学院4康奈尔大学5通用人工智能研究所  

###### 摘要  
形式化定理证明实现了数学推理的可机器验证评估，但现有基准测试常侧重整体证明准确率，局限于狭窄的数学领域，且对等效问题重构的鲁棒性证据有限。我们推出了 MathAdv，一个涵盖本科至研究生数学13个领域的诊断基准测试。除 Lean 4 定理证明任务外，MathAdv 还提供至多三种辅助任务：考察数学知识的选择题、评估非形式化推理的填空题，以及检验问题呈现鲁棒性的人工设计变换。对当前定理证明器的评估得出四个结论：形式化仍是主要瓶颈；性能在不同数学领域差异显著；自然语言指导对通用大语言模型有帮助，但可能阻碍证明专用模型；数学等效重构暴露了显著的鲁棒性局限。这些结果表明，分模块评估能揭示被整体定理证明准确率所掩盖的模型能力与失效模式。数据集与评估脚本已发布于 https://github.com/margotyjx/MathAdv.git。  

图 1：MathAdv 概览。  

## 1 引言  
数学推理是评估人工智能的核心基准，因为它要求超越记忆与表层模式匹配的抽象理解、逻辑推导与多步推理能力（Hendrycks 等，2021）(https://arxiv.org/html/2608.25449#bib.bib53)；（Mirzadeh 等，2025）(https://arxiv.org/html/2608.25449#bib.bib63)。数学推理在科学发现及其他需要可靠、可验证结论的领域也至关重要，使其严格评估日益重要（Lewkowycz 等，2022）(https://arxiv.org/html/2608.25449#bib.bib62)；（Ríos‑García 等，2026）(https://arxiv.org/html/2608.25449#bib.bib65)。  

早期基准测试主要通过最终答案评估非形式化自然语言解答，对中间推理的有效性保障有限（Lewkowycz 等，2022）(https://arxiv.org/html/2608.25449#bib.bib62)；（Luo 等，2025）(https://arxiv.org/html/2608.25449#bib.bib68)。形式化定理证明提供了更严谨的替代方案：模型在 Lean（Moura 与 Ullrich，2021）(https://arxiv.org/html/2608.25449#bib.bib55)、Coq（Bertot 与 Castéran，2004）(https://arxiv.org/html/2608.25449#bib.bib57) 和 Isabelle（Nipkow 等，2002）(https://arxiv.org/html/2608.25449#bib.bib58) 等证明助手中构建可机器验证的证明，实现自动验证并为无效证明提供精确反馈（Li 等，2024）(https://arxiv.org/html/2608.25449#bib.bib67)；（Hubert 等，2026）(https://arxiv.org/html/2608.25449#bib.bib64)。语言模型的最新进展进一步强化了证明生成系统，并加深了对形式化推理的兴趣（Lin 等，2025b）(https://arxiv.org/html/2608.25449#bib.bib49)；（Ren 等，2025）(https://arxiv.org/html/2608.25449#bib.bib69)。  

尽管近期取得进展，现有形式化数学基准测试仅部分反映了现代模型的能力。三个局限尤为重要：  

首先，现有基准测试诊断分辨率有限。成功的定理证明需要数学背景知识、逻辑推导和形式化证明构建，但基准测试通常仅报告整体证明准确率。因此难以确定失败源于知识缺口、推理错误，还是将有效论证转化为形式化证明的困难。  

其次，现有基准测试覆盖的数学领域狭窄。它们主要聚焦于来自高中和本科数学的竞赛级问题，侧重代数与数论（Liu 等，2023）(https://arxiv.org/html/2608.25449#bib.bib54)；（Tsoukalas 等，2024）(https://arxiv.org/html/2608.25449#bib.bib56)。因此，模型在更广泛的高级数学领域的能力仍不明确。  

第三，现有评估对鲁棒性与泛化的证据有限。它们通常评估模型对每个问题的单一固定表述，而语言模型推理可能对问题表述的微小变化敏感（Mirzadeh 等，2025）(https://arxiv.org/html/2608.25449#bib.bib63)。同时，模型规模增大加剧了对数据污染与记忆化的担忧（Gardner 等，2020）(https://arxiv.org/html/2608.25449#bib.bib59)；（Kaushik 等，2020）(https://arxiv.org/html/2608.25449#bib.bib60)；（Sakaguchi 等，2021）(https://arxiv.org/html/2608.25449#bib.bib61)。这些问题共同使得判断成功证明是源于稳健的数学推理，还是对熟悉表述与表面线索的依赖变得日益重要。  

为此，我们推出 MathAdv，一个旨在直接解决上述三个局限的形式化数学诊断基准。  

首先，MathAdv 提供更高的诊断分辨率。原始定理证明任务评估形式化证明构建；选择题考察数学背景知识；填空题评估非形式化推理。这种分模块评估有助于区分知识缺口、推理错误与形式化困难。  

其次，MathAdv 拓宽了评估的数学范围。它包含 321 个问题，涵盖 13 个本科至研究生领域，包括现有定理证明基准中较少涉及的拓扑学、傅里叶分析与泛函分析等领域。其中 298 个问题已形式化为 Lean 4 语句（Moura 与 Ullrich，2021）(https://arxiv.org/html/2608.25449#bib.bib55)；其余 23 个保留用于辅助评估，并因所需 Mathlib 支持不足而推迟形式化。  

第三，MathAdv 明确评估问题重构的鲁棒性。人工设计的变换变体在保留底层数学内容的同时显著改变问题呈现方式，揭示模型成功是否超越原始表述。  

总体而言，每个问题附带至多三种辅助评估，使 MathAdv 能够在统一框架内评估数学知识、非形式化推理、形式化证明构建与鲁棒性。  

构建 MathAdv 带来两大技术挑战：设计能分离不同能力同时保留底层数学的诊断任务，以及生成类型正确且语义忠实的 Lean 语句，尽管 Mathlib 覆盖不均。  

我们通过领域专家策划与独立审查解决第一个挑战：专家选择非冗余问题，构建辅助任务，并验证变换变体保留了原始问题所需的推理。  

我们通过大语言模型辅助、验证器在环的形式化流程解决第二个挑战：大语言模型起草每个 Lean 语句，编译器反馈指导迭代修正，独立的大语言模型和领域专家检查语义保真度，第二位专家进行最终审查。对于 Mathlib 支持不足的概念，专家评估可行编码，并在忠实翻译需要过高库开发成本时推迟形式化。  

利用此诊断框架，我们系统评估了当前定理证明器，得出四个关键发现：  

首先，形式化仍是主要瓶颈。模型常能识别有希望的证明方向，但无法将其转化为有效的 Lean 证明。  

其次，数学推理能力在各领域迁移不均。性能随学科显著变化，揭示了高级数学能力的不均衡。  

第三，自然语言指导并非普遍有益。推理提示提升了通用大语言模型的性能，但可能降低证明专用定理证明器的性能，表明不同模型家族对非形式化指导的利用方式不同。  

最后，当前定理证明器对等效重构敏感。大多数模型解决原始问题的概率远高于其人工变换版本，表明依赖特定呈现模式而非稳健的数学理解。  

我们的贡献如下：  
1. 1\. 一个广泛、经专家审查的高级形式化数学基准。我们推出 MathAdv，包含 321 个问题，涵盖 13 个本科至研究生领域，包括拓扑学、傅里叶分析与泛函分析等代表性不足的领域。其中 298 个问题通过大语言模型辅助、验证器在环的流程构建 Lean 4 语句，并经独立专家审查以确保可编译性与语义保真度。  
2. 2\. 一个分模块的定理证明诊断框架。除整体证明准确率外，MathAdv 评估四种能力：数学知识、非形式化推理、形式化证明构建与重构鲁棒性。原始 Lean 任务附带至多三种辅助评估——选择题、填空题与人工变换变体——以帮助识别模型成功与失败的原因。  
3. 3\. 对当前定理证明器的系统性刻画。我们的评估表明，形式化仍是主要瓶颈；性能在不同数学领域差异显著；自然语言指导的有效性取决于模型专长；对数学等效重构的鲁棒性仍有限。  

## 2 相关工作  
形式化数学推理。形式化数学在证明助手（如 Lean）实现的逻辑系统中编码语句与证明（Moura 与 Ullrich，2021）(https://arxiv.org/html/2608.25449#bib.bib55)。数学对象与定义必须从系统识别的概念构建，且每一步推导必须遵循其逻辑规则。因此证明助手可验证每一步并确保结论从陈述假设中推导。对模型而言，这要求将数学思想转化为精确的定义、语句与逻辑有效的证明步骤。  

现有基准数据集。近期基准测试评估了大语言模型在竞赛数学、非形式到形式的转换、大型形式化定理集合、符号推理与图表几何中的形式化数学推理（Zheng 等，2021）(https://arxiv.org/html/2608.25449#bib.bib1)；（Azerbayev 等，2023a）(https://arxiv.org/html/2608.25449#bib.bib2)；（Liu 等，2023）(https://arxiv.org/html/2608.25449#bib.bib54)；（Tsoukalas 等，2024）(https://arxiv.org/html/2608.25449#bib.bib56)；（Yu 等，2025）(https://arxiv.org/html/2608.25449#bib.bib4)；（Liu 等，2026）(https://arxiv.org/html/2608.25449#bib.bib3)；（Biyani 等，2025）(https://arxiv.org/html/2608.25449#bib.bib5)。但每个基准主要关注特定问题来源、领域或能力；附录 A.1 (https://arxiv.org/html/2608.25449#A1.SS1) 提供了详细回顾。相比之下，MathAdv 覆盖本科至研究生数学的 13 个领域，并包含填空题、选择题与变换题，能够进行超越定理证明准确率的深入分析。  

形式化数学模型。近期研究为非形式数学推理与形式化定理证明开发了广泛的大语言模型方法。形式化定理证明器从直接证明生成器到使用搜索、验证器反馈、大型形式化训练语料或多推理代理的系统（Polu 与 Sutskever，2020）(https://arxiv.org/html/2608.25449#bib.bib11)；（Azerbayev 等，2023b）(https://arxiv.org/html/2608.25449#bib.bib8)；（Ying 等，2024）(https://arxiv.org/html/2608.25449#bib.bib44)；（Lin 等，2024）(https://arxiv.org/html/2608.25449#bib.bib7)；（Shen 等，2025）(https://arxiv.org/html/2608.25449#bib.bib9)；（Lin 等，2025a）(https://arxiv.org/html/2608.25449#bib.bib46)；（Xin 等，2024）(https://arxiv.org/html/2608.25449#bib.bib47)；（Wang 等，2024）(https://arxiv.org/html/2608.25449#bib.bib10)；（Gao 等，2024）(https://arxiv.org/html/2608.25449#bib.bib6)；（Wang 等，2025）(https://arxiv.org/html/2608.25449#bib.bib48)。这些方法主要在生成候选证明和错误恢复方面有所不同；附录 A.2 (https://arxiv.org/html/2608.25449#A1.SS2) 提供了详细回顾。  

## 3 MathAdv：形式化数学推理的高级基准  
3.1 节 (https://arxiv.org/html/2608.25449#S3.SS1) 介绍 MathAdv 并描述三种互补的诊断题型，测试自然语言问题求解、相关定理与证明策略知识，以及对等效重构的鲁棒性。这些诊断任务使我们能够将组件能力从形式化证明构建中分离，后者需要将它们结合以在 Lean 中生成精确、可验证的证明。  

3.2 节 (https://arxiv.org/html/2608.25449#S3.SS2) 介绍用于将问题转化为 Lean 4 的人在回路流程。  

### 3.1 MathAdv  
MathAdv 包含 321 个问题，源自本科至研究生数学教科书或由领域专家贡献。问题涵盖 13 个领域——数论、线性代数、抽象代数、微积分、实分析、复分析、傅里叶分析、泛函分析、概率论、拓扑学、几何学、组合学与逻辑——选择时最大化覆盖并最小化冗余。我们形式化了其中 298 个问题为 Lean 4；其余 23 个保留用于辅助评估，并因当前 Mathlib 缺陷推迟形式化。  

对于每个合适问题，我们构建至多三种辅助任务：填空题、选择题与人工变换题。图 2 (https://arxiv.org/html/2608.25449#S3.F2) 展示了领域分布及诊断任务示例。  

直接回答问题。我们将合适的证明问题重构为直接回答问题，要求模型计算目标量或表达式而不编写 Lean 证明。这些问题测试模型能否用自然语言解决底层数学，从而帮助区分非形式问题求解与形式化证明构建。其领域分布如图 8 (https://arxiv.org/html/2608.25449#A2.F8) 所示。  

选择题。我们要求模型从多个合理选项中识别与原始问题最相关的定理、概念或推理策略。这些问题考察模型是否具备解决问题所需的背景知识。