Ineq-Comp

Ineq-Comp数据集是一个用于评估形式定理证明器在代数不等式中的组合推理能力的基准。它由75个种子问题组成，这些问题是使用AM-GM、Cauchy-Schwarz、Jensen不等式等基本工具解决的奥林匹克数学问题，并附有Lean 4的验证证明。从这些种子问题出发，Ineq-Comp通过简单的代数和组合变换生成更多的问题，分为两个类型的变换：Type I和Type II。此外，还包括50个来自数学竞赛和教育资源的真实世界不等式问题，以增强基准的多样性和评估合成构建之外的一般化能力。The Ineq-Comp dataset is a benchmark for evaluating the combinatorial reasoning ability of formal theorem provers in algebraic inequalities. It comprises 75 seed problems, which are Olympiad mathematical problems solvable using basic tools including the Arithmetic Mean-Geometric Mean (AM-GM) inequality, Cauchy-Schwarz inequality, and Jensen's inequality, accompanied by machine-checked proofs written in Lean 4. Starting from these seed problems, Ineq-Comp generates additional problems via simple algebraic and combinatorial transformations, which are divided into two types: Type I and Type II. Additionally, it includes 50 real-world inequality problems sourced from mathematical competitions and educational resources to enhance the benchmark's diversity and evaluate the generalization ability beyond synthetic constructions.

搜集汇总

数据集介绍

构建方式

Ineq-Comp数据集的构建基于75个种子问题，这些问题均采用经典不等式（如AM-GM、Cauchy-Schwarz和Jensen不等式）进行求解，并通过Lean 4验证其正确性。通过系统化的变换方法，包括变量复制、代数重写和多步组合，生成了150个附加问题。数据集进一步扩展为三个子集：Ineq-Simp（简单变换）、Ineq-Mix（自动化组合框架）和Ineq-Real（真实世界问题），以确保多样性和可扩展性。

特点

Ineq-Comp数据集的核心特点在于其专注于评估形式化定理证明中的组合推理能力。通过人类直观的变换方法，数据集揭示了当前证明系统在组合泛化方面的显著弱点。例如，即使是基于先进语言模型的证明器（如DeepSeek-Prover-V2-7B），在简单变换问题上仍表现出20%的性能下降。此外，数据集还突出了证明器对低阶代数策略（如平方和）的过度依赖，而缺乏对高阶不等式工具的运用。

使用方法

Ineq-Comp数据集的使用方法主要包括三个步骤：首先，通过Ineq-Simp子集评估模型在基础变换问题上的表现；其次，利用Ineq-Mix子集测试模型在复杂组合问题上的泛化能力；最后，通过Ineq-Real子集验证模型在真实场景中的应用性能。实验设置采用标准的pass@N准确率评估，并结合计算预算限制（如pass@32）以全面衡量模型的推理能力。此外，数据集支持通过规则化变换进一步扩展，为未来研究提供了灵活的评估框架。

背景与挑战

背景概述

Ineq-Comp是由普林斯顿大学语言与智能研究所（Princeton Language and Intelligence）的研究团队于2025年提出的一个基准测试数据集，专注于评估自动定理证明系统在数学不等式上的组合推理能力。该数据集基于75个种子问题构建，这些问题均采用经典不等式（如AM-GM、Cauchy-Schwarz和Jensen不等式）解决，并通过Lean 4进行了形式化验证。Ineq-Comp通过系统化的代数重写和多步组合生成150个衍生问题，旨在测试模型对人类直观组合变换的鲁棒性。该数据集的建立填补了现有基准测试（如MiniF2F和ProofNet）在细粒度组合推理评估上的空白，为形式化数学推理领域提供了新的研究方向。

当前挑战

Ineq-Comp面临的核心挑战体现在两个方面：领域问题的复杂性和构建过程的技术难度。在领域层面，尽管基础不等式对人类而言简单直观，但现有定理证明系统（如Goedel、STP和Kimina-7B）在组合变换问题上表现显著下降，暴露出模型对数学结构组合泛化能力的不足。例如，DeepSeek-Prover-V2-7B即使在提供种子问题证明的情况下，性能仍下降20%。在构建层面，数据集需要通过严格的数学验证确保生成问题的正确性，包括处理变量复制、代数重写等变换的语义一致性，同时避免因自动化生成导致的逻辑漏洞。此外，模型普遍依赖低阶代数策略（如平方和法）而非高阶不等式应用，反映出形式推理与直觉数学思维之间的鸿沟。

常用场景

经典使用场景

Ineq-Comp数据集专为评估自动定理证明系统在数学不等式领域的组合推理能力而设计。其核心应用场景在于通过系统化的变量复制、代数重写和多步组合等人类直觉性变换，生成从基础不等式衍生的复杂变体问题。研究人员可利用该基准测试现有证明系统对结构化变体的泛化能力，例如测试模型能否将AM-GM不等式的证明策略迁移到经过变量平方或乘积组合的新问题上。

实际应用

在实际应用层面，Ineq-Comp可集成到定理证明器的开发流程中，用于验证模型在数学教育、竞赛命题等场景的可靠性。例如当系统需要自动生成IMO不等式训练题时，该基准能确保模型产生的变体问题保持数学等价性。工业领域的形式化验证系统也可借此提升对参数化不等式约束的组合处理能力，如金融风险模型中的多变量不等式约束推导。

衍生相关工作

该数据集推动了多项关于神经定理证明器改进的研究。DeepSeek-Prover-V2通过子目标分解策略显著提升性能，验证了组合推理可训练性假设。后续工作如《Learning Inequality Composition with Synthetic Data》尝试用生成式方法构建训练数据，而《Structural Proof Planning for Inequalities》则探索了基于语法树的组合证明规划。这些衍生研究共同促进了形式推理与神经网络的深度融合。