hoskinson-center/proofnet

ProofNet是一个用于自动形式化和形式证明本科级别数学问题的基准数据集。该基准包含371个示例，每个示例包括Lean 3中的形式定理声明、自然语言定理声明和自然语言证明。问题主要来自流行的本科纯数学教科书，涵盖实分析和复分析、线性代数、抽象代数和拓扑学等主题。ProofNet旨在成为一个具有挑战性的基准，推动自动形式化和自动定理证明的进展。ProofNet is a benchmark dataset for automated formalization and formal proof of undergraduate-level mathematical problems. This benchmark contains 371 examples, each including formal theorem statements in Lean 3, natural language theorem statements, and natural language proofs. The problems are mainly sourced from popular undergraduate pure mathematics textbooks, covering topics such as real and complex analysis, linear algebra, abstract algebra, and topology. ProofNet aims to serve as a challenging benchmark that advances research in automated formalization and automated theorem proving.

原始信息汇总

数据集概述

名称: ProofNet

目的: 用于自动形式化和形式证明本科水平的数学问题。

内容: 包含371个示例，每个示例包括一个Lean 3中的形式定理声明、一个自然语言定理声明和一个自然语言证明。问题主要来自流行的本科纯数学教科书，涵盖实分析、复分析、线性代数、抽象代数和拓扑学等主题。

数据字段:

• id: 问题的唯一字符串标识符。
• nl_statement: 自然语言定理声明。
• nl_proof: 自然语言证明，使用LaTeX格式，依赖于amsthm, amsmath, amssymb包。
• formal_statement: Lean 3中的形式定理声明。
• src_header: 文件头，包括导入、命名空间和位置，需要手动下载并放置在包含形式声明的.lean文件的同一目录中的common.lean。

许可证: MIT

引用: bibtex @misc{azerbayev2023proofnet, title={ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics}, author={Zhangir Azerbayev and Bartosz Piotrowski and Hailey Schoelkopf and Edward W. Ayers and Dragomir Radev and Jeremy Avigad}, year={2023}, eprint={2302.12433}, archivePrefix={arXiv}, primaryClass={cs.CL} }

性能评估

声明自动形式化:

模型	类型检查率	准确率
Davinci-code-002 (prompt retrieval)	45.2	16.1
Davinci-code-002 (in-context learning)	23.7	13.4
proofGPT-1.3B	10.7	3.2

声明非形式化:

模型	准确率
Code-davinci-002 (in-context learning)	62.3
proofGPT-6.7B (in-context learning)	6.5
proofGPT-1.3B (in-context learning)	4.3

作者

• Zhangir Azerbayev
• Bartosz Piotrowski
• Jeremy Avigad

搜集汇总

数据集介绍

构建方式

在数学自动形式化与定理证明领域，ProofNet数据集的构建体现了严谨的学术追求。该数据集从本科纯数学经典教材中精心选取了371个定理，涵盖实分析与复分析、线性代数、抽象代数及拓扑学等核心主题。每个样本均包含Lean 3形式化定理陈述、自然语言定理陈述及其对应的自然语言证明，确保了形式化与自然语言表述之间的精确对应。构建过程中，团队注重数学内容的代表性与难度平衡，旨在为自动形式化与自动定理证明研究提供一个具有挑战性的基准测试平台。

特点

ProofNet数据集在数学人工智能领域展现出独特价值。其核心特点在于紧密融合了形式化数学与自然语言数学表述，为跨模态推理研究提供了宝贵资源。数据集覆盖了本科阶段多个重要数学分支，问题设计兼具基础性与挑战性，能够有效评估模型在复杂数学逻辑理解与转换方面的能力。此外，数据集提供了完整的自然语言证明与形式化语句，支持从自动形式化到定理证明的全流程评估，为推动数学推理人工智能的发展奠定了扎实的数据基础。

使用方法

研究者可利用ProofNet数据集开展自动形式化与定理证明的前沿探索。使用前需配置Lean 3环境，并下载所需的公共依赖文件。数据集支持两种主要评估任务：一是根据自然语言定理生成可类型检查的Lean 3形式化语句，即自动形式化；二是将形式化语句转化为准确的自然语言描述，即非形式化。用户可通过加载数据集样本，分别对模型在两种任务上的性能进行量化评估，具体指标包括类型检查率与准确率等，从而系统衡量模型在数学语言理解与生成方面的综合能力。

背景与挑战

背景概述

ProofNet数据集于2023年由Zhangir Azerbayev、Bartosz Piotrowski、Jeremy Avigad等研究人员共同创建，旨在为自动形式化和形式证明领域提供基准测试。该数据集聚焦于本科数学内容，涵盖实分析与复分析、线性代数、抽象代数及拓扑学等核心主题，共包含371个示例，每个示例均包含Lean 3形式定理陈述、自然语言定理陈述及自然语言证明。其构建基于主流本科数学教材，推动了自动定理证明与自然语言处理在数学推理中的交叉研究，对提升人工智能的数学逻辑能力具有重要影响力。

当前挑战

ProofNet数据集面临的挑战主要集中于自动形式化任务，即将自然语言数学陈述准确转换为形式化语言（如Lean 3），这要求模型具备深度的数学语义理解与逻辑结构映射能力。构建过程中的挑战包括从多样化数学教材中提取并统一问题表述，确保形式化代码的语法正确性与数学严谨性，同时处理不同数学领域间的符号与术语差异。这些挑战使得该数据集成为评估模型在复杂数学推理中性能的关键工具。

常用场景

经典使用场景

在自动定理证明与形式化数学领域，ProofNet作为一项基准测试数据集，其经典使用场景聚焦于评估模型在自动形式化与定理证明任务中的性能。该数据集通过提供371个本科数学问题，涵盖实分析、复分析、线性代数等核心主题，为研究者构建了一个标准化的测试平台。模型需将自然语言定理陈述转化为Lean 3形式化语句，或反之进行非形式化转换，从而推动自动推理技术的边界拓展。

实际应用

在实际应用层面，ProofNet可服务于教育技术、智能辅导系统以及形式化验证工具的开发。例如，基于该数据集训练的模型能够辅助学生理解形式化证明结构，或帮助数学家将直觉性论证转化为机器可验证的代码。此外，在软件验证与安全关键系统设计中，此类技术可提升定理证明的自动化程度，增强复杂系统正确性的保障能力。

衍生相关工作

ProofNet的发布催生了多项经典研究工作，尤其是在大语言模型与定理证明的结合领域。例如，基于该数据集的评估推动了如proofGPT等专用模型的开发，这些模型专注于形式化数学任务的微调与优化。同时，相关研究探索了上下文学习、提示检索等策略在自动形式化任务中的应用，进一步丰富了自动推理方法学的技术图谱。