1. GSM8K
https://huggingface.co/datasets/openai/gsm8k
{'question': 'Natalia sold clips to 48 of her friends in April, and then she sold half as many clips in May. How many clips did Natalia sell altogether in April and May?','answer': 'Natalia sold 48/2 = <<48/2=24>>24 clips in May.\nNatalia sold 48+24 = <<48+24=72>>72 clips altogether in April and May.\n#### 72',}
GSM8K数据集为大模型数学能力评测常见的benchmark之一。GSM8K数据集是一个包含8.5K高质量、语言多样性丰富的中小学数学应用题数据集，其量级特点在于提供了大量的题目，每题都配有自然语言的解题答案。这个数据集的应用主要在于支持对当前模型的推理缺陷进行诊断，并帮助推动相关研究的进展。通过GSM8K，研究者们能够测试和提升模型在多步骤数学推理任务中的性能，尤其是在面对需要复杂推理的场景时，GSM8K能够作为一个有效的基准来评估和改进模型的表现。
2. MATH
https://github.com/hendrycks/math
{"problem": "Let $\\mathbf{a}$ and $\\mathbf{b}$ be vectors such that\n\\[\\mathbf{v} = \\operatorname{proj}_{\\mathbf{a}} \\mathbf{v} + \\operatorname{proj}_{\\mathbf{b}} \\mathbf{v}\\]for all vectors $\\mathbf{v}.$ Enter all possible values of $\\mathbf{a} \\cdot \\mathbf{b},$ separated by commas.","level": "Level 4","type": "Precalculus","solution": "Taking $\\mathbf{v} = \\mathbf{b},$ we get\n\\[\\mathbf{b} = \\operatorname{proj}_{\\mathbf{a}} \\mathbf{b} + \\operatorname{proj}_{\\mathbf{b}} \\mathbf{b}.\\]From the projection formula,\n\\[\\operatorname{proj}_{\\mathbf{a}} \\mathbf{b} = \\frac{\\mathbf{a} \\cdot \\mathbf{b}}{\\|\\mathbf{a}\\|^2} \\mathbf{a},\\]and $\\operatorname{proj}_{\\mathbf{b}} \\mathbf{b} = \\mathbf{b},$ so\n\\[\\mathbf{b} = \\frac{\\mathbf{a} \\cdot \\mathbf{b}}{\\|\\mathbf{a}\\|^2} \\mathbf{a} + \\mathbf{b}.\\]Hence,\n\\[\\frac{\\mathbf{a} \\cdot \\mathbf{b}}{\\|\\mathbf{a}\\|^2} \\mathbf{a} = \\mathbf{0}.\\]The vector $\\mathbf{a}$ must be nonzero, in order for the projection of $\\mathbf{v}$ onto $\\mathbf{a}$ to be defined, so we must have $\\mathbf{a} \\cdot \\mathbf{b} = \\boxed{0}.$\n\nNote that we can take $\\mathbf{a} = \\begin{pmatrix} 1 \\\\ 0 \\end{pmatrix}$ and $\\mathbf{b} = \\begin{pmatrix} 0 \\\\ 1 \\end{pmatrix}.$"}
MATH数据集由12,500道复杂数学竞赛题目组成，涵盖代数、几何、概率和数论等多个数学分支。该数据集的显著特点是每一道题目都提供了详尽的解题步骤，这使得它不仅能够测试机器学习模型找寻最终答案的能力，还能评估它们生成解题逻辑和推理过程的能力。由于题目难度与数学竞赛水平相匹配，因此这个数据集极具挑战性，适合用于提升和验证高级数学问题解决技术。此外，数据集中的解题步骤为自动化评估和模型训练提供了丰富的信息资源，有助于机器学习算法在数学领域的进一步发展。
3. Orca-Math-200K
https://huggingface.co/datasets/microsoft/orca-math-word-problems-200k
{"question":"A is 3 groups of 10 and 7 individual units, and B is the number obtained by subtracting 1 from 40. Which is smaller, A or B?","answer":"Let's calculate the value of A and B. A is 3 groups of 10 and 7 individual units. So, A = (3 * 10) + 7 = 30 + 7 = 37. B is the number obtained by subtracting 1 from 40. So, B = 40 - 1 = 39. Now, we compare A and B. A = 37 B = 39 Since 37 is less than 39, A is smaller than B."}
Orca-Math-200K数据集是一个大型的合成数学问题集，包含20万个数学文字题目。这个数据集主要应用于训练和评估语言模型在数学问题解决方面的能力。通过使用一个多代理的设置，这个数据集能够提供一系列从易到难的多样化数学题目，以挑战并提升模型的推理和解题技巧。数据集的生成方式涉及初始种子问题的收集，利用代理之间协作的方式来重新表述和创造新的问题，从而丰富问题集的多样性和难度。这一过程不仅提高了数据集的质量，也为模型的训练提供了更多可能性和灵活性，有助于在保证数据新鲜度和多样性的同时，有效提升模型在数学领域的性能。
4. NaturalProofs
https://github.com/wellecks/naturalproofs
{"id": 30777,"type": "definition","label": "Definition:Folium of Descartes/Cartesian Form","title": "Definition:Folium of Descartes/Cartesian Form","categories": ["Definitions/Folium of Descartes"],"contents": ["The '''folium of Descartes''' is the [[Definition:Locus|locus]] of the [[Definition:Equation of Geometric Figure|equation]]:",":$x^3 + y^3 - 3 a x y = 0$"],"refs": ["Definition:Locus","Definition:Equation of Geometric Figure"],"ref_ids": [22165,25822],"proofs": []},
NaturalProofs从基础计算和应用问题转向了更加抽象和理论化的数学证明领域。NaturalProofs是一个大规模的形式化数学证明数据集，由32k个定理陈述和证明，14k个定义和2k个其他类型的页面（例如公理，推论）组成，这些页面来自三个领域：ProofWiki，一个由贡献者社区撰写的在线数学证明汇编；Stacks项目，一个基于网络的代数、几何教材；以及来自数学教材的数据。NaturalProofs的出现为研究人工智能在高级数学推理和证明生成方面的能力提供了宝贵的资源，它不仅挑战了大模型的逻辑推理能力，还考验了模型理解和生成人类可读的数学证明的能力。这个数据集的规模和质量使它成为了评估和改进大模型在高级数学领域表现的重要benchmark。
5. LeanDojo
https://github.com/lean-dojo/LeanDojo
LeanDojo是一个专为学习型定理证明器设计的资源，它从Lean编程语言的数学库中提取了大量训练数据。这个数据集包含了98,734个定理及其证明，以及130,262个前提的定义，使得它成为定理证明领域内规模最大的数据集之一。定理证明是机器学习在形式化数学和验证领域的一个核心任务，而LeanDojo数据集的构建旨在提供一个丰富的资源，以训练和评估自动化定理证明系统。
LeanDojo数据集的构建过程采用了程序分析技术，确保了数据的质量和相关性，特别是在前提选择方面，这是定理证明中的一个关键瓶颈。通过提供精细标注的证明前提，该数据集能够支持前提选择的训练和评估。此外，LeanDojo数据集还引入了一个新颖的split策略，即novel_premises split，这种策略要求测试集中的证明必须使用至少一个未在训练集中使用过的前提，这有助于防止模型过度依赖记忆训练数据，从而使模型具有更健壮的泛化能力。
LeanDojo不仅是一个数据集，它还是一个完整的开放源代码平台，提供了一套工具、模型和基准，以促进学术社区在大型语言模型（LLMs）辅助的定理证明领域的研究。通过开放代码和模型，LeanDojo旨在降低机器学习在定理证明研究中的门槛，为未来的研究提供可复现的基准和强有力的基础。
6. NuminaMath
https://huggingface.co/datasets/AI-MO/NuminaMath-CoT
{"source":"synthetic_math","problem":" Consider the terms of an arithmetic sequence: $-\frac{1}{3}, y+2, 4y, \ldots$. Solve for $y$.","solution":"For an arithmetic sequence, the difference between consecutive terms must be equal. Therefore, we can set up the following equations based on the sequence given: \[ (y + 2) - \left(-\frac{1}{3}\right) = 4y - (y+2) \] Simplify and solve these equations: \[ y + 2 + \frac{1}{3} = 4y - y - 2 \] \[ y + \frac{7}{3} = 3y - 2 \] \[ \frac{7}{3} + 2 = 3y - y \] \[ \frac{13}{3} = 2y \] \[ y = \frac{13}{6} \] Thus, the value of $y$ that satisfies the given arithmetic sequence is $\boxed{\frac{13}{6}}$.","messages":[ { "content": "Consider the terms of an arithmetic sequence: $-\\frac{1}{3}, y+2, 4y, \\ldots$. Solve for $y$.", "role": "user" }, { "content": "For an arithmetic sequence, the difference between consecutive terms must be equal. Therefore, we can set up the following equations based on the sequence given:\n\\[ (y + 2) - \\left(-\\frac{1}{3}\\right) = 4y - (y+2) \\]\n\nSimplify and solve these equations:\n\\[ y + 2 + \\frac{1}{3} = 4y - y - 2 \\]\n\\[ y + \\frac{7}{3} = 3y - 2 \\]\n\\[ \\frac{7}{3} + 2 = 3y - y \\]\n\\[ \\frac{13}{3} = 2y \\]\n\\[ y = \\frac{13}{6} \\]\n\nThus, the value of $y$ that satisfies the given arithmetic sequence is $\\boxed{\\frac{13}{6}}$.", "role": "assistant" } ]}
NuminaMath数据集是一项开创性的工作，它汇聚了来自各种数学竞赛、论坛和教育资源的86万个问题和解决方案对，以推进人工智能在数学领域的能力。这个数据集的构建过程涉及广泛的来源，包括MATH、GSM8K、AMC、AIME等，以及应用了OCR、翻译、细化和CoT格式化等技术。NuminaMath数据集不仅规模庞大，而且通过其精心设计的CoT格式，支持链式思维推理，这对于训练大型语言模型（如GPT-4）以解决复杂数学问题至关重要。该数据集的成功应用体现在它对赢得AIMO Progress Prize的模型的精细调优上，证明了其在提升AI数学推理能力方面的有效性。NuminaMath数据集的创建和利用，标志着人工智能在数学教育和技术挑战中迈出了重要的一步。
7. DART-Math
https://github.com/hkust-nlp/dart-math
{"query":"Let \[f(x) = \left\{ \begin{array}{cl} ax+3, &\text{ if }x>2, \\ x-5 &\text{ if } -2 \le x \le 2, \\ 2x-b &\text{ if } x <-2. \end{array} \right.\]Find $a+b$ if the piecewise function is continuous (which means that its graph can be drawn without lifting your pencil from the paper).","response":"For the function to be continuous, the parts of the piecewise function must meet at $x = 2$ and at $x = -2$. This means that at $x = 2$, $ax + 3 = x - 5$ and at $x = -2$, $x - 5 = 2x - b$. From $ax + 3 = x - 5$, we get $ax - x = -8$, so $(a-1)x = -8$, and $x = 2$ to get $(a-1)2 = -8$. Solving $(a-1)2 = -8$ for $a$ gives us $2a - 2 = -8$, so $2a = -6$, and $a = -3$. From $x - 5 = 2x - b$, we get $-5 - 2x = -b$, or $-5 - 2(-2) = -b$, $since x = -2$. Thus, $-1 = -b$, so $b = 1$. The problem asks for $a + b$, so $-3 + 1 = -2$. The answer is: $2$ $-2$"}
DART-Math数据集是一个专为提升大型语言模型在数学问题解决领域的能力而设计的合成数据集。该数据集通过Difficulty-Aware Rejection Tuning （DART）方法生成，这种方法特别注重难题，为这些难题分配了更多的生成尝试次数，从而确保在困难的数学问题上获得更多的训练样本。DART-Math数据集的规模约为59万条例子，远小于以往的数据集，但其设计和生成策略大幅提升了模型对难题的应对能力。数据集的创建过程中仅使用了7B参数的开源模型DeepSeekMath-7B-RL，而不依赖于参数规模更大的专属模型，如GPT-4。通过对从7B到70B参数的不同基模型进行微调，结果产出了一系列名为DART-Math的模型。这些模型在包括MATH、GSM8K等在内的六个数学基准测试中，显著优于传统拒绝微调方法，甚至在一些测试中超越了当前最先进的技术，尽管使用的是更小规模的数据集和非专属模型。因此，DART-Math数据集被证明是提高数学问题解决能力的极有效且成本效益高的公开资源。
8. DeepSeekMath
DeepSeekMath数据集生成过程
数据源头：数据集的构建始于Common Crawl项目，这是一个包含互联网页面副本的数据集，每月更新一次。利用这个庞大的数据源，可以获取大量潜在的数学相关内容。 初筛过程：为了筛选出与数学相关的内容，研究团队首先从OpenWebMath构建了一个种子数据集。他们利用这个种子数据集训练了一个fastText模型，用于识别和检索更多数学相关的网页。 分类与筛选：将训练好的fastText模型应用于Common Crawl数据集，对页面进行分类和筛选，仅保留与数学相关的页面。这个过程包括多次迭代，以确保模型能够不断从Common Crawl中识别出更多的数学内容。 数据集规模：经过多次迭代，最终收集到了3550万个数学相关的网页，总计包含1200亿个数学相关的令牌（tokens）。这个庞大的数据集是为语言模型进一步训练准备的原材料。 数据去重与筛查：为了确保数据的质量，原始数据会经过去重处理。同时，为了避免训练数据与测试集或验证集的数据污染，会对数据进行筛查，排除那些与评估基准匹配的页面。 迭代优化：在整个数据集构建过程中，研究团队不断迭代和优化数据筛选模型，确保数据集的多样性、覆盖范围和质量。最终生成的DeepSeekMath数据集具有高度的数学相关性，能够为语言模型提供丰富的数学推理训练材料。
9. AlphaProof
Google的DeepMind团队发布了AlphaProof的技术分享，AlphaProof和AlphaGeometry一起解出了今年IMO试题中的4题，相当于银牌的成绩。
AlphaProof强化学习训练循环流程图
生成训练AlphaProof模型的数据集流程始于使用预训练的Gemini语言模型作为基础。这个模型经过微调，能够将自然语言描述的数学问题自动转换为Lean形式化语言的陈述，从而创建了一个包含不同难度水平的大型形式化数学问题库。AlphaProof系统随后对这些问题生成解决方案候选，并在Lean中搜索可能的证明步骤来证明或反驳这些候选解。每个被发现并验证的证明都用于强化AlphaProof的语言模型，提高其解决更具挑战性问题的能力。在IMO比赛前的几周内，AlphaProof通过证明或反驳数百万个涵盖广泛难度和数学主题的问题进行大规模训练。更重要的是，这个训练过程在比赛期间仍在持续，通过证明自生成的比赛问题变体来不断强化模型，直到找到完整的解决方案。这个流程巧妙地结合了自然语言处理、形式化数学推理和强化学习，创建了一个能够持续自我提升的数学问题求解系统。
整数智能信息技术（杭州）有限责任公司，起源自浙江大学计算机创新技术研究院，致力于成为AI行业的数据领航员。整数智能也是中国人工智能产业发展联盟、ASAM协会、浙江省人工智能产业技术联盟成员，其提供的智能数据工程平台（MooreData Platform）与数据集构建服务（ACE Service），满足了智能驾驶、AIGC等数十个人工智能应用场景对于先进的智能标注工具以及高质量数据的需求。
目前公司已合作海内外顶级科技公司与科研机构客户1000余家，拥有知识产权数十项，通过ISO9001、ISO27001等国际认证，也多次参与人工智能领域的标准与白皮书撰写，也受到《CCTV财经频道》《新锐杭商》《浙江卫视》《苏州卫视》等多家新闻媒体报道。
