ConstructiveBench

ConstructiveBench数据集是一个包含经过精选的奥赛风格数学问题的数据集，每个问题都包含元数据和与Lean 4对应的格式化答案。数据集的问题是来自各种数学竞赛的，例如IMO 2011，并按照数学类别（如代数、组合学）进行分类。每个条目都包括问题陈述、答案、格式化答案、完整定理以及与答案构建对齐的部分。

原始信息汇总

ConstructiveBench 数据集概述

基本信息

• 创建方式：专家生成
• 语言：英语
• 许可证：MIT
• 多语言支持：单语言
• 数据集规模：1K<n<10K
• 数据来源：原创
• 任务类别：问答系统
• 任务ID：开放域问答
• 标签：数学

数据集描述

ConstructiveBench 数据集是为论文《Enumerate–Conjecture–Prove (ECP)》开发的，旨在使用 Lean 4 对数学竞赛中的答案构建问题进行自动化推理系统的基准测试。

数据内容

数据集文件 constructivebench.json 包含以下内容的奥林匹克风格数学问题：

• 问题陈述
• 类别（如代数、组合数学）
• 来源（如 IMO 2011）
• Lean 4 中的形式化答案
• 完整的形式化定理
• 答案构建对齐部分（标题、答案、定理及不含答案的定理）

示例条目

json { "name": "IMO2011SLC4", "category": "Combinatorics", "source": "IMO/2011", "problem": "...", "answer": "The greatest such number k is 3", "formalization": "...", "is_formalized": true }

相关资源

• 源代码仓库：Complete codebase and benchmarks

搜集汇总

数据集介绍

构建方式

在数学竞赛自动推理系统研究领域，ConstructiveBench数据集通过专家生成方式精心构建。该数据集源自国际数学奥林匹克竞赛等权威赛事的典型题目，采用Lean 4形式化验证语言对每道题目进行严格的形式化编码。构建过程中，研究人员不仅收录原始题目陈述，还系统性地标注了题目类别、来源等元数据，并完成从自然语言描述到形式化定理的完整映射，确保每个条目包含问题陈述、参考答案及形式化定理等多个维度的信息。

特点

作为数学竞赛领域的形式化基准测试集，ConstructiveBench最显著的特点是同时涵盖自然语言问题和形式化验证内容。数据集包含代数、组合数学等多个数学分支的竞赛题目，每道题目均配有精确的Lean 4形式化表述，并特别标注了答案构造的对应部分。这种双重表征方式既保留了数学问题的原始表述，又提供了机器可验证的形式化规范，为研究数学自动推理系统如何理解并构造复杂数学答案提供了独特的研究素材。

使用方法

该数据集主要服务于数学自动推理系统的开发与评估，研究人员可通过解析JSON格式的数据文件获取结构化信息。典型使用场景包括：基于问题陈述训练模型生成形式化答案，利用形式化定理验证系统推理的正确性，或者通过答案构造对齐部分研究自动推理的中间过程。数据集配套的ECP框架为系统性能评估提供了标准化流程，用户可参照源仓库提供的基准测试方案，将系统输出与数据集中的形式化答案进行对比验证。

背景与挑战

背景概述

ConstructiveBench数据集由JackSun200312团队于2023年发布，作为《Enumerate–Conjecture–Prove》研究论文的核心组成部分。该数据集专注于数学竞赛领域的答案构建问题，旨在推动自动推理系统在形式化数学证明方面的发展。数据集收录了经过专家精心筛选的奥林匹克风格数学问题，涵盖代数、组合数学等多个子领域，每道题目均配有完整的Lean 4形式化描述。其创新性体现在将传统数学问题转化为可计算的形式化证明任务，为数学自动推理领域提供了首个专注于答案构造过程的基准测试平台。

当前挑战

该数据集面临双重技术挑战：在领域问题层面，数学竞赛答案构建需要系统同时具备枚举可能性、提出合理猜想和完成严格证明的能力，这种复合推理要求远超传统单步推理任务；在构建过程中，团队需要克服形式化数学表达与自然语言问题描述之间的语义鸿沟，确保每道题目的Lean 4编码能准确反映原始问题的数学内涵。数据集中包含的答案构造对齐部分（header/answer/theorem等）的精细标注，对标注人员的数学专业素养和形式化验证能力提出了极高要求。

常用场景

经典使用场景

在数学自动推理领域，ConstructiveBench数据集为研究者提供了标准化的测试平台，专门用于评估系统在解决奥林匹克数学竞赛风格问题时的表现。通过精心设计的数学问题和对应的Lean 4形式化答案，该数据集能够系统地衡量算法在枚举、猜想和证明过程中的准确性和效率。

实际应用

在实际应用中，ConstructiveBench数据集可广泛应用于智能教育系统的开发，特别是针对高阶数学问题求解的辅助工具。教育科技公司可利用该数据集训练AI系统，帮助学生理解复杂的数学证明过程。同时，该数据集也为数学竞赛培训提供了标准化的练习材料，提升了培训效率和质量。

衍生相关工作

基于ConstructiveBench数据集，研究者们已经开展了多项重要工作。Enumerate–Conjecture–Prove (ECP)框架是该数据集最直接的衍生成果，为数学问题的自动求解提供了系统的方法论。此外，该数据集还启发了多个基于深度学习的数学推理模型，推动了形式化数学与人工智能的交叉研究。