Goedel-Pset-v1-solved

这是一个由Goedel-Prover在最大的Lean4语句集Goedel-Pset-v1上生成的数据集。对于每个问题，数据集保留了两个正确答案，并且包含了mathlib。使用这个数据集，通过简单的监督微调训练了Goedel-Prover-SFT模型，该模型在miniF2F上达到了57%的最先进性能。

搜集汇总

数据集介绍

构建方式

该数据集基于Goedel-Prover系统在Lean4语言环境下的大规模数学命题集合Goedel-Pset-v1上生成。通过自动化定理证明技术，为每个数学问题保留两个正确答案的完整证明过程，并整合了mathlib数学库的核心内容。构建过程中采用严格的验证机制确保证明的正确性，最终形成包含255万条训练样本的高质量数据集。

特点

数据集以形式化数学证明为核心特征，每条数据记录包含完整的机器可验证证明链。其独特价值在于同时提供命题陈述与标准化证明路径，覆盖范围从基础引理到复杂定理。作为目前最大的开放形式化数学数据集之一，其证明过程严格遵循Lean4交互式定理证明器的语法规范，为机器学习模型提供结构化、可解析的数学推理范例。

使用方法

该数据集专为训练自动化定理证明系统设计，可直接用于监督式微调任务。研究人员可加载完整数据集后，以full_proof字段作为监督信号训练神经证明器。经实践验证，基于该数据集训练的Goedel-Prover-SFT模型在miniF2F基准测试中达到57%的准确率，使用时应注重保持原始证明结构的完整性以发挥最佳效果。

背景与挑战

背景概述

Goedel-Pset-v1-solved数据集是自动化定理证明领域的重要成果，由Goedel-LM团队于2025年基于Lean4语句集构建。该数据集通过Goedel-Prover系统生成，每个问题保留两个正确答案，并整合了mathlib数学库资源。作为自动化推理领域的前沿研究，其核心价值在于为监督微调提供了高质量的训练样本，推动开源定理证明系统的发展。相关论文发表于arXiv平台，研究团队来自普林斯顿等知名机构，该成果在miniF2F基准测试中达到57%的准确率，显著提升了自动推理模型的性能上限。

常用场景

经典使用场景

在自动定理证明领域，Goedel-Pset-v1-solved数据集通过提供大量经过验证的数学证明，为机器学习模型提供了丰富的训练素材。该数据集特别适用于训练和评估定理证明系统，尤其是在形式化数学环境中。研究人员可以利用这些结构化证明来探索定理自动生成的边界，提升模型在复杂逻辑推理任务中的表现。

实际应用

在实际应用中，Goedel-Pset-v1-solved数据集已被用于开发前沿的定理证明辅助工具。这些工具能够协助数学家快速验证猜想，或在教育领域帮助学生理解复杂数学证明的结构。数据集中的证明来源于Lean4形式化数学库，确保了其在学术和工业场景中的实用性与权威性。

衍生相关工作

基于该数据集训练的Goedel-Prover-SFT模型已在自动定理证明领域产生了广泛影响。其开源性特质催生了一系列改进工作，包括证明搜索算法的优化和新型神经网络架构的探索。这些衍生研究共同推动了自动推理系统在数学基础研究和教育应用中的进步。