利用大型语言模型解决不等式证明问题

不等式证明在多个科学和数学领域中至关重要，它考验了高级推理技能，如发现紧界和战略性定理应用。这使得大型语言模型（LLMs）在这个领域面临着独特的、具有挑战性的前沿问题，提供了超越一般数学问题解决的深刻见解。现有数据集通常稀缺、合成或形式僵化，阻碍了这一领域的进展。为此，我们提出了一种非正式但可验证的任务表述方法，将不等式证明重新划分为两个自动检查的子任务：界估计和关系预测。基于此，我们发布了IneqMath，这是一个由专家策划的奥林匹克级别的不等式数据集，包括测试集和训练语料库，并附有逐步解决方案和定理注释。我们还开发了一个新的LLM-as-judge评估框架，结合了一个最终答案评判器和四个设计用于检测常见推理缺陷的逐步评判器。对29个领先的大规模语言模型在IneqMath上的系统评估揭示了一个令人惊讶的事实：即使是最顶级的模型o1，在逐步审查下整体准确率也低于10%，这比仅考虑最终答案等价时的准确率下降了高达65.5%。这种差异暴露了脆弱的演绎链以及当前大规模语言模型在仅仅找到答案与构建严格证明之间的关键差距。增加模型规模和提高测试时计算量只能有限地提升整体证明正确性。相反，我们的研究结果指出了有前景的研究方向，如定理引导推理和自我完善。代码和数据可在 https://ineqmath.github.io/ 获取。