Goedel-Prover 数据集

Goedel-Prover数据集是由普林斯顿大学的研究团队创建的，包含1.64百万个形式化数学语句。这些语句是通过将从Numina等数据源获取的自然语言数学问题转化为_Lean_语言得到的。数据集通过训练两个形式化器来增强形式化语句的多样性，并使用_Lean_编译器验证语句的正确性。该数据集用于迭代训练定理证明器，以提高自动化定理证明的性能。

The Goedel-Prover dataset was created by a research team at Princeton University, and contains 1.64 million formal mathematical statements. These statements are generated by translating natural language mathematical problems sourced from datasets including Numina into the *Lean* formal language. The dataset enhances the diversity of formal statements by training two formalizers, and verifies the correctness of these statements using the *Lean* compiler. This dataset is used for iteratively training theorem provers to improve the performance of automated theorem proving.

搜集汇总

数据集介绍

构建方式

Goedel-Prover数据集的构建过程首先涉及将自然语言数学问题从Numina数据集中转换为形式化语言（Lean 4），这一步骤由训练有素的陈述形式化器完成。随后，大型语言模型（LLM）被用于验证形式化陈述是否准确保留了原始自然语言问题的内容。在此基础上，通过一系列证明者的迭代训练，逐步构建了一个大规模的形式化证明数据集。每个证明者都能证明前一个证明者无法证明的许多陈述，这些新的证明随后被添加到下一个证明者的训练集中。最终，该证明者在整个证明生成方面超过了所有现有的开源模型。

特点

Goedel-Prover数据集的特点在于其规模庞大，包含了1.64百万个形式化陈述。此外，该数据集通过专家迭代的方法进行构建，使得证明者在每轮迭代中都能够解决更多的问题，从而不断提高其性能。Goedel-Prover在miniF2F基准测试中取得了57.6%的成功率（Pass@32），超过了之前最佳的开源模型7.6%。在PutnamBench上，Goedel-Prover成功解决了7个问题（Pass@512），在排行榜上排名第一。

使用方法

使用Goedel-Prover数据集的方法包括首先训练陈述形式化器，将自然语言数学问题从Numina数据集中转换为形式化语言（Lean 4）。然后，使用LLM验证这些形式化陈述的准确性。最后，通过专家迭代训练一系列证明者，逐步构建形式化证明数据集。每个证明者都使用前一个证明者收集的正确证明进行监督微调，从而不断提高其性能。

背景与挑战

背景概述

在数学证明自动化的领域，Goedel-Prover 数据集标志着重大进展。由 Yong Lin 等研究人员于 2025 年提出的 Goedel-Prover，是一个开源的大型语言模型，旨在解决数学问题的自动形式化证明生成。该数据集的核心挑战在于形式化数学陈述和证明的稀缺性，研究人员通过训练陈述形式化器，将自然语言数学问题从 Numina 转换为形式语言（Lean 4），创建了一个包含 164 万个形式化陈述的数据集。这一突破性工作不仅为数学证明自动化领域提供了宝贵的资源，而且推动了机器学习在形式推理中的应用。

当前挑战

Goedel-Prover 数据集面临的挑战包括：1) 形式化数学陈述和证明的稀缺性，这是自动定理证明领域的关键难题；2) 训练过程中遇到的挑战，例如如何确保形式化陈述准确地保留原始自然语言问题的内容；3) 如何提高模型在复杂推理问题上的性能。尽管 Goedel-Prover 在 miniF2F 和 PutnamBench 等基准测试中取得了显著的成果，但仍然存在一些问题，例如证明风格的局限性、缺乏搜索和在线交互能力，以及如何整合外部符号计算工具等。这些挑战需要进一步的研究和探索，以推动数学证明自动化的未来发展。

常用场景

经典使用场景

Goedel-Prover 数据集主要用于自动形式化证明生成，它通过将自然语言数学问题从Numina翻译成形式语言（Lean 4），并使用LLMs验证形式化语句的准确性，最终实现了全证明生成。该数据集在miniF2F基准测试中达到了57.6%的成功率，超过了之前的最佳开源模型。

解决学术问题

Goedel-Prover 数据集解决了形式化数学语句和证明稀缺的问题，通过训练语句形式化器，将自然语言数学问题从Numina翻译成形式语言（Lean 4），创建了1.64百万个形式化语句的数据集。此外，它还解决了形式语言数据集大小有限的问题，通过专家迭代的方式，训练了一系列证明器，实现了全证明生成。

衍生相关工作

Goedel-Prover 数据集衍生了DeepSeek-Prover等经典工作，这些工作通过将自然语言数学问题从Numina翻译成形式语言（Lean 4），并使用LLMs验证形式化语句的准确性，最终实现了全证明生成。此外，它还衍生了InternLM2.5-StepProver和InternLM-Math-Plus等经典工作，这些工作通过专家迭代的方式，训练了一系列证明器，实现了全证明生成。