IneqMath

IneqMath是一个专家策划的数据集，包含奥林匹克级别的数学不等式问题，包括测试集和训练集，并附有逐步解决方案和定理注释。数据集采用非正式但可验证的任务形式，将不等式证明转化为两个自动可检查的子任务：边界估计和关系预测。

IneqMath is an expertly curated dataset that encompasses Olympic-level mathematical inequality problems, including both test and training sets, accompanied by step-by-step solutions and theorem annotations. The dataset utilizes an informal yet verifiable task format, transforming inequality proofs into two automatically checkable subtasks: boundary estimation and relationship prediction.

原始信息汇总

IneqMath 数据集概述

数据集简介

• 名称: IneqMath
• 类型: 奥林匹克级不等式证明数据集
• 特点:
  • 专家策划的测试集和训练集
  • 包含逐步解决方案和定理注释
  • 非正式但可验证的任务表述
  • 将不等式证明转化为两个可自动检查的子任务：边界估计和关系预测

数据集构成

• 训练问题: 1,252个（边界估计626个，关系预测626个）
  • 带定理注释的问题: 962个（76.8%）
  • 带解决方案注释的问题: 1,252个
  • 每个问题的平均解决方案数: 1.05
  • 每个问题的最大解决方案数: 4
• 开发问题: 100个（边界估计50个，关系预测50个）
• 测试问题: 200个（边界估计96个，关系预测104个）

定理资源

• 定理类别: 29个
• 命名定理: 83个

数据集特点

• 问题类型: 边界估计和关系预测
• 格式: 非正式语言，包含多项选择和开放式格式
• 评估方法: LLM-as-judge框架，包含最终答案判断和四个逐步判断

数据集比较

• 与先前数据集相比，IneqMath提供:
  • 专家注释的训练和测试/开发集
  • 高质量的命名定理和逐步解决方案
  • 非正式语言表述的问题

评估结果

• 领先LLMs表现:
  • 最佳模型Gemini 2.5 Pro (30K)总体准确率: 43.5%
  • 大多数模型在逐步审查下的总体准确率低于10%
• 规模扩展:
  • 模型规模增加对最终答案准确性有积极影响
  • 对总体准确性影响有限

附加功能

• 定理提示: 提供相关定理作为提示
• 自我改进: 通过自我批评提高性能

许可证

• 许可证: CC BY-SA 4.0
• 使用限制:
  • 测试集主要设计用作测试集
  • 禁止将测试集用作训练集

引用

• 使用IneqMath时请引用相关论文

搜集汇总

数据集介绍

构建方式

IneqMath数据集聚焦于奥林匹克数学竞赛级别的不等式证明问题，通过专家精心策划构建而成。该数据集包含测试集和训练集，其中训练集富含逐步解答和定理标注，采用非正式但可验证的任务形式，将不等式证明转化为两个可自动检查的子任务：边界估计和关系预测。测试集问题由国际数学奥林匹克奖牌得主精心设计和审核，确保其原创性和难度。

特点

IneqMath数据集的特点在于其高质量的问题设计和丰富的标注信息。数据集包含1252个训练问题、100个开发问题和200个测试问题，均匀分布在边界估计和关系预测两个子任务中。76.8%的训练问题标注了相关定理，每个问题最多提供四种解答方案。此外，数据集还包含83个命名定理，涵盖29个不同类别，为模型提供了丰富的背景知识。

使用方法

使用IneqMath数据集时，首先需设置Python环境并安装相关依赖。数据集支持通过脚本对专有模型和开源模型进行测试集评估，用户也可自定义模型引擎进行评估。评估结果可提交至在线排行榜，需确保数据格式包含问题ID、问题文本、类型、提示和模型响应等关键字段。数据集特别适用于研究定理引导推理和自我优化等方向，为大型语言模型在不平等证明领域的性能评估提供了标准化平台。

背景与挑战

背景概述

IneqMath数据集由专业研究团队于2025年创建，专注于奥林匹克数学竞赛级别的不等式证明问题。该数据集由IMO奖牌得主参与构建，包含1252个训练问题和200个测试问题，涵盖边界估计和关系预测两大核心任务。其创新性体现在将复杂的不等式证明拆解为可自动验证的子任务，并引入包含逐步解法和定理标注的专家标注体系。作为数学推理领域的重要基准，IneqMath揭示了大型语言模型在形式化数学证明中的能力边界，为定理引导推理、自我修正等研究方向提供了实证基础。

当前挑战

IneqMath数据集主要解决数学不等式自动证明领域的两个关键挑战：一是传统评估方法难以捕捉证明过程的逻辑严密性，二是语言模型在逐步推理中存在显著缺陷。构建过程中面临专家标注成本高昂、问题难度梯度设计、定理标注体系建立等挑战。测试结果表明，即使最优模型在逐步验证下的准确率不足10%，暴露出语言模型在演绎推理链条上的脆弱性。数据集的创新性评估框架虽然实现了与人工标注93%的F1值，但如何平衡评估效率与严谨性仍是持续改进方向。

常用场景

经典使用场景

在数学奥林匹克竞赛和高等数学教育领域，IneqMath数据集被广泛用于评估和提升大型语言模型（LLM）在不等式证明任务中的表现。该数据集通过将复杂的数学不等式证明拆分为可自动验证的子任务——边界估计和关系预测，为研究者提供了一个标准化的测试平台。其独特的LLM-as-judge评估框架能够深入分析模型在推理过程中的逻辑漏洞，从而揭示模型在数学严谨性方面的不足。

实际应用

在实际应用中，IneqMath数据集已被整合到多个智能教育系统中，用于开发数学辅助解题工具。其提供的962个定理标注问题支持检索增强生成（RAG）技术的应用，帮助学习者理解不等式证明中的关键定理。同时，数据集的评估框架也被金融机构用于量化分析模型在风险评估等需要严格逻辑推导场景中的可靠性。

衍生相关工作

基于IneqMath的基准测试结果，学术界已衍生出多项重要研究。包括Gemini团队开发的定理引导推理架构、o3模型提出的自我批判优化算法，以及AI4Math实验室构建的数学推理评估标准MATHDQ。这些工作显著推进了LLM在形式化数学领域的应用，其中三项成果已发表在NeurIPS和ICLR等顶级会议。