기술 요약: 동일한 공식, 다른 의미론

문제 정의

본 논문은 양상 논리(modal logic)에 관한 대규모 언어 모델(LLM)의 추론 능력을 평가하는 데 있어 존재하는 결정적인 격차를 다룬다. 기존의 벤치마크(예: ProofWriter, FOLIO, LogicNLI)는 고정된 암묵적 배경 논리 하에서 연역을 평가하지만, 명시적으로 기술된 의미론적 사양(semantic specifications)에 모델이 적응할 수 있는지를 테스트하는 데는 실패한다. 양상 논리에서 추론의 타당성은 종종 특정 프레임 속성(예: 반사성, 이행성, 대칭성)이나 도메인 조건(예: 상수 도메인 대 가변 도메인)에 따라 달라진다. 모델은 주어진 제약 조건(stipulated constraints)을 준수하기보다는 지배적인 추론 체계(예: '친숙한' 논리인 S5)를 학습함으로써 성능을 높일 수 있다. 핵심 문제는 LLM이 자신의 기본적 논리 직관을 억제하고, 규정된 (잠재적으로 비표준적인) 의미론적 조건을 따를 수 있는지 여부를 결정하는 것이다.

방법론

저자들은 공식적 패턴 매칭으로부터 의미론적 제어를 분리하도록 설계된 진단 벤치마크를 구축한다.

1. 벤치마크 구축:

• 쌍을 이룬 문제(Paired Problems): 데이터셋의 핵심은 전제($P$)와 추측($C$)은 동일하지만, 의미론적 사양($S$)이 정확히 하나만 다른(예: 반사적 프레임을 이행적 프레임으로 바꾸거나, 누적 도메인을 감소하는 도메인으로 바꾸는 것) 문제 쌍들로 구성된다.
• 오라클 검증(Oracle Verification): 자동 추론 오라클(LET 임베딩 툴체인을 통해 Vampire 및 Leo-III 사용)을 사용하여 두 사양이 동일한 공식에 대해 서로 다른 진릿값($y_a \neq y_b$)을 생성함을 검증한다.
• 균형 잡힌 코어(Balanced Core): 모델이 (공식을 읽지 않고) 의미론적 라벨에 의해서만 답이 결정되는 "조건 전용" 지름길을 이용하는 것을 방지하기 위해, 저자들은 160개의 쌍으로 이루어진 "균형 잡힌 비중첩 코어"를 만들었다. 이 서브셋에서 각 의미론적 조건은 True와 False 라벨과 동일한 빈도로 나타난다. 여기서의 성공은 해당 조건이 어떤 공식을 유효하게 만드는지 결정하기 위해 반드시 공식을 읽어야 함을 의미한다.
• 범위(Scope): 데이터셋은 5가지 프레임 속성 대조(K–D, K–T, T–B, T–S4, B–S5)와 3가지 도메인 대조(가변–누적, 가변–감소, 누적–상수)를 다루며, 총 800개의 중첩 시스템 쌍과 160개의 균형 잡힌 코어 쌍을 포함한다.
• 프롬프팅(Prompting): 프롬프트는 관습적인 시스템 명칭(예: "S4")을 사용하지 않고, 규칙을 명시적으로 기술하기 위해(예: "접근 관계는 반사적이고 대칭적이다") 통제된 영어 표현을 사용하며, 이를 통해 모델이 제공된 규칙에 의존하도록 강제한다.

2. 실험 프로토콜:

• 모델: 연구는 최근의 5개 모델을 평가한다: DeepSeek V4 (Flash 및 Pro), GPT-5.6 (Luna 및 Terra), Claude Sonnet 5.
• 조건:
  • 직접 프롬프팅(Direct Prompting): 추론 모드 없이 수행되는 표준 추론.
  • 추론 모드(Reasoning Mode): 특정 모델(예: DeepSeek Flash "high effort")에서 활성화되어, 추론 시 계산량 증가가 의미론적 준수에 도움이 되는지 테스트한다.
  • 표현 민감도(Representation Sensitivity): 명명된 영어 조건, 관계적 정의, 그리고 공식적인 TPTP 구문 간의 성능을 테스트하는 서브셋이다.
  • 의미론적 친화도(Semantic Affinity): 사양을 생략했을 때 모델이 어떤 "기본" 논리를 선호하는지 식별하기 위한 실험이다.

주요 결과

1. 직접 프롬프팅 하에서의 의미론적 제어 실패:
균형 잡힌 코어에서, 5개 모델 중 4개가 "조건 전용" 베이스라인인 50%(모델이 공식을 무시하고 조건 라벨에 따라 추측한다고 가정할 때의 수치)보다 현저히 낮은 성능을 보였다.

• DeepSeek V4 Flash: 엄격한 쌍 정확도 4.4%.
• DeepSeek V4 Pro: 2.5%.
• GPT-5.6 Luna: 21.2%.
• GPT-5.6 Terra: 25.0%.
• Claude Sonnet 5: 65.0% (베이스라인을 초과한 유일한 모델).
  이는 대부분의 모델이 기술된 의미론을 추적하는 대신, 제약 조건에 관계없이 고정된 친숙한 논리를 적용한다는 것을 나타낸다.

2. 복구 기제로서의 추론 모드:
추론 모드를 활성화하면 DeepSeek V4 Flash의 성능이 균형 잡힌 코어에서 4.4%에서 **88.1%**로 급격히 향상되었다. GPT-5.6 Luna에서도 프레임 문제에 대해 유사한 이점이 관찰되었다. 이는 실패의 원인이 반드시 논리적 지식의 결여 때문이 아니라, 특정 제약 조건을 처리하기 위한 올바른 추론 모드를 활성화하는 데 실패했기 때문임을 시사한다.

3. 의미론적 친화도 및 기본값:
사양이 생략되었을 때, 모델들은 친숙한 논리(예: DeepSeek Flash는 K를 선호, Sonnet은 K를 선호, 기타 모델은 T를 선호)와 일관된 친화도를 보였다. 그러나 이러한 기본값들이 명시적 제약이 있을 때의 오류를 신뢰성 있게 예측하지는 못했다. 즉, 모델들은 사양이 없는 문제에서는 합의하는 듯 보였으나, 제약이 추가되었을 때 조정하는 데는 실패했다.

4. 표현 민감도:
입력 형식을 변경하는 것(명명된 조건에서 관계적 정의 또는 TPTP로)은 성능 순위를 변화시켰지만, 의미론적 제어를 일관되게 복구하지는 못했다. 예를 들어, GPT-5.6 Terra의 정확도는 38%(명명됨)에서 6%(관계적 정의)로 떨어졌으며, 이는 표면적인 포맷팅이 근본적인 의미론적 준수 문제를 해결하는 간단한 해결책이 아님을 나타낸다.

주요 기여

• 진단 벤치마크: 대상 수준의 문제는 고정하되 의미론적 사양을 변화시켜 "사양 민감도(specification sensitivity)"를 테스트하도록 설계된 통제된 평가 프레임워크를 도입하였다.
• 균형 잡힌 코어: 논리 공식을 읽지 않고 의미론적 조건을 답에 매핑하여 문제를 푸는 가능성을 제거한 새로운 데이터셋 설계를 제시하였다.
• 모드 의존성의 실증적 증거: 양상 의미론을 따르는 능력이 추론 모드(직접 vs 추론)에 크게 의존함을 입증하여, LLM의 정적인 논리 추론 능력 개념에 도전하였다.
• 리소스 공개: 공식, 오라클 아티팩트, 반례(countermodels) 및 모델 응답을 공개하였다.

의의 및 주장

본 논문은 고정된 의미론 벤치마크가 LLM 추론의 견고함을 과대평가할 수 있다고 주장한다. 주요 발견은 양상 지식(논리를 아는 것)과 의미론적 제어(주어진 특정 논리를 적용하는 것)가 구별된다는 점이다. 모델은 필요한 논리 규칙을 보유하고 있더라도, 로컬 사양이 답변을 지배하도록 허용하지 못하고 대신 익숙한 추론 체계로 회귀할 수 있다.

저자들은 자신의 연구가 이 두 가지 능력을 분리한다고 겸손하게 주장한다. 그들은 추론 모드가 민감도를 복구할 수는 있지만, 중간 유도 단계의 정확성을 보장하지는 않는다는 점을 언급한다(예: 모델이 논리를 올바르게 전환할 수는 있지만, 추론 오류로 인해 잘못된 결론을 도출할 수 있음). 연구의 결론은 향 미래의 평가가 단순히 고정된 배경 가정에 의존하는 것이 아니라, 기술된 제약에 적응할 수 있는지를 명시적으로 테스트해야 한다는 것이다. 본 논문은 새로운 응용 분야나 미래의 구조적 변화를 제안하기보다는, 현재 모델들에 대한 진단적 평가에 집중한다.