用大模型自动构建可验证的数学证明步骤评测集
Mask-Proof: An LLM-based Automated Data Curation Pipeline on Mathematical Proofs
- 将真实证明转为带掩码的步骤任务，通过大模型投票判断还原正确性
- 17个模型测试显示增强推理模型性能提升12%至27%，与专家一致率达96.8%
- 适合评估数学推理能力或构建可复现评测基准的研究者使用
大语言模型在数学问题求解上日益成熟，甚至能协助研究级证明，但缺乏跨来源、可扩展且可复现的长证明步骤级推理评估方法。现有评测多关注最终答案或依赖昂贵的人工评分，而端到端生成难以自动验证。我们提出Mask-Proof，一个将真实证明转化为可自动校验的掩码步骤任务的流水线。该方法掩码关键公式步骤，保留必要上下文，利用基于大模型的等价性判别器通过多次投票确保稳定性。构建的Mask-ProofBench包含292个来自不同研究领域的题目。17个模型实验表明，增强推理模型性能比标准模型高出12%至27%。评估器与专家标注者达成96.8%的一致率，实现了对步骤级数学推理的忠实、可复现、可比较测量。基准数据、标注与代码已开源。
原文摘要 · Abstract (English)
Large language models (LLMs) are increasingly capable of mathematical problem solving and can even assist with research-level proofs, yet we still lack a scalable and reproducible way to measure step-level reasoning in long proofs across diverse sources. This evaluation gap limits trustworthy AI assistance in proof-certified scientific progress. Existing evaluations often emphasize final answers or rely on costly expert grading, while end-to-end proof generation remains open-ended and hard to verify automatically. We introduce Mask-Proof, a pipeline that turns real proofs into automatically checkable masked-step tasks. It masks key formula steps, provides the necessary surrounding context, and evaluates model reconstructions with an LLM-based equivalence judge using repeated votes for stability. The resulting Mask-ProofBench contains 292 curated problems across diverse research areas. Experiments with 17 models show that reasoning-enhanced models outperform standard models by 12% to 27%. Our evaluator achieves 96.8% agreement with expert annotators, enabling faithful, reproducible, and comparable measurement of step-level mathematical reasoning. Benchmark, annotations, and code are available at https://github.com/weating/Mask-Proof.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。