The Open Proof Corpus

这是一个大规模、人工验证的数据集，专注于LLM生成的证明。

This is a large-scale, manually verified dataset that focuses on proofs generated by LLMs.

原始信息汇总

The Open Proof Corpus 数据集概述

数据集基本信息

• 名称: The Open Proof Corpus
• 类型: 数学证明数据集（LLM生成证明的人工验证数据集）
• 许可证: MIT
• 编程语言: Python 3.12

数据集内容

• 包含LLM生成的数学证明及其人工验证结果
• 问题格式为JSON，包含：
  • 问题ID
  • 元数据（包括难度级别等）
  • 问题陈述
  • 标准解决方案（含图像链接）

主要功能

1. 实验复现: 可复现论文中的实验
2. 自定义实验: 支持通过用户界面运行自定义实验
3. 模型训练: 提供基于该数据集的模型训练流程

配置管理

• 项目配置: 定义项目名称、管理员和模型配置
• 求解器配置: 设置问题提示、采样数量等
• 分配配置: 控制问题分配给评审者的参数
• 评审者配置: 定义评审者属性和工作量分配

数据处理流程

1. 问题添加:
   • 以JSON格式添加新问题
   • 通过脚本处理和验证问题
2. 问题求解: 生成模型输出
3. 问题分配: 将问题分配给评审者
4. 结果收集: 从网站获取评审结果
5. 结果转换: 将原始结果转换为训练数据格式

模型训练

• 预处理: 将数据转换为parquet格式
• 训练配置: 支持超参数调整
• 训练执行: 支持本地和Slurm集群训练
• 模型保存: 最佳验证结果和最新检查点分别保存

评估功能

• LLM评审评估: 评估模型作为评审者的能力
• 结果计算: 计算测试集上的评审结果

引用信息

bibtex @article{openproofcorpus2025, title={The Open Proof Corpus: A Large-Scale Human Study of LLM Proofs}, author={Jasper Dekoninck and Ivo Petrov and Kristian Minchev and Mislav Balunovic and Martin Vechev and Miroslav Marinov and Maria Drencheva and Lyuba Konova and Milen Milenov Shumanov and Kaloyan Tsvetkov and Lazar D. Todorov and Kalina Nikolova and Nikolay Georgiev and Vanesa Kalinkova and Margulan Ismoldayev}, journal={arXiv}, year={2025}, }

搜集汇总

数据集介绍

构建方式

The Open Proof Corpus数据集通过系统化的流程构建，涵盖了大规模语言模型生成的数学证明。其构建过程包括问题收集、模型求解、人工验证和数据处理四个主要阶段。研究人员首先从数学竞赛中精选问题，并设计标准化格式存储原始数据。随后利用多种语言模型生成候选证明，通过精心设计的评审流程，由专业数学工作者对证明质量进行多轮评估。数据验证环节确保问题与解决方案的唯一性和一致性，最终形成结构化的训练语料库。

特点

该数据集最显著的特点是实现了人类专家与AI系统的协同验证机制。数据集包含丰富的元数据标注，包括问题难度分级、证明错误分类等细粒度信息。其双盲评审设计有效避免了评估偏差，而瑞士轮赛制的引入则优化了证明质量的比较效率。数据格式兼容多种机器学习框架，特别设计了支持数学公式渲染的图像存储方案，为形式化验证研究提供了独特价值。

使用方法

使用者可通过模块化的工作流程灵活应用该数据集。安装环节支持UV和Conda两种环境管理方式，配置系统采用YAML文件实现高度可定制化。研究人员可基于提供的Flask框架快速部署评审界面，或通过命令行工具完成问题分配、进度监控等全流程操作。数据集特别设计了模型验证模块，支持离散评估、连续评分等多种评判模式，并内置了结果转换脚本，便于直接用于监督学习或强化学习任务的训练数据准备。

背景与挑战

背景概述

The Open Proof Corpus是由Jasper Dekoninck等研究人员于2025年创建的大规模数学证明数据集，旨在系统评估大型语言模型（LLM）在数学证明生成方面的能力。该数据集由苏黎世联邦理工学院等机构联合开发，通过严谨的人类验证流程构建，包含丰富的数学问题及其对应证明。作为首个专注于LLM生成证明质量评估的标准化数据集，它为形式化验证、自动推理等领域的算法研究提供了重要基准，推动了可解释AI在数学推理方向的发展。

当前挑战

该数据集面临的核心挑战体现在两个维度：在领域问题层面，数学证明的严谨性要求与LLM生成内容的不确定性构成根本矛盾，需要建立细粒度的错误分类体系来评估证明质量；在构建过程层面，如何设计有效的众包验证机制以确保标注一致性，以及处理证明步骤间的逻辑依赖关系，成为技术实现的关键难点。此外，保持问题难度分布的平衡性，同时解决不同数学领域术语的标准化问题，也是数据集构建过程中需要克服的挑战。

常用场景

经典使用场景

在数学逻辑与形式化验证领域，The Open Proof Corpus数据集为研究者提供了大规模、经过人工验证的LLM生成证明集合。该数据集广泛应用于验证大型语言模型在数学推理任务中的表现，特别是在自动定理证明和形式化数学场景下。研究者通过对比不同模型生成的证明质量，能够深入分析模型在逻辑一致性、推理深度和数学严谨性等方面的差异。

解决学术问题

该数据集有效解决了形式化验证领域缺乏标准化评估基准的难题。通过提供人类专家验证的证明样本，它为量化LLM的数学推理能力提供了可靠依据。在自动定理证明研究中，该数据集帮助识别模型常见的逻辑缺陷，如过度泛化、计算步骤缺失等问题，推动了可解释性数学推理模型的发展。

衍生相关工作

基于该数据集衍生的经典研究包括自动化证明评分系统、混合人类-AI协作验证框架等。多项工作探索了不同提示工程策略对证明质量的影响，推动了few-shot数学推理技术的发展。在可解释AI方向，研究者利用该数据集开发了证明错误定位工具，显著提升了模型输出的可信度。