这不是简单的笑话或调侃，而是正在发生的现象。
近期，大语言模型在处理不等式证明问题时展现出了令人惊讶的能力，它们可以给出看似正确的答案。这些答案背后的推理过程却常常经不起推敲，逻辑往往存在严重问题。斯坦福大学、UC伯克利和MIT等机构联合发布了一篇研究论文《大语言模型在不等式证明任务上的能力评估》，首次系统地研究了29个顶级大模型在解决奥数级别的不等式证明任务时的表现。
研究团队深入探究了大语言模型在不等式证明这一典型任务中的真实推理能力。他们发现，尽管模型给出的答案有时与标准答案一致，但其推理过程却存在大量错误。传统的数学不等式证明既难以自动验证，又常依赖于高度形式化的语言系统，这些系统虽然逻辑严谨，但表达繁琐、建模成本高，难以适应奥数级别问题的规模化分析。它们与人类的自然推理过程存在较大距离。
为了解决这个问题，团队开发了一种新型的不等式任务数据集IneqMath，以及一套名为LLM as Judge的评估系统。IneqMath数据集将复杂的不等式证明过程分解为两个子任务，旨在用自然语言保证与人的直觉统一，同时确保结果的可验证性。LLM as Judge则可以对模型的推理过程进行逐步，实现自动化评分和细粒度诊断。
尽管研究团队发现了两个有效的优化策略：自我反思反馈机制和引入定理线索辅助模型思考，但他们发现大多数大型模型的逻辑推理能力仍远远达不到真正逻辑证明的水平。尽管如此，IneqMath的挑战榜仍在不断推动大语言模型在严谨数学推理方面的进展。如果你有兴趣展示你的模型推理实力，欢迎参与挑战。更多信息可访问项目主页查看论文和开源代码等详细内容。这种现象值得我们进一步关注和研究，以推动人工智能技术的发展。
