기술 요약: LLM은 프로그래밍 언어의 의미론이 아닌 사전 지식(Priors)에 의존한다

문제 정의

현재 대규모 언어 모델(LLM)은 프로그램의 동작을 추론하는 데 필요한 작업(예: 출력 예측, 코드 수정, 코드 생성 등)을 해결하기 위해 점점 더 많이 배치되고 있습니다. 그러나 근본적인 미해결 과제가 남아 있습니다. 이 모델들이 사전 학습을 통해 습득한 통계적 규칙성(어휘적 사전 지식)에 주로 의 Rely하는지, 아니면 명시적으로 제공된 행동 규칙에 따라 유연하게 추론을 조건화할 수 있는지 여부입니다.

LLM은 표준적인 프로그래밍 작업에서는 종종 우수한 성능을 보이지만, 학습된 데이터로부터의 확고한 사전 지식과 충돌하는 외부 지정 형식 체계에 자신의 추론을 적응시킬 수 있는지는 불분명합니다. 예를 들어, 만약 기호 '+'가 제공된 규칙 세트 내에서 뺄셈을 수행하도록 명시적으로 정의된다면, 사전 지식에 의존하는 모델은 여전히 덧셈을 출력하겠지만, 규칙에 따라 조건화된 모델은 적응할 것입니다. 본 논문은 LLM이 프로그램 실행을 통해 형식적 의미론에 자신의 추론을 조건화할 수 있는지 조사하며, 특히 공급된 추론 규칙을 위해 학습된 기호-의미 연관성을 덮어쓸 수 있는지 테스트합니다.

방법론

저자들은 제어된 분포 변화 하에서 규칙 기반 추론을 조사하기 위해 설계된 의미론 중심 벤치마크인 PLSEMANTICSBENCH를 소개합니다. 방법론은 세 가지 핵심 구성 요소로 이루어집니다.

1. 형식주의 및 언어

이 벤치마크는 C에서 파생되었으나 구문적 모호성을 피하기 위해 단순화된(예: Python에서 발견되는 들여쓰기 민감도 문제를 피하기 위해 명시적인 블록 구분자 {} 사용) 경량 임페러티브 언어인 **C⋆**를 활용합니다. 이 언어는 두 가지 구별된 형식적 의미론 체계와 쌍을 이룹니다:

• Small-step 구조적 운영 의미론 (S): 각 규칙이 하나의 원자적 계산 단계를 나타내는 세밀한 시스템입니다.
• K 의미론 (K): 더 거친 수준의 리라이팅(rewriting) 기반 시스템입니다.

이러한 형식주의는 프로그램의 표면 구문을 변경하지 않고도 규칙 정의를 체계적으로 변경할 수 있게 합니다.

2. 의미론적 변화 및 스트레서(Stressors)

구문적 친숙함과 의미론적 추론을 분리하기 위해, 벤치마크는 두 가지 유형의 의미론적 변이를 도입합니다:

• KeywordSwap: 선택된 구문 연산자(예: +, -)가 그 의미 해석을 교환합니다. 예를 들어, +가 뺄셈을 수행하도록 정의됩니다. 이는 사전 학습된 사전 지식과 직접적인 충돌을 일으키면서도 표면 구문은 보존합니다.
• KeywordObf: 표준 키워드 및 연산자가 제공된 규칙에 의해서만 의미가 정의되는 새로운 기호(코카서스-알바니아 스크립트에서 추출)로 대체됩니다. 이는 모든 구문적 사전 지식을 제거합니다.

벤치마크는 증가하는 구조적 복잡도에 따라 세 가지 데이터셋 분할을 통해 평가합니다:

• Human-Written: 표준 코딩 벤치마크(LeetCode, HumanEval 등)에서 적응된 프로그램.
• LLM-Translated: LLM에 의해 C⋆로 번역된 C++ 솔루션.
• Fuzzer-Generated: 제어 흐름 및 데이터 흐름 복잡도를 극대화하기 위해 깊이 제어 기능이 있는 의미론 인식 퍼저(fuzzer)에 의해 자동 생성된 프로그램.

3. 평가 작업

벤치마크는 네 가지 가설에 대한 모델의 능력을 조사합니다:

• H1 (전역 규칙 조건화): 모델이 최종 프로그램 상태를 올바르게 예측하기 위해 많은 규칙 적용을 합성할 수 있는가? (작업: PredState)
• H2 (상태 독립 규칙 조건화): 프로그램 상태가 변하지 않을 때 모델이 올바른 운영 규칙을 선택할 수 있는가? (작업: PredRule)
• H3 (장기 실행 경로 규칙 조건화): 모델이 긴 실행 트레이스(루프, 중첩된 제어 흐름) 동안 규칙 기반 추론을 유지할 수 있는가? (작업: PredTrace)
• H4 (의미론적 변화 하의 규칙 조건화): 모델이 사전 지식과 충돌하는 새로운 의미론 하에서도 제공된 규칙을 계속 따르는가?

연구는 비-추론 모델(예: Llama-3.3, Qwen2.5-Inst)과 추론 지향 모델(예: DeepSeek-R1 변체, O3-mini, GPT-5-mini, Gemini-2.5-pro)을 포함한 11개의 프런티어 LLM을 평가합니다.

주요 기여

1. PLSEMANTICSBENCH: 프로그램 실행을 제어된 프로브(probe)로 활용하여, LLM이 통계적 사전 지식이 아닌 형식적 규칙에 추론을 조건화하는지 테스트하도록 명시적으로 설계된 최초의 대규모 벤치마크입니다.
2. 형식적 의미론적 변화: KeywordSwap 및 KeywordObf 변환을 도입하여, 규칙 구조는 보존하면서 기호-의미 매핑을 체계적으로 교란함으로써 어휘적 연관성과 형식적 정의 간의 의존성을 격리했습니다.
3. 세밀한 추론 분석: 프로그램 실행 추론을 전역 상태 예측, 로컬 규칙 선택, 장기 실행 경로 생성으로 분해하여 현재 모델들의 구체적인 실패 모드를 밝혀냈습니다.
4. 포괄적 경험적 평가: 11개 모델, 3가지 데이터셋 복잡도, 2가지 의미론 형식을 가로지르는 체계적인 평가를 통해 현재의 능력과 한계에 대한 상세한 지도를 제공합니다.

결과

실험은 몇 가지 중요한 발견을 도출합니다:

• 사전 지식에 대한 의존: 표준 의미론 하에서 많은 모델은 단순한 작업에 대해 높은 정확도(최대 90%)를 달성합니다. 그러나 의미론적 변이(KeywordSwap)가 발생하면 성능이 40~60 퍼센트 포인트 급격히 떨어집니다. 이는 모델이 제공된 형식 규칙보다는 사전 학습된 어휘적 연관성에 주로 의존함을 나타냅니다.
• 의미론적 변화 민감도: KeywordSwap 변이는 KeywordObf보다 훨씬 더 큰 성능 저하를 유발합니다. 이는 익숙한 구문(의미가 바뀌더라도)의 존재가 강력한 사전 지식 기반 반응을 유발하며, 모델이 이를 극복하지 못함을 시사합니다.
• 장기 실행 경로의 취약성: 긴 실행 트레이스에 걸쳐 규칙 기반 추론을 유지하는 것은 매우 취약합니다. 극소수의 모델만이 PredTrace 작업에서 0이 아닌 정확도를 달성하며, 가장 우수한 시스템조차 약 35%의 정확도에 그칩니다. 대부분의 모델은 수십 단계에 걸쳐 상태를 추적하고 규칙을 반복 적용해야 할 때 정확도가 0으로 수렴합니다.
• 복잡도의 영향: 구조적 복잡성(제어 흐름 깊이, 데이터 흐름 의존성)이 증가함에 따라 성능이 체계적으로 악화됩니다. 추론 지향 모델은 단순한 인간 작성 프로그램에서 형식 규칙의 이점을 얻지만, 복잡한 퍼저 생성 프로그램에서는 이 이점이 사라지거나 역전되기도 합니다.
• Chain-of-Thought (CoT)의 한 한계: CoT 프롬프팅은 비-추론 모델의 표준 의미론 성능을 높여주지만, 의미론적 스왑에 의해 도입된 편향을 극복하는 데는 실패합니다. 이는 추론 과정(reasoning traces) 자체가 정착된 연산자 사전 지식을 극복할 수 없음을 나타냅니다.
• 표기법 이해: 모델은 일반적으로 형식적 표기법 자체를 이해하는 데 높은 능력을 보여줍니다 (NL→Rule 및 Rule→NL 작업). 이는 실행 작업에서의 실패가 추론 능력의 한계에서 비롯된 것이지, 형식론을 파싱하는 능력의 부재 때문이 아님을 시사합니다.

의의 및 주장

본 논문은 **추론 규칙 조건화(inferential rule conditioning)**를 학습 기반 시스템의 미해결된 능력 축으로 규정합니다. 저자들은 현대 LLM이 데이터에서 유도된 사전 지식과 충돌할 때, 외부로 지정된 형식 시스템에 자신의 추론을 조건화하는 데 자주 실패한다고 주장합니다.

이 연구의 의의는 다음과 같습니다:

1. 진단 능력: LLM의 통계적 패턴 매칭과 진정한 규칙 준수를 구분할 수 있는 엄격한 방법을 제공합니다.
2. 한계 식별: 현재 모델들이 연산자 오버로딩, 도메인 특화 언어(DSL), 형식 검증과 관련된 애플리케이션에 필수적인, 새로운 형식 의미론에 적응하는 견고함이 부족함을 강조합니다.
3. 미래 방향 제시: "정착된 어휘적 연관성"에 대한 의존을 넘어, 제공된 규칙에 기반하여 진정한 조건부 추론을 수행할 수 있는 시스템으로 나아가기 위한 동기를 부여합니다.

저자들은 LLM이 표준 실행 작업에서는 유망한 모습을 보이지만, 명시적인 형식 규칙에 자신의 추론을 조건화하는 능력은 특히 의미론적 변화와 긴 실행 경로 하에서 여전히 중요한 병목 구간으로 남아 있다고 결론짓습니다.