用大语言模型解决不等式证明
Solving Inequality Proofs with Large Language Models
AI总结：
本文提出了一种非正式但可验证的任务公式化方法，通过IneqMath数据集和LLM-as-judge评估框架，揭示了大语言模型在解决不等式证明任务中的局限性及改进方向。
摘要：
不等式证明在众多科学和数学领域中至关重要，它测试了发现紧界和战略定理应用等高级推理技能。这使得它成为大语言模型（LLMs）的一个独特且具有挑战性的前沿领域，提供了超越一般数学问题解决的见解。在这一领域的发展受到现有数据集的阻碍，这些数据集通常稀缺、合成或形式化严格。我们通过提出一个非正式但可验证的任务公式化方法来解决这个问题，将不等式证明重新表述为两个可以自动验证的子任务：界估计和关系预测。基于此，我们发布了IneqMath，一个由专家整理的竞赛级不等式数据集，包括测试集和训练语料库，后者补充了分步解决方案和定理注释。我们还开发了一个新的LLM-as-judge评估框架，结合一个最终答案判断者和四个分步判断者，用于检测常见的推理错误。对29个领先的LLM在IneqMath上的系统评估揭示了一个令人惊讶的现实：即使像o1这样的顶级模型在分步检验下整体准确率也低于10%；这比仅考虑最终答案等价性的准确性下降了高达65.5%。这种差异暴露了脆弱的推理链条和当前LLM在仅仅找到答案与构建严谨证明之间的关键差距。扩大模型大小和增加测试时计算量在整体证明正确性上获得有限的提升。相反，我们的发现突显了有前途的研究方向，如定理引导推理和自我完善。代码和数据可在https://ineqmath.github.io/上获得。
英文摘要：
Inequality proving, crucial across diverse scientific and mathematical fields, tests advanced reasoning skills such as discovering tight bounds and strategic theorem application. This makes it a distinct, demanding frontier for large language models (LLMs), offering insights beyond general mathematical problem-solving. Progress in this area is hampered by existing datasets that are often scarce, synthetic, or rigidly formal. We address this by proposing an informal yet verifiable task formulation, recasting inequality proving into two automatically checkable subtasks: bound estimation and relation prediction. Building on this, we release IneqMath, an expert-curated dataset of Olympiad-level inequalities, including a test set and training corpus enriched with step-wise solutions and theorem annotations. We also develop a novel LLM-as-judge evaluation framework, combining a final-answer judge with four step-wise judges designed to detect common reasoning flaws. A systematic evaluation of 29 leading LLMs on IneqMath reveals a surprising reality: even top models like o1 achieve less than 10% overall accuracy under step-wise scrutiny; this is a drop of up to 65.5% from their accuracy considering only final answer equivalence. This discrepancy exposes fragile deductive chains and a critical gap for current LLMs between merely finding an answer and constructing a rigorous proof. Scaling model size and increasing test-time computation yield limited gains in overall proof correctness. Instead, our findings highlight promising research directions such as theorem-guided reasoning and self-refinement. Code and data are available at https://ineqmath.github.io/.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
