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.


翻译:大型语言模型在数学问题求解方面能力日益增强,甚至能辅助研究级证明,但我们仍缺乏一种可扩展且可复现的方法,来衡量来自不同来源的长篇证明中的逐步推理能力。这一评估差距限制了在经证明认证的科学进展中实现可信赖的人工智能辅助。现有评估常侧重于最终答案或依赖昂贵的专家评分,而端到端的证明生成仍具有开放性且难以自动验证。我们提出Mask-Proof,一种将真实证明转化为可自动检查的掩码步骤任务的流水线。它掩码关键公式步骤,提供必要的上下文,并利用基于大语言模型的等效性评判器通过重复投票进行稳定性评估,从而重构模型。由此生成的Mask-ProofBench包含来自不同研究领域的292个精选问题。对17个模型的实验表明,增强推理能力的模型在性能上比标准模型高出12%至27%。我们的评判器与专家标注者的一致性达到96.8%,从而实现了对逐步数学推理进行忠实、可复现且可比较的测量。基准测试、标注及代码可在https://github.com/weating/Mask-Proof获取。

0
下载
关闭预览

相关内容

ACM/IEEE第23届模型驱动工程语言和系统国际会议,是模型驱动软件和系统工程的首要会议系列,由ACM-SIGSOFT和IEEE-TCSE支持组织。自1998年以来,模型涵盖了建模的各个方面,从语言和方法到工具和应用程序。模特的参加者来自不同的背景,包括研究人员、学者、工程师和工业专业人士。MODELS 2019是一个论坛,参与者可以围绕建模和模型驱动的软件和系统交流前沿研究成果和创新实践经验。今年的版本将为建模社区提供进一步推进建模基础的机会,并在网络物理系统、嵌入式系统、社会技术系统、云计算、大数据、机器学习、安全、开源等新兴领域提出建模的创新应用以及可持续性。 官网链接:http://www.modelsconference.org/
大型语言模型(LLM)赋能的知识图谱构建:综述
专知会员服务
56+阅读 · 2025年10月24日
LLM4SR:关于大规模语言模型在科学研究中的应用综述
专知会员服务
42+阅读 · 2025年1月9日
WSDM 2024| LLMs助力图学习?基于大模型的图数据增强
专知会员服务
27+阅读 · 2023年11月19日
论文浅尝 | GMNN: Graph Markov Neural Networks
开放知识图谱
20+阅读 · 2020年2月14日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
论文浅尝 | 基于知识图谱子图匹配以回答自然语言问题
开放知识图谱
26+阅读 · 2018年6月26日
论文浅尝 | 基于知识图谱的子图匹配回答自然语言问题
开放知识图谱
27+阅读 · 2018年5月17日
概率图模型体系:HMM、MEMM、CRF
机器学习研究会
30+阅读 · 2018年2月10日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
3+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
16+阅读 · 2013年12月31日
国家自然科学基金
18+阅读 · 2012年12月31日
VIP会员
最新内容
《通过小型无人机系统将情报能力“作战化”》
专知会员服务
1+阅读 · 今天7:28
消耗优势:美军的“精确规模化”概念
专知会员服务
7+阅读 · 6月15日
《离线语言支持系统:面向空战战术决策》
专知会员服务
8+阅读 · 6月15日
俄乌战场地面机器人如何改写战争规则
专知会员服务
9+阅读 · 6月14日
相关基金
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
3+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
16+阅读 · 2013年12月31日
国家自然科学基金
18+阅读 · 2012年12月31日
Top
微信扫码咨询专知VIP会员