HOLMES: LLM에서 고차 논리 추론 능력 평가

HOLMES: Evaluating Higher-Order Logical Reasoning in LLMs

논리적 추론은 신뢰할 수 있는 AI를 구축하는 데 필수적이지만, 기존의 벤치마크는 주로 1차 논리에 기반하며, 고정된 술어에 대한 객체 수준의 연역에 초점을 맞추고 있습니다. 이는 모델이 규칙, 술어, 함수, 제약 조건 및 의사 결정 절차 자체를 추론해야 하는 많은 현실적인 시나리오를 간과합니다. 본 연구에서는 LLM에서 고차 기호 추론을 위한 최초의 실제 벤치마크인 HOLMES (Higher-Order Logic Meets real-world Explainable Symbolic reasoning)를 소개합니다. HOLMES는 총 1379개의 인스턴스로 구성되어 있으며, 고차 논리를 기반으로 자연어 문제를 HOL 형식화, 정답, 검증 가능한 추론 과정 및 법률 및 금융 분야의 세밀하게 제어 가능한 추론 요소와 연결합니다. 실험 결과, 현재 LLM은 여전히 HOLMES에서 어려움을 겪으며, 평균 정확도는 50.64%에 불과하고 최고 성능 모델도 59.54%에 그쳤습니다. 추가 분석 결과, 높은 최종 답변 정확도가 충돌 해결 설정에서 단축 경로 기반의 추론을 가릴 수 있으며, 범위 조건 및 구성적 추론 하에서는 성능이 크게 저하됩니다. 이러한 결과는 고차 기호 추론이 신뢰할 수 있고 검증 가능한 LLM을 구축하는 데 있어 중요한 병목 현상임을 보여줍니다. 프로젝트 코드와 데이터셋은 https://github.com/wuyucheng2002/HOLMES 에서 공개적으로 이용 가능합니다.

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.