arXiv:2606.23238v3 Announce Type: replace Abstract: Existing LLM logical-reasoning benchmarks largely focus on object-level inference under fixed predicates and rules, leaving higher-order reasoning over rules and policies underexplored. We introduce HOLogicBench, a 1,379-instance benchmark that systematically evaluates five representative higher-order reasoning operations, with Isabelle/HOL formalizations and proof-verified answers. Beyond answer accuracy, HOLogicBench provides solver-verified reference reasoning paths for each instance, enabling fine-grained evaluation of model-generated reasoning against valid derivations. Across 16 model configurations, average accuracy is 53.86\%, with the best configuration reaching 65.99\%. Further analyses reveal that LLMs exhibit limited alignment with valid derivations, remain vulnerable to minimal counterfactual perturbations, and display distinct failure patterns across higher-order reasoning types.