首个评估大模型高阶逻辑推理能力的真实世界基准
HOLMES: Evaluating Higher-Order Logical Reasoning in LLMs
- 基于高阶逻辑构建，融合自然语言与形式化表达
- 当前大模型平均准确率仅50.64%，最优模型达59.54%
- 适用于法律、金融场景，适合研究可信AI的学者
逻辑推理对可靠人工智能至关重要，但现有评测基准多聚焦一阶逻辑，仅关注固定谓词上的对象级推断，忽略了现实中需对规则、谓词、函数、约束和决策过程本身进行推理的情形。我们提出HOLMES（高阶逻辑对接真实世界可解释符号推理），首个面向大模型高阶符号推理的真实世界评测基准，包含1379个实例。基于高阶逻辑，HOLMES将自然语言问题与高阶逻辑形式化表达、真值答案、可验证推理路径及细粒度可控推理因子结合，覆盖法律与金融领域。实验表明，当前大模型在HOLMES上表现仍不佳，平均准确率仅为50.64%，最佳模型达到59.54%。分析发现，高最终答案准确率可能掩盖冲突解决情境中的捷径推理，且在作用域约束和组合推理条件下性能显著下降。这些结果揭示高阶符号推理是构建可靠可验证大模型的关键瓶颈。项目代码与数据集已公开于https://github.com/wuyucheng2002/HOLMES。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。