LogicSkills: 대규모 언어 모델의 형식적 추론을 위한 구조화된 벤치마크

LogicSkills: A Structured Benchmark for Formal Reasoning in Large Language Models

대규모 언어 모델은 다양한 논리적 추론 벤치마크에서 괄목할 만한 성능을 보여주었습니다. 그러나 모델들이 어떤 핵심 논리적 기술을 진정으로 습득했는지는 여전히 불분명합니다. 이를 해결하기 위해, 우리는 형식적 추론의 세 가지 기본 기술을 분리하도록 설계된 통합 벤치마크인 LogicSkills를 소개합니다. 이 세 가지 기술은 (i) 형식적 기호화(전제를 1차 논리로 변환), (ii) 반례 모델 구성(모든 전제가 참이면서 결론은 거짓인 유한 구조 형성), (iii) 타당성 평가(주어진 전제 집합에서 결론이 도출되는지 결정)입니다. 항목들은 (동일성을 포함하지 않는) 1차 논리의 2변수 단편에서 추출되었으며, 자연스러운 영어와 무의미한 단어(nonce words)를 사용한 캐럴(Carroll) 스타일 언어 두 가지로 제시됩니다. 모든 예제는 SMT 솔버 Z3를 사용하여 정확성과 비자명성(non-triviality)을 검증했습니다. 주요 모델들을 대상으로 평가한 결과, 타당성 평가 성능은 높게 나타났으나 기호화 및 반례 모델 구성 성능은 상당히 낮았으며, 이는 모델들이 진정한 기호적 또는 규칙 기반 추론보다는 표면적 패턴에 의존하고 있음을 시사합니다.

Large language models have demonstrated notable performance across various logical reasoning benchmarks. However, it remains unclear which core logical skills they truly master. To address this, we introduce LogicSkills, a unified benchmark designed to isolate three fundamental skills in formal reasoning: (i) $\textit{formal symbolization}\unicode{x2014}$translating premises into first-order logic; (ii) $\textit{countermodel construction}\unicode{x2014}$formulating a finite structure in which all premises are true while the conclusion is false; and (iii) $\textit{validity assessment}\unicode{x2014}$deciding whether a conclusion follows from a given set of premises. Items are drawn from the two-variable fragment of first-order logic (without identity) and are presented in both natural English and a Carroll-style language with nonce words. All examples are verified for correctness and non-triviality using the SMT solver Z3. Across leading models, performance is high on validity but substantially lower on symbolization and countermodel construction, suggesting reliance on surface-level patterns rather than genuine symbolic or rule-based reasoning.