DeepTheorem

DeepTheorem是一个包含12.1万条IMO级别非正式数学定理及其高质量证明的大型自然语言数据集，系统性地标注了正确性、难度、主题多样性，并包括可验证的定理变体，适合高级强化学习。数据集从多个网络语料库中挖掘，通过严格的去重和清洗过程，保证了数据的纯净性和多样性。DeepTheorem为推动大型语言模型在非正式数学定理推理方面的发展提供了宝贵的资源。

DeepTheorem is a large-scale natural language dataset containing 121,000 IMO-level informal mathematical theorems and their high-quality proofs. It is systematically annotated with correctness, difficulty level and topic diversity, and includes verifiable theorem variants, making it suitable for advanced reinforcement learning. Curated from multiple web corpora, the dataset undergoes stringent deduplication and cleaning processes to ensure its purity and diversity. DeepTheorem serves as a valuable resource for advancing the development of large language models in the field of informal mathematical theorem reasoning.

搜集汇总

数据集介绍

构建方式

DeepTheorem数据集的构建始于从MMIQC、WebInstruct和NuminaMath-CoT等多个来源聚合原始数据。随后通过严格的去污染流程，使用嵌入模型生成句子嵌入并计算余弦相似度，以识别并移除与测试数据集重叠的样本，确保数据集的独立性。接着，通过LLM验证问题的完整性并生成高质量的定理-证明对，最终保留难度评分≥5的121K个挑战性定理，形成数据集。

使用方法

DeepTheorem数据集可通过监督微调（SFT）和强化学习（RL-Zero）两种方式使用。在SFT中，模型通过模仿数据集中的证明进行学习；在RL-Zero中，模型通过探索已验证的定理变体来增强数学推理能力。评估时，采用结果评估（检查定理及其变体的真值预测一致性）和过程评估（分析证明的逻辑有效性、完整性和清晰度）相结合的方法，全面衡量模型的推理性能。

背景与挑战

背景概述

DeepTheorem数据集由腾讯AI Lab与上海交通大学的研究团队于2025年提出，旨在推动大语言模型在非形式化数学定理证明领域的发展。该数据集包含12.1万条国际数学奥林匹克（IMO）难度级别的定理-证明对，覆盖代数、几何、数论等多个数学领域，并标注了正确性标签、难度等级和主题分类。其创新性在于采用自然语言而非传统形式化证明系统，更贴合大语言模型的预训练知识结构。该数据集通过强化学习策略RL-Zero显著提升了模型在数学推理任务中的表现，成为评估AI复杂推理能力的重要基准。

当前挑战

DeepTheorem面临的挑战主要体现在两个方面：领域问题层面，传统自动定理证明（ATP）依赖形式化系统，与LLMs基于自然语言的预训练知识存在根本性错配，如何建立自然语言与数学推理的有效桥梁是关键难题；数据构建层面，需确保IMO级定理的高质量标注，包括处理逻辑一致性验证（如1.08M定理对的逻辑校验）、难度分级（基于9级标度筛选难度≥5的题目）以及严格去污染（清除与MATH、AIME等基准重叠的199K样本）。此外，生成可验证的定理变体（如通过逻辑蕴含或矛盾生成242K变体）对强化学习训练也提出极高要求。

常用场景

经典使用场景

DeepTheorem数据集在自然语言处理与自动定理证明领域具有广泛的应用价值。其核心应用场景包括训练和评估大型语言模型（LLMs）在数学推理和定理证明方面的能力。通过提供121K个高质量的非正式数学定理及其证明，数据集能够支持模型从自然语言的角度理解和生成数学证明，从而弥补传统形式化证明系统与LLMs预训练知识之间的鸿沟。

解决学术问题

DeepTheorem解决了多个关键的学术研究问题，特别是在非正式定理证明领域。首先，它通过大规模的自然语言定理和证明对，为LLMs提供了丰富的训练数据，显著提升了模型在复杂数学推理任务中的表现。其次，数据集引入了RL-Zero训练策略，进一步优化了模型的推理能力，超越了传统的监督微调方法。此外，数据集还提供了全面的评估指标，包括结果评估和过程评估，为研究社区提供了可靠的性能衡量标准。

实际应用

在实际应用中，DeepTheorem数据集被广泛用于开发智能教育工具和自动化证明辅助系统。例如，它可以用于构建能够自动生成数学证明的AI助手，帮助学生和研究人员快速理解和验证复杂的数学定理。此外，数据集还可以用于开发竞赛级别的数学问题求解系统，为数学奥林匹克竞赛（IMO）等高水平数学竞赛提供支持。

数据集最近研究

最新研究方向

DeepTheorem数据集在自然语言定理证明领域的最新研究方向主要集中在利用大规模语言模型（LLMs）的预训练知识，通过自然语言和强化学习相结合的方法提升定理证明能力。该数据集包含12.1万条高质量的IMO级别非正式定理及其证明，涵盖了多样化的数学领域，并通过系统构建的可验证定理变体支持强化学习策略（如RL-Zero）的训练。前沿研究探索了如何利用自然语言的灵活性来弥补传统形式化证明系统与LLMs预训练知识之间的鸿沟，从而在自动化非正式定理证明和数学推理方面取得突破。此外，该数据集还推动了过程评估框架的发展，不仅关注证明结果的正确性，还深入分析推理步骤的逻辑有效性、完整性和清晰度，为LLMs在复杂数学推理任务中的表现提供了更全面的评估标准。

相关研究论文

• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning

  腾讯与上海交通大学 · 2025年