l3lab/miniCTX

miniCTX数据集包含数学定理的上下文、定理声明、定理名称、文件创建信息、定理创建信息、文件名称、位置元数据、依赖元数据和证明元数据。每个条目以JSON格式表示，提供了定理的详细信息和证明过程。数据集还提供了用于评估的各个分割的链接和git提交版本。

The miniCTX dataset contains the context of mathematical theorems, theorem statements, theorem names, file creation information, theorem creation information, file names, position metadata, dependency metadata, and proof metadata. Each entry is represented in JSON format, providing detailed information about the theorem and its proof. The dataset also provides links and git commit versions for each split for evaluation purposes.

原始信息汇总

miniCTX 数据集概述

数据集结构

每个数据集条目包含以下部分：

• srcContext: 源文件中定理之前的上下文，包括导入和相关定义。
• theoremStatement: 定理的陈述。
• theoremName: 定理的名称。
• fileCreated: 文件创建时的git提交哈希。
• theoremCreated: 定理添加时的git提交哈希。
• file: 包含定理的文件名。
• positionMetadata:
  • lineInFile: 定理在文件中的行号。
  • tokenPositionInFile: 定理开始前的文件中的token数量。
  • theoremPositionInFile: 文件中定理之前的定义或定理数量。
• dependencyMetadata:
  • inFilePremises: 定理是否使用同一文件中的定义或引理。
  • repositoryPremises: 定理是否使用同一仓库中其他文件的定义或引理。
• proofMetadata:
  • hasProof: 定理是否有证明。
  • proof: 定理的证明。
  • proofType: 证明类型，如术语证明或策略证明。
  • proofLengthLines: 证明的行数。
  • proofLengthTokens: 证明的token数量。

数据集来源

数据集包含以下部分的链接和git提交版本：

• PrimeNumberTheoremAnd: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd, commit 23650db830a45c227bd85d25d520725545192333
• PFR: https://github.com/teorth/pfr, commit 6aeed6ddf7dd02470b3196e44527a6f3d32e54cf
• Mathlib: https://github.com/leanprover-community/mathlib4, commit f4b4298bd76b82f7b28f0fb6b5ab92bdf5e5634d
• HTPI: https://github.com/hanwenzhu/HTPILeanPackage4.7, commit 8eeebaec8d7fa17b5fe9d97589839ca2560e3ce2

搜集汇总

数据集介绍

构建方式

l3lab/miniCTX数据集的构建采取了对数学定理证明的上下文信息进行收集与整合的方法。该数据集从多个数学库中提取定理及其证明，包括前序代码、定理陈述、元数据等信息，并以JSON格式存储。数据集分为多个配置，每个配置包含验证集和测试集，涵盖了不同数学领域的定理，如数论、数学分析等。

使用方法

使用l3lab/miniCTX数据集时，用户可以根据需要选择不同的配置来获取相应的数据。每个数据条目均以JSON格式提供，包含源代码上下文、定理陈述、定理名称、创建时间、文件位置、依赖关系以及证明信息等。用户可以利用这些信息进行定理证明的机器学习研究，或是对数学定理证明的上下文进行深入分析。

背景与挑战

背景概述

l3lab/miniCTX数据集，作为定理证明领域的一项重要研究资源，由Hu Jiewen、Zhu Thomas和Welleck Sean等研究人员于2024年提出。该数据集旨在为神经网络定理证明提供带有丰富上下文信息的定理及其证明，涵盖数学、计算机科学等多个领域的定理。其核心研究问题是如何利用上下文信息，特别是长期依赖的上下文，来提高定理证明的准确性和效率。miniCTX的发布对于促进自动定理证明技术的发展和应用具有重要意义。

当前挑战

在构建miniCTX数据集的过程中，研究人员面临了多项挑战。首先，如何准确地提取和表示定理的上下文信息，包括相关的定义、定理和证明策略，是一大难题。其次，由于定理证明涉及到的上下文可能非常长，因此保持数据集的规模可控同时又能提供足够的上下文信息，也是数据集构建中的一个重要挑战。此外，数据集的多样性和覆盖面也是确保其能够适应不同研究领域和问题的重要考量。

常用场景

经典使用场景

在科学计算与形式化证明领域，l3lab/miniCTX数据集的典型应用场景在于支持神经定理证明系统，通过整合定理的上下文信息，包括前序文件内容、定理陈述以及元数据信息，以提升证明过程的准确性和效率。

解决学术问题

该数据集解决了传统定理证明中难以处理长上下文信息的难题，为学术研究提供了处理复杂数学证明的新途径。通过提供丰富的元数据，l3lab/miniCTX使得研究者能够更深入地理解定理之间的依赖关系，从而推动了自动化证明和数学形式化验证的发展。

实际应用

在实际应用中，l3lab/miniCTX数据集可用于训练机器学习模型，以辅助数学家验证定理的正确性，或是在软件开发中自动生成形式化证明，确保代码的健壮性和安全性。

数据集最近研究

最新研究方向

l3lab/miniCTX数据集近期研究方向聚焦于神经定理证明，特别是在融合长上下文信息方面取得了显著进展。该数据集通过引入丰富的源代码上下文，为定理证明任务提供了更全面的背景知识，有助于提升证明的准确性和效率。研究领域内的热点事件包括对数学库Mathlib的深入挖掘，以及在程序验证、科学计算等多个领域的应用探索。miniCTX数据集的提出，不仅丰富了形式化数学证明的数据资源，也为相关领域的研究提供了新的视角和工具，具有重要的学术价值和实践意义。