Mask-Proof：基于大模型的数学证明自动化数据策展流水线

背景

尽管大型语言模型（LLMs）在数学问题解决方面的能力日益增强，甚至能够辅助进行科研级别的证明工作，但我们目前仍缺乏一种可扩展且可复现的方法，来衡量来自不同来源的长证明中的“逐步推理”（step-level reasoning）能力。这一评估缺口限制了可信 AI 在通过证明认证的科学研究进展中的辅助作用。

现有的评估方法往往侧重于最终答案，或者依赖成本高昂的专家评分。与此同时，端到端的证明生成仍然是一个开放性问题，难以通过自动化手段进行验证。为了填补这一空白，研究人员引入了 Mask-Proof，这是一种将真实数学证明转化为可自动检查的“掩码步骤”任务的流水线。

核心内容

本文提出了一种名为 Mask-Proof 的自动化数据策展流水线，旨在解决数学证明评估中的可扩展性和可复现性难题。该系统的核心逻辑是将复杂的数学证明转化为一种特定的评估任务格式，具体流程如下：

1. 掩码步骤生成：流水线从真实的数学证明中提取关键公式步骤，并将其“掩码”（即隐藏或遮盖）。
2. 上下文提供：为模型提供必要的周围上下文信息，确保模型能够基于已知条件进行推理。
3. LLM 等价性评判：利用基于大语言模型的等价性评判器（equivalence judge）来评估模型对掩码步骤的重构能力。为了提高评估的稳定性，该评判器采用重复投票（repeated votes）机制。

基于此流水线，研究团队构建了 Mask-ProofBench 基准测试集。该数据集包含经过精心策展的 292 个数学问题，涵盖了多样化的研究领域。

在对 17 个不同模型进行的实验中，结果显示：

• 经过推理增强的模型（reasoning-enhanced models）在性能上优于标准模型，提升幅度在 12% 到 27% 之间。
• 该评估器与专家标注者的一致性达到了 96.8%。

这一成果使得对数学推理的逐步测量变得忠实、可复现且可比较。基准测试数据、标注文件及代码已公开。

关键要点

• 解决评估痛点：现有评估多关注最终答案或依赖昂贵的人工专家评分，难以自动化验证端到端的证明生成。Mask-Proof 提供了一种自动化的、基于步骤的评估方案。
• 方法论创新：通过“掩码关键步骤 + 提供上下文 + LLM 等价性评判 + 重复投票”的组合策略，实现了对数学证明逐步推理能力的自动化、稳定评估。
• 数据集规模与多样性：构建了包含 292 个问题的 Mask-ProofBench 基准，覆盖多个研究领域，确保了评估的广泛适用性。
• 显著的性能差异：实验证实，推理增强型模型在数学证明任务上显著优于标准模型（提升 12%-27%），凸显了推理能力在复杂数学任务中的重要性。
• 高可信度评估：自动化评估器与人类专家的一致性高达 96.8%，证明了该方法在衡量数学推理能力时的可靠性和有效性。
• 开源贡献：研究团队公开了基准测试、标注数据和代码，促进了社区在数学 AI 评估领域的进一步研究。

意义与影响

Mask-Proof 的提出标志着数学 AI 评估领域的一个重要进展。它不仅仅是一个新的基准测试，更代表了一种从“结果导向”向“过程导向”评估范式的转变。

1. 推动可信 AI 在科学中的应用：通过提供可复现、可扩展的逐步推理评估工具，Mask-Proof 有助于建立更可信的 AI 辅助科研系统，特别是在需要严格逻辑验证的数学和科学领域。
2. 降低评估成本，提高可扩展性：摆脱对昂贵专家评分的依赖，使得大规模、高频次的模型能力评估成为可能，加速了数学 AI 模型的迭代和优化。
3. 促进推理增强模型的发展：实验结果明确指出了推理增强策略的有效性，为后续模型架构设计和训练策略提供了实证依据，引导研究者更加关注模型的中间推理过程而非仅关注最终输出。
4. 标准化数学推理评估：Mask-ProofBench 及其评估方法为社区提供了一个标准化的参考框架，有助于不同研究团队之间进行公平、可比较的性能对比，推动整个领域的健康发展。

总之，Mask-Proof 为解决长证明中的逐步推理评估难题提供了切实可行的技术方案，为构建更强大、更可信的数学 AI 助手奠定了重要基础。