Open Proof Corpus (OPC)

Open Proof Corpus (OPC) 是一个大规模的、由人类评估的、由 LLM 生成的数学证明数据集，包含超过 5,000 个证明。该数据集旨在用于证明生成研究中的下游应用，并包括来自著名数学竞赛（如 USAMO 和 IMO）的大量正确、由 LLM 生成的解决方案。数据集的创建过程包括从顶级国际数学竞赛中选取问题，使用最先进的 LLM 生成证明，并由人类评估证明的正确性。该数据集旨在解决当前 LLM 在数学证明生成方面的性能差距、最终答案准确性与完整证明有效性之间的差异，以及最佳-of-n 选择对证明质量的影响等问题。

Open Proof Corpus (OPC) is a large-scale, human-evaluated, LLM-generated mathematical proof dataset containing over 5,000 proofs. This dataset is intended for downstream applications in proof generation research, and includes a large number of correct, LLM-generated solutions from prominent international mathematics competitions such as the USAMO and IMO. The dataset's construction process involves selecting problems from top-tier international mathematics competitions, generating proofs using state-of-the-art LLMs, and having human evaluators assess the correctness of these proofs. This dataset aims to address current challenges in LLM-based mathematical proof generation, including the performance gap of LLMs, the discrepancy between final answer accuracy and the validity of full proofs, as well as the impact of best-of-n selection on proof quality.

搜集汇总

数据集介绍

构建方式

Open Proof Corpus (OPC) 数据集通过系统性流程构建，包含来自国际数学奥林匹克（IMO）、美国数学奥林匹克（USAMO）等顶级竞赛的1,000余道题目，并由前沿大语言模型（如GEMINI-2.5-PRO、O4-MINI等）生成5,062份证明。每份证明均经过13位前IMO参赛者或国家级选拔赛优胜者的双重评审，采用定制化Web界面实现高效标注，并通过10%样本的双重评分验证，确保标注一致性达90.4%。数据构建特别设计了问题筛选机制，平衡正负样本比例，并整合MathArena和PutnamBench等子集以支持形式化与自然语言证明的对比研究。

特点

OPC的核心价值在于其规模性与严谨性：作为首个包含大量正确LLM生成证明的开放数据集，其43%的正确率揭示了模型在复杂数学推理中的潜力。数据集涵盖高中至本科难度层级，特别包含60道问题的8次生成样本，支持最佳N选择策略研究。独特的人类反馈标注不仅包含二元判断，还提供错误定位注释，如逻辑漏洞或定理误用。数据分布上，IMO Shortlist问题占比17.6%，模型间性能差异显著（GEMINI-2.5-PRO正确率最高），为证明生成能力的多维度评估提供了基准。

使用方法

研究者可通过Hugging Face平台获取OPC数据集，其四类子集设计明确区分使用场景：MathArena和PutnamBench作为测试集评估模型性能；Generic和Best-of-n子集支持模型微调与采样策略优化。实际应用中，可利用该数据集进行三类关键分析：（1）通过对比自然语言与形式化证明的准确率（11倍差距），探究推理范式差异；（2）结合最终答案与完整证明的正确性关联（如O3模型存在30%性能落差），验证评估指标的可靠性；（3）采用瑞士轮排名法等最佳N选择策略，将证明生成准确率提升17%。数据集附带的8B参数微调模型可实现88.1%的证明判断准确率，与顶级商业模型持平。

背景与挑战

背景概述

Open Proof Corpus (OPC)是由ETH Zurich和INSAIT等机构的研究团队于2025年创建的大规模数学证明数据集，旨在解决大型语言模型在数学证明生成领域缺乏高质量评估基准的问题。该数据集包含5,000余条经过人工验证的数学证明，覆盖IMO、USAMO等顶级数学竞赛题目，首次系统性地收录了LLM生成的正确证明。作为数学推理领域的重要资源，OPC为证明生成模型的训练与评估提供了标准化平台，推动了形式化证明与自然语言证明的对比研究。

当前挑战

该数据集面临的核心挑战包括：1) 领域问题方面，需解决数学证明生成中自然语言与形式化验证的效能差距（实验显示自然语言证明解决能力是形式化方法的11倍），以及最终答案准确性与完整证明有效性之间的显著差异（部分模型差异达30%）；2) 构建过程中需克服人工验证的高成本问题（依赖13位IMO级评审）、证明质量评估的主观性（评审间一致率90.4%），以及模型在几何推理和不等式处理中的系统性错误。此外，数据污染风险和问题难度集中于中学水平也构成局限性。

常用场景

经典使用场景

Open Proof Corpus (OPC) 数据集在数学证明生成研究中具有广泛的应用场景。该数据集包含了超过5,000个人工评估的数学证明，这些证明由先进的LLM生成，并涵盖了多种数学竞赛题目，如USAMO和IMO。研究人员可以利用OPC数据集来评估和比较不同LLM在数学证明生成任务中的表现，特别是在自然语言证明和形式化证明生成之间的性能差异。此外，该数据集还可用于探索最佳采样策略对证明质量的影响，以及分析最终答案准确性与完整证明有效性之间的差异。

解决学术问题

OPC数据集解决了数学证明生成研究中的多个关键问题。首先，它填补了大规模、高质量数学证明数据集的空白，为训练和评估LLM提供了重要资源。其次，该数据集使得研究人员能够系统地研究自然语言证明与形式化证明之间的性能差距，揭示了当前LLM在这两种证明生成任务中的优劣势。此外，OPC还帮助研究者深入理解最终答案准确性与完整证明有效性之间的不一致性，为开发更可靠的数学推理评估方法奠定了基础。

衍生相关工作

基于OPC数据集，已经衍生出多项重要研究工作。例如，研究人员利用该数据集微调了一个8B参数的模型，在证明正确性评估任务上达到了与最佳模型GEMINI-2.5-PRO相当的性能。此外，OPC还启发了对最佳采样策略的深入研究，开发了基于排名的选择方法，显著提高了证明生成的质量。该数据集也为后续的数学推理基准测试和评估框架的开发提供了重要参考，推动了数学自动推理领域的整体进步。