LogicSkills ‘논리 잘함’을 스킬 단위로 쪼개서 보자

LogicSkills ‘논리 잘함’을 스킬 단위로 쪼개서 보자

LLM의 “논리추론 능력”은 한 덩어리로 측정하면 착시가 생기기 쉽습니다. LOGICSKILLS는 논리 과제를 하위기술로 분해하고 Z3로 자동검증해, 모델이 진짜 구조를 이해했는지 아니면 보기 좋은 분류만 잘하는지 드러내려는 시도입니다.

기호화가 왜 논리력의 관문인지

이 논문의 가장 큰 기여는 “논리추론”을 세 가지 핵심 하위기술로 분해해 평가 프레임을 만든 점입니다. (i) 자연어→1차논리 기호화(formal symbolization), (ii) 반례 카운터모델 구성(countermodel construction), (iii) 후보 결론의 타당성 판단(validity assessment)입니다. 이 분해는 단순히 태스크를 나눈 것이 아니라, 우리가 흔히 “추론 잘한다”고 부르는 모델의 성능이 사실은 (iii) 분류형 판정에 치우쳐 있을 수 있다는 문제의식을 실험으로 검증 가능하게 만듭니다.

특히 기호화는 논리 시스템에서 가장 현실적인 병목입니다. 사람도 논리학 과제에서 “정답(타당/비타당)”을 고르는 문제는 어느 정도 감으로 풀지만, 문장을 스스로 정확히 논리식으로 옮기려면 양화사 범위, 조건문 구조, ‘only’ 같은 제한자(only-restrictor), 부정의 위치 등에서 실수가 잦습니다. LOGICSKILLS는 이 병목을 의도적으로 분리해 드러냅니다. 문장과 함께 “Key(기호 사전)”를 주고, 모델이 제공된 술어/상수/연산자만 사용해 단일 well-formed formula를 출력하도록 요구합니다. 이 설계는 “자연어 이해”와 “형식화 능력”을 동시에 보게 하며, 특히 기호화가 단지 표기 변환이 아니라 ‘논리 구조에 대한 민감성’을 요구한다는 점을 부각합니다.

논문이 선택한 논리 범위도 의도가 분명합니다. 모든 예제는 FO2(두 변수 1차논리, identity 없음)에서 생성됩니다. FO2는 결정가능성과 유한만족성 같은 성질 덕분에 대규모 생성·검증이 가능하고, Z3 기반으로 “정답을 자동으로 확정”할 수 있습니다. 사용자의 비평처럼 이것은 장점이면서 동시에 범위 제한입니다. 현실 자연어 논증의 핵심 난점(동일성, 스코프 모호성, 수량 비교, 고차/모달 성질 등)이 일부 빠지기 때문입니다. 그럼에도 저는 이 선택이 “벤치마크로서의 책임”을 우선한 판단이라고 봅니다. 논리 범위를 넓히면 표현력은 좋아지지만, 데이터 생성과 자동검증의 신뢰성이 떨어져 “평가가 흔들리는 벤치”가 되기 쉽기 때문입니다.

여기서 독자가 실제로 얻을 교훈은 단순합니다. 어떤 모델이 validity에서 천장에 가깝게 나온다고 해서, 그 모델이 자연어 문장을 논리 구조로 안정적으로 옮길 줄 안다고 결론내리면 위험합니다. LOGICSKILLS의 구조는 “기호화를 못하면 결국 논리 시스템을 스스로 세울 수 없다”는 점을 수치로 보여줍니다. 그리고 그 수치는 단순 채점이 아니라 Z3 등가성 검증까지 거친 결과라, ‘정답 라벨의 신뢰도’가 높다는 점도 의미가 큽니다.

하위기술	LOGICSKILLS가 겨냥한 ‘착시’
formal symbolization	정답 분류는 잘하지만, 문장을 스스로 논리식으로 옮기지 못하는 문제
countermodel construction	비타당을 ‘설명’하지 못하고 반례 구조를 직접 구성하지 못하는 문제
validity assessment	표면 패턴으로 후보 결론을 고르는 능력이 ‘논리 이해’로 오인되는 문제

반례가 가장 판별력 높은 이유와 ‘포맷 실패’ 분리

논문이 가장 인상적으로 보여주는 패턴은 “validity는 높은데 countermodel은 낮다”는 비대칭입니다. 예컨대 GPT-4o는 validity에서 높게 나오지만 countermodel은 매우 낮고, Gemini-2.5-Flash도 validity가 높음에도 countermodel이 낮습니다. 반면 Qwen3-32B는 세 과제 모두에서 예외적으로 높게 보고됩니다(예: validity 97%, symbolization 85%, countermodel 89% 수준). 논문은 countermodel을 “가장 판별력 높은 과제”로 취급하는데, 그 이유는 단순합니다. 비타당성을 안다는 것은 “어딘가 반례가 존재한다”는 메타 지식이 아니라, 실제로 전제를 모두 만족시키면서 결론을 거짓으로 만드는 구체적 구조를 구성할 수 있어야 하기 때문입니다. 즉, 규칙적 증명(또는 분류)보다 ‘모형론적 이해’가 더 직접적으로 요구됩니다.

다만 사용자의 비평처럼 countermodel 과제는 논리력 외에 “구조화 출력 능력”이 점수에 섞일 수 있습니다. LOGICSKILLS는 고정 도메인(예: [0,1,2])에서 상수 해석, 단항 술어의 확장, 이항 술어의 쌍 리스트를 요구합니다. 이때 논리적 아이디어는 맞는데 리스트 형식, arity, 상수 누락 같은 인터페이스 문제로 실패할 수 있습니다. 논문도 이를 인지하고 extractor LLM으로 출력 정규화/복구를 하고, Z3로 “진짜로 전제는 참이고 결론은 거짓인지”를 자동검증합니다. 그럼에도 포맷 민감성이 완전히 사라지지는 않습니다.

그래서 이 벤치마크가 더 강해지려면(그리고 독자가 해석을 더 안전하게 하려면), 실패를 “논리 실패 vs 포맷 실패”로 더 세분해야 합니다. 논문은 에러 분석에서 countermodel의 오류가 크게 두 갈래라는 점을 보여줍니다. 다수는 “구조는 그럴듯하지만 실제로 반례가 아님(전제 중 일부가 거짓이 됨)”이고, 일부는 “해석 누락/형식 오류”입니다. 이 분해는 이미 좋은 출발점입니다. 여기서 한 걸음 더 나가 “동일 논리 내용의 표현 다양성(순서 변경, 중복 허용, 동치 표현)”에 대해 채점이 얼마나 관대해질 수 있는지, 그리고 관대함을 늘렸을 때 모델 순위가 바뀌는지까지 보여주면 countermodel이 ‘논리 판별력’으로서 더 깔끔해집니다. 예를 들어 다음과 같은 추가 분석이 유용합니다.

표현 다양성 허용 실험입니다. 술어 확장의 원소 순서, 이항 술어 쌍의 순서, 상수 배정 표기 등을 다양화해도 동일한 구조로 인정하는지 점검하는 것입니다.

“최소 수정(repair) 거리” 기반 분석입니다. 모델 출력이 거의 맞지만 한 쌍만 틀린 경우와 완전히 엉뚱한 경우를 구분해, 논리적 근접도를 측정할 수 있습니다.

포맷 강제 vs 자유 출력 비교입니다. 포맷을 엄격히 요구할 때와, 자연어로 “이 도메인에서 a는 1이고… ”처럼 말하게 한 뒤 파서가 구조를 추출하도록 할 때의 성능 차이를 보면, 실패 원인이 인터페이스인지 논리인지 더 분명해집니다.

이런 제안은 논문 메시지를 약화시키지 않습니다. 오히려 “countermodel이 낮다”는 결론이 정말로 ‘모형론적 추론의 부재/취약’에서 오는 것인지, 아니면 ‘구조 출력 인터페이스’에서 오는지 정밀하게 가를수록 논문의 주장은 더 강해집니다. 특히 논문 자체가 solver-verified 평가를 강점으로 내세우는 만큼, 채점 로직의 관대함/엄격함이 결과에 미치는 영향까지 계량화하면 “벤치마크 신뢰도”가 한 단계 올라갑니다.

타당성 천장과 ‘표면 패턴’ 해석의 균형

LOGICSKILLS 결과 해석에서 가장 조심해야 할 대목이 바로 메커니즘 단정입니다. 논문은 “LLM이 명시적 상징·모형 절차 없이 근사적으로 성공한다”는 결론 방향을 제시하지만, 동시에 본 평가가 behavioral evaluation임을 분명히 합니다. 즉, 모델 내부에 어떤 절차가 “없다”는 것을 직접 관찰한 것이 아니라, 행동 패턴이 전통적인 상징 절차와 다르다는 점을 보여준 것입니다. 사용자의 비평대로 이 간격은 중요합니다. 같은 결과도 “상징 절차가 없다”가 아니라 “상징 절차를 안정적으로 실행하는 행동 증거가 약하다” 정도가 더 안전한 문장입니다.

그럼에도 논문이 제시하는 시사점은 매우 큽니다. 많은 모델에서 validity가 천장에 가깝고(symbolization/ countermodel은 낮음), 이는 “후보 결론 중 정답 고르기”가 논리 구조 이해의 충분조건이 아님을 보여줍니다. 특히 validity 과제에서 틀린 응답의 다수가 “정답을 포함하면서도 추가로 오답을 함께 고르는(슈퍼셋 오류)” 형태라는 분석은, 모델이 ‘따라야 하는 것(must follow)’과 ‘그럴듯한 것(plausible)’을 분리하는 데 약할 수 있음을 시사합니다. 이는 실제 응용에서도 위험 신호입니다. 에이전트가 어떤 결론을 “반드시 참”이라고 확정해버리면 시스템이 경직되지만, 반대로 가능한 결론을 모두 “참일 수 있음”으로 묶어버리면 결정을 못 내립니다.

또 하나의 설계 강점은 Carrollian(무의미 단어) 조건입니다. controlled English와 구조는 동일하되 어휘를 무의미하게 바꿔 상식/의미 기반 휴리스틱을 걷어내려는 시도입니다. 흥미롭게도 논문은 English와 Carroll 성능 차이가 크지 않다고 보고합니다(평균적으로 validity와 symbolization 모두 큰 차이가 없음). 이 결과는 “적어도 이 설정에서는 의미 지식이 크게 작동하지 않는다”는 쪽으로 읽힐 수 있습니다. 다만 해석은 양면적입니다. (1) 모델이 정말로 구조 중심으로 처리했을 수도 있고, (2) 반대로 과제가 통제된 문장이라 애초에 의미 지식이 개입할 여지가 작았을 수도 있습니다. 그래서 Carrollian이 만능 필터라고 보기보다는, “상식 지식의 개입을 줄인 조건에서도 동일한 스킬 프로파일이 나온다”는 점이 의미 있다고 보는 편이 더 정확합니다.

Qwen3-32B의 예외적 성능 해석도 같은 균형이 필요합니다. 논문은 Qwen3-32B가 자발적 self-scaffolding( 같은 내부 구분자)을 사용하고, chain-of-thought가 다른 모델보다 평균 7.5배 길다는 관찰을 함께 제시합니다. 이는 흥미로운 상관이지만, 인과로 말하려면 사용자의 제안처럼 통제 실험이 필요합니다. 같은 모델에서 CoT 길이를 제한/유도했을 때 성능이 어떻게 바뀌는지, 또는 다른 모델에 유사한 스캐폴딩을 강제했을 때 symbolization/countermodel이 실제로 오르는지 검증해야 합니다. 그렇지 않으면 “긴 생각=잘함”이라는 단순화로 흐를 위험이 있습니다. 실제로는 (a) 학습 데이터/아키텍처 차이, (b) 논리식 출력에 유리한 내부 루틴, (c) 출력 포맷을 안정화하는 디코딩 습관 등 여러 요인이 얽혀 있을 수 있기 때문입니다.

마지막으로, PEFT(LoRA) 전이 실험은 이 논문에서 가장 실용적인 경고등입니다. Llama-3.2-3B-Instruct를 대상으로 symbolization과 countermodel을 각각 100k씩 LoRA로 학습했을 때, 과제 내 성능은 크게 오르지만 validity에는 전이가 거의 없거나 오히려 하락하는 결과를 보고합니다. 이는 “하위기술을 잘하게 만들면 상위 분류도 좋아질 것”이라는 흔한 기대가 자동으로 성립하지 않음을 보여줍니다. 실무적으로는 멀티태스크 목표 설계, 보상 구성, 혹은 ‘하위기술이 상위 판정에 실제로 호출되도록 만드는 스캐폴딩’이 따로 필요하다는 뜻입니다.

LOGICSKILLS는 기호화·반례·타당성으로 논리력을 분해하고 Z3 검증으로 신뢰도 높은 평가를 제시합니다. 다만 결과는 행동적 증거이므로 메커니즘 단정은 신중해야 하며, 카운터모델의 포맷 영향과 CoT 상관의 인과는 추가 통제가 필요합니다.

자주 묻는 질문 (FAQ)

Q. LOGICSKILLS의 세 과제 중 무엇이 가장 “진짜 논리력”을 잘 가르나요? A. 논문 결과 패턴상 countermodel construction이 가장 판별력이 높습니다. 많은 모델이 validity는 높지만 countermodel에서 크게 무너져, 단순 분류가 아닌 모형론적 구성 능력을 더 직접 드러냅니다.

Q. Carrollian(무의미 단어) 조건이 있으면 “상식 기반 치팅”을 완전히 막을 수 있나요?
A. 완전히 막는다고 단정하기는 어렵습니다. 다만 controlled English와 동일 구조를 유지하면서 어휘 의미를 제거해, 의미 지식 개입을 줄인 조건에서도 유사한 스킬 프로파일이 나타나는지를 점검하는 데 유용합니다.

Q. symbolization과 countermodel을 LoRA로 학습하면 validity도 같이 오르지 않나요?
A. 논문에서는 LoRA로 과제 내 성능은 크게 올렸지만 validity로의 전이는 거의 없거나 감소하는 결과를 보고합니다. 이는 하위기술 학습만으로 상위 판정이 자동 개선되지 않으며, “호출 구조(스캐폴딩)와 목표 설계”가 별도로 필요하다는 신호입니다.

[출처]https://arxiv.org/html/2602.06533v1