大语言模型求解不等式证明

不等式证明是贯穿于多个数学与科学领域的关键任务，考验着发现紧界限和战略定理应用等高级推理能力。这使得其成为大语言模型(LLMs)面临的独特且艰巨的前沿，为超越一般数学问题解决提供了洞见。当前研究受限于数据稀缺、合成或僵化形式的现有数据集。我们通过提出一种非正式但可验证的任务表述，解决了这一问题，将不等式证明重新塑造为两个可自动检查的子任务：界限估计和关系预测。在此基础上，我们发布IneqMath，一个由专家精选的奥林匹克级不等式数据集，包括测试集和训练语料，增添了逐步解决方案和定理注释。我们还开发了一种新型LLM评估框架，结合最终答案评判器与四个步骤级评判器，以检测常见推理缺陷。对29个领先LLM在IneqMath上的系统评估揭示了惊人现实：即便是像o1这样的顶级模型，在步骤级审查下也仅达到10%以上的整体准确率；相对于仅考虑最终答案等价性，其准确率下降了最高可达65.5%。这一差距暴露了脆弱的演绎链以及当前LLMs在仅找到答案与构建严密证明之间存在的关键差距。模型规模扩大和增加测试时计算仅在整体证明正确性方面有限地带来收益。相反，我们的发现凸显了诸如定理引导推理和自我精炼等有前景的研究方向。代码和数据已在https://ineqmath.github.io/上提供。