HOLMES: 评估大语言模型中的高阶逻辑推理
HOLMES: Evaluating Higher-Order Logical Reasoning in LLMs
AI总结：
提出HOLMES基准，基于高阶逻辑评估LLM在规则、谓词和约束上的推理能力，发现当前模型平均准确率仅50.64%，揭示高阶符号推理是关键瓶颈。
摘要：
逻辑推理对于可靠的AI至关重要，然而现有的基准大多以一阶逻辑为中心，侧重于固定谓词上的对象级演绎。这忽略了模型必须对规则、谓词、函数、约束和决策过程本身进行推理的许多现实场景。我们引入了HOLMES（高阶逻辑遇见现实世界可解释符号推理），这是LLM中高阶符号推理的第一个现实世界基准，包含1379个实例。基于高阶逻辑，HOLMES将自然语言问题与HOL形式化、真实答案、可验证的推理轨迹以及跨法律和金融的细粒度可控推理因素配对。实验表明，当前LLM在HOLMES上仍然困难重重，平均准确率仅为50.64%，最佳模型达到59.54%。我们的分析进一步揭示，高最终答案准确性可能掩盖冲突解决设置中的捷径推理，而在范围条件和组合推理下性能急剧下降。这些发现将高阶符号推理确定为构建可靠且可验证LLM的关键瓶颈。项目代码和数据集在此https URL公开。
英文摘要：
Logical reasoning is essential for reliable AI, yet existing benchmarks are largely first-order-logic-centric, focusing on object-level deduction over fixed predicates. This misses many realistic scenarios where models must reason over rules, predicates, functions, constraints, and decision procedures themselves. We introduce HOLMES (Higher-Order Logic Meets real-world Explainable Symbolic reasoning), the first real-world benchmark for higher-order symbolic reasoning in LLMs, containing 1379 instances. Built on higher-order logic, HOLMES pairs natural-language problems with HOL formalizations, ground-truth answers, verifiable reasoning traces, and fine-grained controllable reasoning factors across law and finance. Experiments show that current LLMs still struggle on HOLMES, with an average accuracy of only 50.64% and the best model reaching 59.54%. Our analyses further reveal that high final-answer accuracy can mask shortcut reasoning in conflict-resolution settings, while performance drops sharply under scope-conditioned and compositional reasoning. These findings identify higher-order symbolic reasoning as a key bottleneck for building reliable and verifiable LLMs. The project code and dataset are publicly available at https://github.com/wuyucheng2002/HOLMES.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
