构建首个大规模人工评估的数学证明数据集，助力LLM证明能力研究
The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs
- 收集5000+条LLM生成的数学证明并经人工评估
- 发现自然语言证明准确率远高于形式化证明
- 适合研究数学推理与大模型验证的学者使用
近期大型语言模型（LLMs）在数学证明生成方面取得显著进展，但进一步发展受限于缺乏大规模、高质量的人工评估证明数据集。尽管创建成本高昂，此类数据集对训练优化和严谨分析证明生成能力至关重要。本文提出开放证明语料库（OPC），包含超过5000条由先进LLMs生成并经人工评估的证明。该数据集专为广泛适用性和下游研究设计，是首个包含大量来自美国数学奥林匹克（USAMO）和国际数学奥林匹克（IMO）等顶级竞赛问题的正确LLM生成解法的数据集。基于OPC，我们探讨了自动证明生成中的关键问题：（1）自然语言与形式化证明生成间的性能差距；（2）最终答案正确性与完整证明有效性之间的差异；（3）best-of-n选择对证明质量的影响。最后，为展示其价值，我们在该数据集上微调一个80亿参数模型，使其在证明正确性评估任务上达到与Gemini-2.5-Pro最佳模型相当的性能。
原文摘要 · Abstract (English)
In recent months, large language models (LLMs) have made significant progress in mathematical proof generation, but further advancement is hindered by the lack of a large-scale, high-quality dataset of human-evaluated proofs. While expensive to create, such a dataset is essential for driving improvements in training and enabling a rigorous analysis of proof generation capabilities. In this work, we present the Open Proof Corpus (OPC), a dataset comprising over 5,000 human-evaluated proofs produced by state-of-the-art LLMs. The OPC was specifically designed for broad applicability and downstream usage in proof generation research and is the first to include a substantial number of correct, LLM-generated solutions to problems from prestigious mathematics competitions such as the USAMO and IMO. Using the OPC, we explore critical questions in automated proof generation: (1) the performance gap between natural language and formal proof generation, (2) the discrepancy between final-answer accuracy and full-proof validity, and (3) the impact of best-of-n selection on proof quality. Finally, to showcase the utility of the OPC, we finetune an 8B-parameter model on the dataset, obtaining a model that performs on par with the best model, Gemini-2.5-Pro, on the task of evaluating proof correctness.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。