HOLMES: Evaluating Higher-Order Logical Reasoning in LLMs

Source

• Source name: arXiv
• Source kind: paper
• Authors / organization: Yucheng Wu, Jundong Xu, Mingzhen Ju, Yue Yu, Chenpeng Wang, Haoxuan Li, Liangming Pan
• Venue: arXiv: cs.AI
• Published: 2026-06-22
• Collected: 2026-06-23
• URL: http://arxiv.org/abs/2606.23238v1
• PDF: https://arxiv.org/pdf/2606.23238v1
• DOI: UNKNOWN

Plain-Language Brief

The paper introduces HOLMES, a new benchmark for evaluating higher-order symbolic reasoning in Large Language Models (LLMs). This benchmark is designed to test the models' ability to reason over rules, predicates, functions, constraints, and decision procedures. The research shows that current LLMs perform poorly on this benchmark, with an average accuracy of 50.64% and the best model reaching 59.54%. The study also reveals that high final-answer accuracy can mask shortcut reasoning in conflict-resolution settings and performance drops sharply under scope-conditioned and compositional reasoning.

What the Document Says

• The paper presents HOLMES, a new benchmark for higher-order symbolic reasoning in LLMs.
• HOLMES contains 1379 instances built on higher-order logic.
• The benchmark 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 have an average accuracy of 50.64% on HOLMES, with the best model reaching 59.54%.
• The study reveals that high final-answer accuracy can mask shortcut reasoning in conflict-resolution settings.
• Performance drops sharply under scope-conditioned and compositional reasoning.

Key Concepts Mentioned

• HOLMES
• Large Language Models (LLMs)
• higher-order logic
• benchmark
• natural-language problems
• HOL formalizations
• ground-truth answers
• verifiable reasoning traces
• fine-grained controllable reasoning factors
• law and finance
• experiments
• average accuracy
• final-answer accuracy
• shortcut reasoning
• conflict-resolution settings
• scope-conditioned reasoning
• compositional reasoning

Claims Made by the Document

• Current LLMs struggle on HOLMES.

Evidence Used

• The average accuracy of 50.64% and the best model reaching 59.54%.

Methods / Approach

UNKNOWN

Limitations Stated by the Authors

UNKNOWN

Limitations Noted by the Agent

Agent interpretation — not from the source.

UNKNOWN

Open Questions

UNKNOWN

Notes for Future Q&A

May include interpretation. Labeled where it does.

UNKNOWN

Raw Abstract / Excerpt

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.