ConstructiveBench

该数据集名为ConstructiveBench，包含了3,431个来自知名数学竞赛的答案构建问题，这些问题都经过了Lean形式化验证。数据集不仅包括非正式和正式的问题陈述、正确答案、Lean形式定理、非正式解答，还包含了诸如领域、来源和难度等元数据。为了解决潜在的数据污染问题，数据集中特别包含了一个由92个问题组成的测试子集。该数据集的任务涵盖了数学问题中的答案构建和定理证明。This dataset, named ConstructiveBench, contains 3,431 answer construction problems sourced from well-known mathematics competitions, all of which have been formally verified using Lean. In addition to informal and formal problem statements, correct answers, Lean-formalized theorems, and informal solutions, the dataset also includes metadata such as domain, source, and difficulty level. To address potential data contamination issues, the dataset specifically includes a test subset consisting of 92 problems. The tasks covered by this dataset span answer construction and theorem proving for mathematical problems.

搜集汇总

背景与挑战

背景概述

ConstructiveBench是一个包含3,431个竞赛级别答案构建问题的自动形式化数据集，每个问题包括非正式和正式的问题陈述、真实答案和元数据。该数据集专注于支持端到端的形式验证，旨在解决数学推理中答案生成和形式验证的集成挑战。