ChristianZ97/putnambench-satp

PutnamBench Lean 4问题集，经过SATP-DSP-Eval流程标准化处理。包含672个问题，主要用于数学定理证明和形式化验证。数据集来源于trishullab/PutnamBench，并经过解析脚本处理。数据集包含多个字段，如问题名称、形式化声明、非正式声明、解决方案、标签等。

PutnamBench Lean 4 problems normalized for the SATP-DSP-Eval pipeline. Contains 672 problems, primarily used for mathematical theorem proving and formal verification. The dataset originates from trishullab/PutnamBench and is processed by a parsing script. It includes various fields such as problem name, formal statement, informal statement, solution, tags, etc.

搜集汇总

数据集介绍

构建方式

PutnamBench-SATP 数据集基于 PutnamBench 原生 Lean 4 源码及非正式问题描述构建，经标准化处理以适配 SATP-DSP-Eval 评估流水线。其构建流程涵盖：从上游仓库抽取 `lean4/src/*.lean` 文件中的形式化定理陈述及 `informal/putnam.json` 中的英文问题与解答，并借助 `parse_lean4.py` 脚本解析每个文件首部的 `import`、`open`、`open scoped` 及 `set_option` 等导入指令，汇聚为 `header` 字段。关键规范化步骤包括将 `formal_statement` 的末尾由 `:= sorry` 统一改写为 `:= by`（省略尾随策略），并基于规范化后形式化陈述的 SHA256 哈希值截取前 16 字符生成唯一标识符 `uuid`，从而保证每个问题的可追溯性与一致性。

特点

该数据集汇聚 672 道来自普特南数学竞赛的 Lean 4 形式化问题，集高等数学挑战与形式验证于一身。其核心特色在于提供了结构一致、可直接用于定理证明器评估的标准化数据：每个样本包含稳定的 `name`（即可读的问题名称，如 `putnam_1962_a1`）、经规范的形式化定理陈述（以 `:= by` 结尾）、完整的导入头、英文非正式陈述与解题思路、标注的数学分类标签（如代数、分析、几何）以及恒为 `"test"` 的分割字段。所有字段除规范化处理外均保留上游原貌，确保了数据纯净度与可复现性。

使用方法

本数据集专为评估神经定理证明系统在纯数学推理任务上的表现而设计，适用于微调或零样本评估场景。用户可直接加载各样本的 `formal_statement` 与 `header` 字段作为 Lean 4 输入，驱动证明搜索器（如 GPT-4、ReProver 等）生成完整证明；借助 `informal_statement` 与 `informal_solution` 进行跨形式与非形式空间的对照分析；利用 `tags` 按数学子领域筛选问题，开展针对性模块测试。所有样本均归入 `"test"` 分割，便于统一量化模型在普特南竞赛级别问题上的形式化证明能力。

背景与挑战

背景概述

PutnamBench-SATP 数据集由 George Tsoukalas 等研究人员于2024年创建，依托于普特南数学竞赛（Putnam Mathematical Competition）的经典题目，旨在评估神经定理证明器在高等数学推理任务中的表现。该数据集包含672道经标准化处理的 Lean 4 形式化定理问题，覆盖代数、分析、几何等多个数学分支。作为 PutnamBench 的衍生版本，它通过 SATP-DSP-Eval 流水线进行归一化处理（如将形式化陈述统一为 `:= by` 结尾、添加唯一标识符与导入头部信息），为定理自动证明领域提供了高难度、高权威性的基准测试。其影响力体现在推动神经符号系统与形式化验证技术的交叉融合，尤其对 Large Language Models 在数学推理泛化能力上的评估具有里程碑意义。

当前挑战

PutnamBench-SATP 所解决的领域核心挑战在于，当前神经定理证明器在应对多项选择或基础数学问题外的高阶推理时表现欠佳，而普特南竞赛题目对创造性、多步推演与严格形式化要求极高，恰好成为检验模型深层理解与泛化能力的试金石。数据集构建过程中面临两大技术挑战：一是将自然语言描述的竞赛问题精准翻译为 Lean 4 形式化语言，需兼顾语法严谨性与原始题意的保真度；二是对上游数据中格式不一的 `formal_statement` 进行标准化处理（如去除 `:= sorry` 占位符并改为 `:= by`），同时通过 SHA256 哈希生成稳定标识符以避免歧义，这要求解析脚本具备高度鲁棒性以处理 Lean 源码中的导入、作用域及设置指令等复杂结构。

常用场景

经典使用场景

PutnamBench-SATP 是一个专为定理证明任务设计的基准数据集，源自于富有盛誉的威廉·洛厄尔·普特南数学竞赛（William Lowell Putnam Mathematical Competition）。该数据集包含了672个经过SATP（Statement-Aware Theorem Proving）归一化处理的Lean 4形式化问题，每个问题均以规范的定理语句呈现，并附有英文的非正式问题描述与解答思路。在经典使用场景中，研究人员利用此数据集训练和评估基于神经网络的定理证明系统，测试模型在高等数学推理、多步推导和符号操作方面的能力。通过将非正式的自然语言问题转化为严格的形式化定理证明任务，PutnamBench-SATP 为自动定理证明领域提供了一个高难度、高代表性的评测平台，推动了证明搜索、策略学习与语言模型在数学推理中的深度融合。

解决学术问题

PutnamBench-SATP 的核心价值在于解决了自动定理证明研究中缺乏高难度、标准化形式化数学基准的学术困境。以往的数据集多集中于初等数学或逻辑问题，难以全面评估模型在抽象代数、实分析、组合数学等高等数学分支上的推理能力。该数据集通过统一规范化处理（如将定理语句末尾的 ':=' 改为标准形式），并引入基于SHA256的稳定标识符 'uuid'，确保了实验结果的可重复性和跨系统公平比较的基石。其672个问题的规模与难度梯度，使得研究者能够系统性地分析神经定理证明器在复杂命题分解、多步推理链构建和搜索空间缩减等核心学术问题上表现，进而揭示当前技术在处理非平凡数学证明时的瓶颈与突破方向。

衍生相关工作

PutnamBench-SATP 的发布催生了一系列与之紧密相关的经典工作。首先，其上游项目 PutnamBench（Tsoukalas et al., 2024）开创了将普特南竞赛问题系统形式化为Lean 4代码的先河，并提出了基于SATP的归一化流程，后续研究在此基础上扩展了多语言支持和大规模证明搜索策略。其次，该数据集被用于评估GPT-4、Codex等大语言模型在形式化定理证明中的表现，衍生出针对证明状态编码与注意力机制的改进方案。此外，部分学者借鉴其 'uuid' 稳定标识和 'header' 元数据结构，构建了可扩展的定理证明元基准架构，推动了跨数据集的公平评测方法论发展。还有工作将 PutnamBench-SATP 与 Reinforcement Learning 结合，探索通过课程学习策略逐步提升证明器在难题上的搜索效率，这些衍生工作共同推动了神经定理证明从简单玩具命题向高等数学竞技场的跨越。