Mask-Proof: 一种基于LLM的数学证明自动化数据梳理流水线

# Mask-Proof：基于大语言模型的数学证明自动数据整理流水线

**来源：** https://arxiv.org/html/2606.15258

张洁睿 [email protected] ([mailto:[email protected]](https://arxiv.org/html/2606.15258v1/mailto:[email protected]))
北京邮电大学计算机学院 北京 中国

谭思远 cream˙[email protected] ([mailto:cream%CB%[email protected]](https://arxiv.org/html/2606.15258v1/mailto:cream%CB%[email protected]))
北京邮电大学研究生院 北京 中国

李新航 [email protected] ([mailto:[email protected]](https://arxiv.org/html/2606.15258v1/mailto:[email protected]))
复旦大学数学科学学院 上海 中国

林龙壮志 [email protected] ([mailto:[email protected]](https://arxiv.org/html/2606.15258v1/mailto:[email protected]))
北京邮电大学网络空间安全学院 北京 中国

李大林家 [email protected] ([mailto:[email protected]](https://arxiv.org/html/2606.15258v1/mailto:[email protected]))
大连理工大学计算机科学与技术学院 大连 中国

顾成峰 [email protected] ([mailto:[email protected]](https://arxiv.org/html/2606.15258v1/mailto:[email protected]))
浙江大学竺可桢学院 杭州 中国

李新平 [email protected] ([mailto:[email protected]](https://arxiv.org/html/2606.15258v1/mailto:[email protected]))
清华大学心理与认知科学系 北京 中国

郝雅娴 [email protected] ([mailto:[email protected]](https://arxiv.org/html/2606.15258v1/mailto:[email protected]))
北京邮电大学研究生院 北京 中国

梁圣佳 [email protected] ([mailto:[email protected]](https://arxiv.org/html/2606.15258v1/mailto:[email protected]))
北京航空航天大学虚拟现实技术与系统国家重点实验室 北京 中国

任宇翔 [email protected] ([mailto:[email protected]](https://arxiv.org/html/2606.15258v1/mailto:[email protected]))
南京大学智能科学与技术学院 南京 中国

刘文浩 [email protected] ([mailto:[email protected]](https://arxiv.org/html/2606.15258v1/mailto:[email protected]))
北京邮电大学计算机学院 北京 中国

(2026)

###### 摘要。

大语言模型（LLMs）在数学问题解决方面能力日益增强，甚至能辅助研究级别的证明，但我们仍然缺乏一种可扩展且可重复的方法来衡量跨不同来源的长证明中的步骤级推理。这一评估差距限制了可证明科学进步中值得信赖的AI辅助。现有的评估通常强调最终答案或依赖昂贵的人工评分，而端到端的证明生成仍然是开放式的，且难以自动验证。我们介绍**Mask-Proof**，一个将真实证明转化为可自动检查的**遮蔽步骤**任务的流水线。它遮蔽关键的公式步骤，提供必要的上下文，并使用基于LLM的等价性判断器（通过重复投票确保稳定性）评估模型的重建结果。由此产生的**Mask-ProofBench**包含292个涵盖不同研究领域的精选问题。在17个模型上的实验表明，推理增强型模型比标准模型表现高出12%至27%。我们的评估器与人工专家注释者的一致性达到96.8%，实现了对步骤级数学推理的忠实、可重复和可比较的衡量。基准测试、注释和代码可在 https://github.com/weating/Mask-Proof 获取。

数学推理，大语言模型，基准测试，证明评估，自动整理

††期刊年份：2026
††版权：cc
††会议：第32届ACM SIGKDD知识发现与数据挖掘会议V.2；2026年8月9日至13日；韩国济州岛
††会议录：第32届ACM SIGKDD知识发现与数据挖掘会议V.2会议录 (KDD '26)，2026年8月9日至13日，韩国济州岛
††DOI：10.1145/3770855.3818886
††ISBN：979-8-4007-2259-2/2026/08
††CCS：计算方法论 人工智能
††CCS：计算方法论 自然语言处理

## 1. 引言

大语言模型（LLMs）在数学问题解决方面日益胜任[balunović2026matharenaevaluatingllmsuncontaminated]，甚至可以协助研究级别的证明[Wei et al., 2022 (https://arxiv.org/html/2606.15258#bib.bib2); Trinh et al., 2024 (https://arxiv.org/html/2606.15258#bib.bib3)]。然而，我们仍然缺乏一种可扩展且可重复的测量工具来评估长证明中的步骤级推理——一种能够忠实于底层数学，并适用于研究论文和竞赛基准等异构来源的工具[Ma et al., 2025 (https://arxiv.org/html/2606.15258#bib.bib35); Zheng et al., 2025 (https://arxiv.org/html/2606.15258#bib.bib29); Pandit et al., 2025 (https://arxiv.org/html/2606.15258#bib.bib7)]。这一差距在最近的前沿系统调查中愈发明显。例如，OpenAI的Sébastien Bubeck及其合作者报告称，GPT-5在专家引导下有时能在研究级别的证明任务上取得有意义的进展[Bubeck et al., 2025 (https://arxiv.org/html/2606.15258#bib.bib1)]。然而，此类证据往往依赖于逐步的专家判断，这种判断成本高昂、难以复现且难以跨领域比较。

##### 为何这对“AI for Sciences”至关重要。

这个测量差距不仅仅是基准测试的麻烦。数学是一门基础性科学学科，其进展是通过证明来认证的。因此，数学中值得信赖的AI辅助需要对推理过程进行基于领域的评估，而不仅仅是最终结果[Chen et al., 2022 (https://arxiv.org/html/2606.15258#bib.bib34); Ma et al., 2025 (https://arxiv.org/html/2606.15258#bib.bib35); Yang et al., 2025 (https://arxiv.org/html/2606.15258#bib.bib36)]。Mask-Proof提供了以证明为中心的数据和评估工具，使得在真实世界证明源中的步骤级推理变得可衡量、可复现和可比较。

##### 步骤级证明评估中的测量问题。

将步骤级评估视为科学测量，揭示了三个相互交织的障碍：测量什么、需要什么上下文以及如何评分的正确性。
(1) **步骤选择并非易事。** 证明在风格和粒度上差异很大。许多步骤是平凡的、纯定义性的或由局部表面线索主导。遮蔽此类步骤可能衡量的是捷径利用而非真正的推理，从而损害了构念效度[Geirhos et al., 2020 (https://arxiv.org/html/2606.15258#bib.bib5); Zhu et al., 2024 (https://arxiv.org/html/2606.15258#bib.bib37); Yu et al., 2023 (https://arxiv.org/html/2606.15258#bib.bib38)]。
(2) **依赖关系常常缺失。** 研究论文中的证明经常依赖外部依赖——交叉引用的引理、宏或未说明的背景事实。如果这些依赖关系未被恢复，遮蔽的步骤可能因提供的上下文不足而欠定，从而混淆推理能力与信息缺失，使得失败无法解释。
(3) **可扩展的检查很困难。** 即使有了ground-truth步骤，大规模的正确性检查仍然困难：字符串匹配不够充分，符号工具无法提供通用保证，且专家评估无法扩展。因此，自动评判需要显式机制来控制方差并确保可重复性[Kim et al., 2024 (https://arxiv.org/html/2606.15258#bib.bib39); Thakur et al., 2025 (https://arxiv.org/html/2606.15258#bib.bib40); Ke et al., 2024 (https://arxiv.org/html/2606.15258#bib.bib41); Zheng et al., 2023 (https://arxiv.org/html/2606.15258#bib.bib8)]。
综合来看，这些挑战阻碍了数学中的步骤级推理作为一个可复现的科学现象进行研究。

##### Mask-Proof：使步骤级推理变得可衡量。

我们介绍**Mask-Proof**，一个直接解决上述障碍的流水线，它将异构证明转化为可验证、自包含、步骤级的评估问题，并带有方差受控的自动检查。核心思想有意保持简单：我们不是对整个证明进行端到端评分，而是测试模型能否重建一个关键的公式步骤，其ground truth直接从原始证明中提取。具体来说，Mask-Proof (i) 使用Codex CLI以代理方式选择无法仅通过局部线索解决的关键步骤，(ii) 恢复使每个遮蔽步骤自包含所需的最小依赖闭包，这意味着除了提供的上下文外，不再需要外部引理、定义或宏，以及 (iii) 使用经过校准的基于LLM的等价性判断器检查模型输出，并通过重复独立判断和多数投票来减少方差。除了基准测试之外，Mask-Proof还可作为一个可复用的测量框架，在证明源之间展现出有效性、可复现性和泛化能力。图1 (https://arxiv.org/html/2606.15258#S1.F1) 展示了最终遮蔽步骤格式的示例。在这项工作中，我们做出了三项贡献：
1. (1) **Mask-Proof**，一个基于LLM的自动整理流水线，用于识别关键推理的公式步骤，重建自包含的证明上下文，并从真实世界的数学证明中生成可验证的遮蔽步骤问题。
2. (2) **Mask-ProofJudge**，一个自动的步骤级评估框架，经过专家判断的校准，通过重复独立判断和投票实现了96.8%的人机判断一致性，并减少了方差。
3. (3) **Mask-ProofBench**，由该流水线生成的基准测试，能够对真实世界研究级别的数学证明中的步骤级推理进行可扩展且可靠的评估。该基准测试包含292个Mask-Proof问题，所有问题均由数学领域的人类专家进行了人工审计。

参照图注

图1. (I) IMO-ProofBench [Luong et al., 2025 (https://arxiv.org/html/2606.15258#bib.bib19)] 代表竞赛级别的证明问题，附带完整解答和评分标准的评估方式。(II) 经过Mask-Proof处理，相同的证明数据被转换为可验证的遮蔽格式，其中关键的公式/推导步骤被隐藏，作为自动评估的目标。(III) Mask-ProofBench将此可验证的遮蔽格式扩展到研究级别的证明，这些证明具有更长的推导过程，遮蔽的是严格的中级步骤，而非最终数值结果或高度模板化的片段。详见附录E (https://arxiv.org/html/2606.15258#A5)。

证明评估格式的三面板比较
面板I展示了一个IMO-ProofBench竞赛问题（USAMO 2025），包含涉及二项式系数恒等式的完整解法和部分评分标准。面板II展示了经过Mask-Proof处理后的相同证明，其中一个关键的同余公式被替换为MASK标记，同时保留了周围的证明上下文。面板III展示了一个基于Shankar等人引理2.4的研究级遮蔽证明，涉及特征不为2的域上的SL3轨道分类，包括定义2.3的额外自包含信息、一个被遮蔽的矩阵构造步骤，以及DeepSeek-V3.2-Thinking给出的示例LLM响应（其错误地反转了(2，2)项的正负号）。

## 2. 相关工作

##### 基于答案的数学推理基准测试。

LLM数学推理的评估历史上集中于具有唯一可验证终点的基准测试。GSM8K [Cobbe et al., 2021 (https://arxiv.org/html/2606.15258#bib.bib4)] 和 MATH [Hendrycks et al., 2021 (https://arxiv.org/html/2606.15258#bib.bib13)] 确立了最终答案准确率作为主导指标，实现了可扩展的评估，但对推理过程的可见性有限。随着在这些基准测试上的性能趋于饱和，后续工作通过引入奥林匹克级别问题 [He et al., 2024 (https://arxiv.org/html/2606.15258#bib.bib25); Gao et al., 2025 (https://arxiv.org/html/2606.15258#bib.bib14)]、专家编写的前沿评估 [Glazer et al., 2024 (https://arxiv.org/html/2606.15258#bib.bib30)] 和研究级别问答 [Zhang et al., 2025 (https://arxiv.org/html/2606.15258#bib.bib21)] 来提高难度。然而，即使是基于答案的复杂基准也从根本上评估的是*结论*而非*公式*，这使得证明质量未经检验。

##### 以证明为中心的评估与形式化定理证明。

以证明为中心的评估将焦点从答案正确性转移到公式严谨性，使可验证性成为核心挑战。形式化定理证明通过将正确性验证委托给证明助手内核来解决此问题：miniF2F [Zheng et al., 2022 (https://arxiv.org/html/2606.15258#bib.bib24)] 和 PutnamBench [Tsoukalas et al., 2024 (https://arxiv.org/html/2606.15258#bib.bib26)] 是竞赛数学形式化证明的基准测试。然而，自然语言到形式语言的差距引入了难以消除的语义错误；ReForm [Chen et al., 2026 (https://arxiv.org/html/2606.15258#bib.bib20)] 揭示了自动化形式化本身充满挑战，即使是人类专家在38.5%的案例中也会产生语义错误。自然语言证明评估更接近实际的数学实践，但大规模评分要困难得多。IMO-ProofBench [Luong et al., 2025 (https://arxiv.org/html/2606.15258#bib.bib19)] 引入了基于评分标准的竞赛证明评分方法，而 STORM-BORN [Liu et al., 2025 (https://arxiv.org/html/2606.15258#bib.bib12)] 则从研究论文中挑选具有挑战性的公式，并采用人机协同验证。最近，IMProofBench [Schmitt et al., 2025 (https://arxiv.org/html/2606.15258#bib.bib33)] 针对*研究级别*的证明生成，使用专家编写的问题，并结合了对完整证明的专家评分和可评分的后续子问题。然而，这些评估仍然需要大量的人类专家注释，并且无法扩展到评估“野外”研究级别的证明。

##### 验证器与可扩展检查。

为了减少对专家评分的依赖，一个重要的研究方向是训练验证器来为推理过程打分。过程奖励模型 [Lightman et al., 2024 (https://arxiv.org/html/2606.15258#bib.bib23); Luo et al., 2024 (https://arxiv.org/html/2606.15258#bib.bib28)] 提供步骤级反馈，而诊断研究则揭示LLM难以定位推理错误，但可以在给定错误位置时纠正它们 [Tye et al., 2024 (https://arxiv.org/html/2606.15258#bib.bib18)]。自我纠正方法取得的成功有限：Huang等人 [Huang et al., 2024 (https://arxiv.org/html/2606.15258#bib.bib31)] 证明LLM无法在没有外部反馈的情况下可靠地自我纠正推理。更近期的生成器-验证器框架，如DeepSeekMath-V2 [Shao et al., 2025 (https://arxiv.org/html/2606.15258#bib.bib11)]，通过元验证和自训练扩展了验证能力，尽管其评估仍以竞赛风格问题为中心。高调展示的AI辅助数学 [Bubeck et al., 2025 (https://arxiv.org/html/2606.15258#bib.bib1)] 仍然强调专家监督而非完全自动评估。总的来说，先前的工作突显了持续存在的能力-可验证性张力：随着评估接近研究级别的证明，获得低成本、可扩展和可重复的验证变得显著更加困难。

参照图注

图2. Mask-Proof流水线。
从原始的arXiv LaTeX源码开始，我们的流水线提取完整的证明，将其修复为自包含的上下文，并通过代理方式遮蔽一个关键公式步骤，以生成Mask-ProofBench。

Mask-Proof流水线概览图
该流水线包含三个阶段。阶段一，论文收集：下载并过滤包含LaTeX源码的arXiv论文