DeepTheorem

DeepTheorem数据集包含121K个IMO级别的不严格定理和证明，覆盖了广泛的数学领域。每个定理-证明对都经过严格的准确性注释，包括由o3-mini模型生成或验证的证明、定理的真值、难度等级、主题分类以及定理的正负变体。

The DeepTheorem dataset contains 121K IMO-level informal theorems and proofs, covering a broad range of mathematical fields. Each theorem-proof pair has undergone rigorous accuracy annotation, including proofs generated or verified by the o3-mini model, the truth value of the theorem, difficulty levels, topic classifications, as well as positive and negative variants of the theorems.

原始信息汇总

DeepTheorem 数据集概述

基本信息

• 许可证: MIT
• 数据集大小: 1,146,705,612 字节
• 下载大小: 554,423,240 字节
• 训练集样本数: 120,754

数据特征

• id: 唯一标识符 (int64)
• source: 数据来源 (string)
• ori_question: 原始问题 (string)
• ori_solution: 原始解答 (string)
• domain: 数学领域 (string序列)
• difficulty: 难度等级 (float64)
• rationale: 推理过程 (string)
• informal_theorem: 非正式定理 (string)
• informal_theorem_qa: 非正式定理问答 (string)
• proof: 证明过程 (string)
• truth_value: 真值 (bool)
• pos: 正例结构体
  • question: 问题 (string)
  • response: 回答 (string)
  • truth_value: 真值 (bool)
• neg: 负例结构体
  • question: 问题 (string)
  • response: 回答 (string)
  • truth_value: 真值 (bool)

数据集特点

1. 规模与质量

   • 包含121K个IMO级别的非正式定理和证明
   • 覆盖多个数学领域：代数、几何、数论等

2. 标注信息

   • 数学准确性验证（通过o3-mini模型）
   • 定理真值标注（真/假）
   • 难度等级分类
   • 主题分类标注
   • 包含正负变体定理

3. 评估指标

   • 在FIMO、HMMT和Putnam等数学竞赛数据集上评估
   • 与Gemini、o1等商业模型对比性能

性能表现

模型	FIMO(out.)	FIMO(proc.)	HMMT(out.)	HMMT(proc.)	Putnam(out.)	Putnam(proc.)	平均排名(out.)	平均排名(proc.)
DeepTheorem-RL-7B	55.56	39.07	28.81	20.85	57.29	42.20	47.22(#5)	34.04(#5)

搜集汇总

数据集介绍

构建方式

DeepTheorem数据集通过整合国际数学奥林匹克竞赛（IMO）级别的非正式定理与证明，构建了一个高质量的数学推理资源库。该数据集采用多阶段标注流程，首先由o3-mini模型生成或验证定理证明，确保数学严谨性；随后人工标注真实值、难度等级及学科分类，并系统性地构建了共享相同或相反真实值的定理变体，为强化学习训练提供丰富素材。数据来源涵盖代数、几何、数论等多个数学领域，最终形成包含12.1万条样本的标准化结构。

使用方法

研究者可利用该数据集进行定理证明任务的端到端训练，通过加载标准化的训练分割数据快速构建基线模型。典型流程包括：基于原始问题和非正式定理进行模型预训练，利用变体样本实施强化学习微调，最后通过验证集评估模型在不同难度和学科上的表现。数据集中提供的真值标签和难度分级支持多维度性能分析，而结构化存储的证明过程可直接用于生成任务的数据增强。建议结合RL-Zero策略进行训练，以充分发挥变体样本在提升模型鲁棒性方面的作用。

背景与挑战

背景概述

DeepTheorem数据集由前沿研究团队于近年推出，旨在革新大语言模型在数学定理证明领域的推理能力。该数据集聚焦于国际数学奥林匹克竞赛（IMO）级别的高难度定理证明问题，通过自然语言形式呈现，突破了传统形式化证明系统的局限。其核心创新在于将强化学习策略与大规模非正式数学推理数据相结合，为评估和提升语言模型的复杂逻辑推理能力设立了新基准。数据集涵盖代数、几何、数论等多个数学分支，每个定理均经过严格验证并标注难度等级，为人工智能在高级数学推理领域的研究提供了重要基础设施。

当前挑战

DeepTheorem面临的挑战主要体现在两个维度：在领域问题层面，如何准确评估语言模型对非正式数学表述的理解深度仍存在困难，特别是当处理反例构造和真值判定等复杂推理任务时。数据集构建过程中，确保数千个高阶定理证明的数学严谨性耗费大量专家资源，而生成具有相同逻辑结构但真值相反的有效变体定理，需要精密的语义保持与逻辑转换技术。此外，不同数学领域间知识表示的异质性，以及难度分级标准在跨学科场景下的统一性，均为数据质量控制带来显著挑战。

常用场景

经典使用场景

在数学推理与定理证明领域，DeepTheorem数据集以其丰富的非正式数学定理和证明对，成为评估和提升大型语言模型（LLM）数学推理能力的经典工具。该数据集广泛应用于训练和验证模型在复杂数学问题上的表现，特别是在国际数学奥林匹克（IMO）级别的问题上。通过提供多样化的数学领域和难度级别的定理，DeepTheorem为研究人员提供了一个标准化的测试平台，用以衡量模型在非正式数学语言理解和推理上的能力。

解决学术问题

DeepTheorem数据集解决了传统形式化证明系统与LLM在非正式数学语言理解上的不匹配问题。通过提供高质量的非正式定理和证明，该数据集填补了LLM在数学推理研究中的空白，使得研究人员能够更准确地评估模型在复杂数学问题上的表现。此外，数据集的真理值和难度标注为研究模型在不同复杂度问题上的泛化能力提供了重要依据，推动了自动定理证明领域的进步。

实际应用

在实际应用中，DeepTheorem数据集被广泛用于开发和优化数学辅助工具和教育软件。通过利用数据集中的非正式定理和证明，开发者能够构建更智能的数学辅导系统，帮助学生和研究者理解和解决复杂的数学问题。此外，该数据集还被用于增强商业语言模型（如Gemini和o1）的数学推理能力，提升其在科学计算和教育领域的应用效果。

数据集最近研究

最新研究方向

在数学定理证明领域，DeepTheorem数据集通过融合自然语言处理与强化学习技术，为大型语言模型的推理能力评估开辟了新路径。该数据集以其高质量的IMO级非正式定理及证明为核心，覆盖代数、几何、数论等多学科领域，并创新性地引入验证性定理变体构建机制，显著提升了模型对数学概念深层逻辑的捕捉能力。当前研究聚焦于RL-Zero强化学习策略的优化，通过利用定理变体激励机制，推动语言模型在非形式化推理中的鲁棒性表现。其性能评估体系（如FIMO、HMMT等基准测试）显示，该方法在商业与开源模型中均具备竞争力，尤其验证了自然语言交互在复杂数学问题求解中的可行性，为自动推理系统的实际应用提供了重要范式。