摘要
大型语言模型（LLMs）在数学问题解决方面越来越强大，甚至能够协助进行研究级别的证明。然而，我们仍然缺乏一种可扩展且可重复的方法来测量跨多种来源的长证明中的逐步推理。这一评估缺口限制了可信赖的AI在证明认证科学进展中的辅助作用。现有评估通常强调最终答案，或依赖昂贵的专家评分，而端到端的证明生成则开放且难以自动验证。
我们提出了Mask-Proof，一个将真实证明转化为可自动检查的掩码步骤任务的管道。该管道掩盖关键公式步骤，提供必要的上下文，并使用基于LLM的等价判断器通过重复投票来评估模型重构的稳定性。最终生成的Mask-ProofBench包含292个来自不同研究领域的整理问题。
对17个模型的实验表明，增强推理能力的模型比标准模型的表现提高了12%至27%。我们的评估器与专家注释者的协议达到了96.8%，使逐步数学推理的测量变得真实、可重复且可比较。基准、注释和代码可在 GitHub 上获取。
博主点评： Mask-Proof的提出不仅填补了数学证明评估中的空白，还为LLM在科学研究中的应用提供了新的思路。通过引入可检查的掩码步骤任务，提升了数学推理的可信度，未来可能会对科学验证和教育产生深远影响。