leanbench

LeanBench是一个用于评估AI系统在Lean 4定理证明任务性能的基准数据集，包含从真实Lean 4 pull requests提取的482个任务。数据以CSV/Parquet格式提供，每个任务包含：唯一标识符(task_id)、任务类型(task_type)、三级难度分类及数值评分(difficulty/difficulty_score)、来源仓库(repo)、PR编号(pr_number)、自然语言问题描述(problem_statement)、标准解决方案(golden_patch)和验证命令(verification_command)。任务难度分布为：Easy 330个、Medium 121个、Hard 31个，采用Apache 2.0许可证。

LeanBench is a benchmark dataset for evaluating AI systems on Lean 4 theorem proving tasks, containing 482 tasks extracted from real Lean 4 pull requests. Provided in CSV/Parquet formats, each task includes: unique identifier (task_id), task type (task_type), three-level difficulty classification with numerical score (difficulty/difficulty_score), source repository (repo), PR number (pr_number), natural language problem statement (problem_statement), golden solution (golden_patch in diff format), and verification command. Difficulty distribution: 330 Easy, 121 Medium, 31 Hard tasks, licensed under Apache 2.0.

原始信息汇总

LeanBench 数据集概述

基本信息

• 数据集名称：LeanBench Dataset
• 许可证：Apache 2.0
• 任务类别：文本生成（text-generation）
• 语言：英语（en）
• 标签：Lean4、定理证明、代码生成、基准测试（benchmark）

数据集规模

• 总任务数：482 个
• 难度分布：
  • 简单（Easy）：330 个
  • 中等（Medium）：121 个
  • 困难（Hard）：31 个

数据来源

所有任务均提取自真实的 Lean 4 项目的 Pull Request，涵盖多个 GitHub 仓库。

任务格式

每个任务包含以下关键字段：

字段名	说明
task_id	唯一标识符（如 LB-0001）
task_type	任务类型（如 pr_completion）
difficulty	难度等级（easy/medium/hard）
difficulty_score	数值化的难度评分
repo	来源 GitHub 仓库
pr_number	Pull Request 编号
problem_statement	任务的自然语言描述
golden_patch	期望的解决方案（diff 格式）
verification_command	验证解决方案的命令

数据文件

• leanbench_tasks.csv：完整数据集的 CSV 格式文件
• data/train-00000-of-00001.parquet：Parquet 格式的数据文件（适用于 datasets 库）

使用方式

可通过 Hugging Face 的 datasets 库加载使用：

python from datasets import load_dataset

dataset = load_dataset("foundry-ai/leanbench")

遍历任务

for task in dataset["train"]: print(task["task_id"], task["difficulty"])

配置信息

• 配置名称：default
• 数据文件：data/train-*.parquet（训练集）
• 大小类别：n<1K（少于 1000 个样本）

搜集汇总

数据集介绍

构建方式

在定理证明领域，形式化验证在确保数学论证严谨性方面扮演着至关重要的角色，而Lean 4作为一款功能强大的交互式定理证明器，其应用日益广泛。为评估人工智能系统在Lean 4环境下的定理证明能力，LeanBench数据集应运而生。该数据集通过从真实的GitHub拉取请求中精心提取问题与解决方案，构建了包含482个任务的基准集合。每个任务均包含自然语言描述的问题陈述、预期答案的差异补丁以及验证命令，确保了任务的真实性与可复现性。

特点

LeanBench数据集具备鲜明的结构与层次化难度设计。任务按难度划分为简易（330个）、中等（121个）与困难（31个）三个层级，并辅以数值化难度评分，便于研究者针对不同能力水平的模型进行精细化评测。每个任务均附带唯一标识符、来源仓库与拉取请求编号，保证了数据来源的透明性与可追溯性。任务类型聚焦于代码补全场景，体现了对实际应用需求的深刻洞察。

使用方法

该数据集旨在支持文本生成与代码生成模型在定理证明任务上的评估与微调。用户可通过HuggingFace的datasets库便捷加载数据，示例代码展示了如何快速迭代训练集任务。对每个任务，可结合problem_statement作为模型输入，以golden_patch作为参考输出，并使用verification_command自动化验证生成解的正确性。这种设计不仅简化了实验流程，也为人工智能在形式化证明领域的进步提供了标准化测试平台。

背景与挑战

背景概述

近年来，形式化验证在数学定理证明与软件可靠性领域日益受到重视，其中Lean 4作为新兴的交互式定理证明器，因其强大的表达能力和严谨的形式化基础，正逐步成为学术界与工业界验证复杂逻辑命题的核心工具。在此背景下，由Foundry AI团队开发的LeanBench数据集应运而生，该数据集于2024年创建，旨在系统评估人工智能系统在Lean 4定理证明任务中的性能。数据集包含482个真实提取自Lean 4代码库拉取请求的任务，涵盖“简单”、“中等”、“困难”三个难度等级，核心聚焦于检验AI在代码补全、补丁生成等关键环节的推理能力。作为首个面向Lean 4的标准化基准，LeanBench有力推动了形式化推理与自动编程交叉领域的研究进展，为衡量和优化大语言模型的数学证明能力提供了可靠参考。

当前挑战

LeanBench数据集所面临的挑战首先体现在其旨在解决的领域问题上：现存的大语言模型在自然语言生成任务上表现优异，但面对Lean 4这类高度符号化、强调严格逻辑链的定理证明任务时，往往难以把握形式化环境中的上下文约束和语法精确性，容易产生语法错误或逻辑断裂的补丁。此外，数据集构建过程中也遭遇了诸多困难：从真实拉取请求中提取483个任务需要对复杂代码库进行精准解析与筛选，确保每个任务的“golden_patch”唯一正确且可验证；噪声数据的剔除、难度评分的客观化以及验证命令的标准化，均对数据质量控制提出了严苛要求。同时，仅482条数据的规模限制了模型的泛化边界，且“硬”难度任务仅有31个，导致高复杂度场景的评估置信度不足，进一步加剧了基准的实用性与全面性之间的矛盾。

常用场景

经典使用场景

在人工智能与形式化验证的交叉领域中，LeanBench作为一项专为评估AI系统在Lean 4定理证明任务上性能而设计的基准数据集，其经典使用场景聚焦于衡量和比较各类模型在自动定理证明任务中的表现。研究人员通过将数据集中的482个任务——涵盖易、中、难三个等级，并且每个任务均包含自然语言描述的问题陈述、预期解决方案（以diff格式呈现）以及验证命令——输入至诸如大型语言模型或强化学习驱动的证明助手等AI系统中，进而系统性地评估其在自动化推理、代码生成与补全方面的能力。该数据集的标准化格式与离散难度分级使得跨模型、跨方法的横向对比成为可能，是为定理证明领域AI技术进步的可靠度量标尺。

解决学术问题

LeanBench问世的初衷在于撬动自动定理证明领域中一个长期悬而未决的学术难题：如何构建一个真实、可复现且具有区分度的评估框架来量度AI系统的形式化推理能力。在LeanBench出现之前，学术研究往往受限于评估标准不统一、任务规模过小或脱离实际代码库语境等问题，导致不同方法间的性能比较缺乏公允基础。本数据集通过从真实的Lean 4拉取请求中萃取任务，天然继承了开源项目开发中的实际挑战——包括代码补全、错误修复及证明策略构建等——从而使得评估结果更具生态效度。其等级化的难度评分进一步推动了对AI系统在不同推理复杂度下表现差异的精细分析，为理论探索中关于模型规模、训练数据构成与推理能力之间关联的假设提供了经验验证平台，引领自动定理证明的研究范式从碎片化迈向系统化。

衍生相关工作

自LeanBench公开以来，它作为权威基准引发了一系列衍生工作与纵深研究。在模型架构层面，部分研究者以其任务难度分层为切入点，探索专门针对定理证明的神经符号融合架构，例如结合图神经网络来编码证明状态的拓扑结构。在训练策略领域，围绕该数据集的难度评分分布，出现了针对课程学习（Curriculum Learning）的优化方法，旨在让模型先从简单题目学起，再逐步过渡至复杂证明。不仅如此，基于LeanBench的标准格式，学术界衍生了多模态提示模板与适应性反馈机制的探讨，试图通过赋予模型更多上下文信息（如相似旧题目的证明片段）来提升推理准确性。此外，若干开源社区发起了围绕LeanBench的竞赛与排行榜，促使了大型模型评测实验室发布专项报告，并激励了后续针对Autoformalization（自动形式化）与Proof Repair（证明修复）等子问题的专用数据集的构建，整体形成了一个良性发展的科研生态。