IneqMath

IneqMath是一个由专家精心策划的不等式问题数据集，包含200个由国际数学奥林匹克奖牌得主设计的测试问题和1252个来自高级教材的训练问题。每个训练问题都附有最多四个逐步解决方案，并且76.8%的训练问题被标注了与解决方案相关的83个定理。数据集采用非正式的语言，通过边界估计和关系预测两个子任务来评估不等式证明，旨在推动大型语言模型在不等式证明方面的能力。

IneqMath is a meticulously curated dataset of inequality problems developed by experts. It includes 200 test problems designed by International Mathematical Olympiad medalists and 1252 training problems sourced from advanced textbooks. Each training problem is accompanied by up to four step-by-step solutions, and 76.8% of the training problems are annotated with 83 theorems relevant to their solutions. The dataset uses informal language, and evaluates inequality proof capabilities through two subtasks: bound estimation and relationship prediction, aiming to advance the capacity of large language models (LLMs) in inequality proving.

搜集汇总

数据集介绍

构建方式

IneqMath数据集通过专家精心策划构建，包含1252个训练问题和200个测试问题。测试集由IMO级别奖牌得主设计，确保原创性和难度；训练问题源自高级教材，通过LLM重新表述并由专家审核。每个训练问题包含最多四个分步解决方案，76.8%的问题标注了相关定理。

特点

IneqMath是首个大规模非正式语言描述的奥数级别不等式数据集，其特点包括：1) 专家策划的训练和测试集；2) 丰富的分步解决方案和83个标注定理；3) 通过边界估计和关系预测两个可自动验证的子任务重新表述不等式证明问题。

使用方法

IneqMath数据集可用于评估LLM在不等式证明中的表现。使用时需：1) 将问题分为边界估计和关系预测两类；2) 采用提出的LLM-as-judge评估框架，包含最终答案判断器和四个分步判断器；3) 只有当解决方案通过所有五个判断器时才被视为完全正确。

背景与挑战

背景概述

IneqMath数据集由斯坦福大学和加州大学伯克利分校的研究团队于2025年创建，旨在解决数学不等式证明领域的关键挑战。该数据集聚焦于奥林匹克数学竞赛级别的不等式问题，包含1,252个训练问题和200个测试问题，每个问题都配有逐步解答和定理标注。核心研究问题在于探索大型语言模型在非正式但可验证的不等式证明任务中的表现，包括边界估计和关系预测两个子任务。IneqMath通过专家评审的问题设计和创新的LLM-as-judge评估框架，为数学推理领域提供了首个大规模、高质量的非正式不等式证明基准。

当前挑战

IneqMath面临的挑战主要体现在两个方面：领域问题的复杂性和数据集构建的严谨性。在领域问题方面，不等式证明要求模型具备发现紧边界、战略性地应用经典定理（如AM-GM不等式、柯西不等式）和精确符号变换的能力，这超越了常规数学问题求解的难度。在构建过程中，研究人员需要克服现有数据集稀缺、合成数据缺乏多样性、形式化表示与LLM非正式推理能力不匹配等挑战。特别是确保测试问题的原创性（由IMO奖牌得主设计）和评估框架的可靠性（结合最终答案和逐步推理的严格验证），这些都对数据集的构建提出了极高要求。

常用场景

经典使用场景

IneqMath数据集专为评估大型语言模型在不等式证明任务中的推理能力而设计。其经典使用场景包括数学奥林匹克竞赛级别的不等式问题求解，特别是在需要发现紧界和策略性应用经典定理（如AM-GM不等式、柯西-施瓦茨不等式等）的复杂推理任务中。该数据集通过将不等式证明问题重新表述为两个可自动验证的子任务——界估计和关系预测，为模型提供了结构化的挑战。

解决学术问题

IneqMath解决了数学推理领域中的几个关键学术问题：首先，它填补了现有数据集中不等式问题稀缺的空白，这些数据集往往过于形式化或规模不足；其次，它提供了一种非正式但可验证的任务表述，使得模型能够在接近人类直觉的推理模式下工作，同时避免了形式证明助手的严格语法要求；最后，通过引入细粒度的评估框架，该数据集揭示了当前语言模型在构建严格数学证明时的显著缺陷，即模型可能在找到正确答案的同时缺乏合理的逐步推理。

衍生相关工作

IneqMath的发布促进了多项相关研究工作的开展，特别是在定理引导推理和自我改进方法方面。基于该数据集，研究者们探索了如何通过检索增强生成（RAG）技术为模型提供相关定理提示，以及如何通过自我批判机制改进模型的推理过程。此外，该数据集还激发了对LLM作为评估者的进一步研究，特别是在开发更精细的步骤级评判标准以检测推理中的常见缺陷方面。这些衍生工作共同推动了对大型语言模型数学推理能力的深入理解和改进。