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

不等式证明在众多科学和数学领域至关重要，它考验着发现紧密界限和战略性应用定理等高级推理能力。这使得它成为大型语言模型（LLMs）一个独特且极具挑战性的前沿领域，其提供的洞察力超越了一般的数学问题解决。现有数据集的稀缺性、合成性或过于严格的正式性阻碍了该领域的进展。为解决此问题，我们提出了一种非正式但可验证的任务表述，将不等式证明重构为两个可自动检查的子任务：界限估计和关系预测。在此基础上，我们发布了IneqMath，这是一个由专家精心策划的奥林匹克竞赛级别不等式数据集，包含一个测试集和丰富的训练语料库，其中包含了逐步解题过程和定理注释。我们还开发了一种新颖的“LLM即评判者”评估框架，该框架结合了一个最终答案评判者和四个逐步评判者，旨在检测常见的推理缺陷。对IneqMath上29个领先LLM进行的系统评估揭示了一个惊人的事实：即使是像o1这样的顶级模型，在逐步审查下的整体准确率也低于10%；这与它们仅考虑最终答案等效性的准确率相比，下降了高达65.5%。这一差异暴露出脆弱的演绎链，以及当前LLM在仅仅找到答案和构建严谨证明之间存在的关键鸿沟。扩大模型规模和增加测试时计算量对整体证明正确性的提升有限。相反，我们的研究结果强调了定理引导推理和自我完善等有前景的研究方向。代码和数据可在https://ineqmath.github.io/获取。