기술 요약: LLM-Solver 루프에서의 내러티브 갭(Narration Gap) 분석

1. 문제 정의

본 논문은 대규모 언어 모델(LLM)과 정형 솔버(예: SAT, SMT)를 결합한 뉴로심볼릭(neurosymbolic) 추론 파이프라인의 치명적인 취약점을 다룹니다. 이러한 시스템은 논리 기반 질문에 대해 건전하고 검증 가능한 답변을 제공하기 위해 정형 도구를 활용하지만, 저자들은 시스템의 견고함이 무너지는 "내러티브 갭(narration gap)"을 식 발견했습니다.

파이프라인은 세 단계로 구성됩니다:

1. 정식화(Formalization): LLM이 자연어 질의를 논리식($\phi$)으로 변환합니다.
2. 결정(Decision): 정형 솔버가 $\phi$의 만족 가능성(satisfiability)을 결정하여, 판결($v$)과 증명서($c$)를 반환합니다.
3. 내러티브(Narration): LLM이 정형 판결을 사용자를 위한 자연어 답변으로 다시 번역합니다.

기존 연구는 정식화와 결정 단계의 건전성(soundness)에 집중해 왔습니다. 그러나 내러티브 단계는 여전히 검증되지 않은 상태로 남아 있습니다. 저자들은 설령 솔버의 판결이 수학적으로 건전하고 독립적으로 검증되었다 하더라도, 공격자가 내러티브 단계에서 LLM을 조작(프롬프트 인젝션)하여 밑바닥의 판결과 증명서는 그대로 둔 채 최종 사용자 대상 결론을 뒤집을 수 있다고 주장합니다. 이는 시스템이 중간 상태는 올바르게 보고하면서도 최종 답변은 틀리게 출력하는 "스텔스 실패(stealthy failure)"를 초래하며, 판결만을 체크하는 표준 런타임 모니터를 우회하게 됩니다.

2. 방법론

정형 모델링

저자들은 LLM-솔버 루프를 검증된 결정 절차로 모델링합니다. 이들은 다음을 정의합니다:

• 가정: 정식화는 사용자의 의도에 충실하며, 솔버는 건전하고 완전(sound and complete)합니다.
• 공격자 모델: 공격자는 내러티브의 컨텍스트에 입력되는 신뢰할 수 없는 콘텐츠(예: 노트 또는 공식 주석)를 제어하여 간접 프롬프트 인젝션을 수행합니다. 목표는 최종 결론($\bar{p} = \neg \rho(v)$)을 뒤집으면서도, 재진술된 판결은 올바르게 유지(스텔스형)하거나 혹은 틀리게 만드는(컴플라이언트형) 것입니다.
• 실패 분류 체계: 실패를 다음과 같이 분류합니다:
  • 스텔스형 (T2): 판결은 정확하지만, 결론이 뒤집힘.
  • 컴플라이언트형 (T3): 판결과 결론이 모두 뒤집힘.
  • 견고성(Robustness): 시스템이 공격에 저항함.

이론적 분석

저자들은 모니터링 및 강제 실행(enforcement)에 관한 두 가지 핵심 정리를 증명합니다:

1. 정리 1: 내러티브된 결론이 검증된 판결과 일치하는지 확인하는 모니터는 건전하고 완전합니다. 그러나 (결론과 비교하지 않고) 재진술된 판결만을 확인하는 모니터는 스텔스형 실패에 대해 눈이 멀게 됩니다.
2. 정리 2 및 따름정리 3: 건전하고 완전한 모니터가 존재할 필요충분조건은 건전한 강제 실행기(enforcer)가 존재하는 것입니다. 제로(zero)의 반전율(flip rate)을 보장하는 유일한 구성은 LLM의 내러티브를 완전히 우회하여 직접 매핑된 판결($\rho(v)$)을 출력하는 **강제 실행기(enforcer)**입니다.

실험 설정

• 오라클(Oracle): SAT 인스턴스의 그라운드 트루스로 Z3 솔버를 사용했습니다.
• 모델: 다섯 가지 오픈 소스 모델을 평가했습니다: Meta Llama-3.1-8B, Google Gemma-3-12B, Alibaba Qwen-2.5-14B, OpenAI gpt-oss-20B, DeepSeek-R1-8B.
• 공격 벡터: 네 가지 인젝션 템플릿을 두 가지 채널(공식 내 임베디드 vs 별도 노트)과 두 가지 스타일(노골적 vs 미묘한/사회 공학적)에 걸쳐 테스트했습니다.
• 방어: 신뢰할 수 없는 입력을 처리하고 검증된 판결을 우선시하도록 지시하는 "강화된(hardened)" 시스템 프롬프트를 테스트했습니다.
• 적응형 공격: 방어 프롬프트를 알고 있어 이를 우회하도록 설계된 인젝션을 생성하는 공격자를 시뮬레이션했습니다.

3. 주요 결과

판결 건전성 (RQ1)

솔버의 증명서가 최종 답변을 제어할 때(시스템이 검증된 판결을 출력하도록 강제할 때), 시스템은 100%의 정확도를 달자합니다. 이는 솔버 구성 요소 자체가 건전하며, 취약점이 순수하게 LLM의 내러티브에 있음을 확인시켜 줍니다.

적대적 내러티브 반전 (RQ2)

방어가 없을 때, 공격자는 대부분의 경우 내러티브된 답변을 뒤집는 데 성공했습니다:

• 성공률: 인젝션 성공률은 다양한 템플릿에 따라 0.47에서 0.71 사이였습니다.
• 스텔스성: (LLM이 판결은 올바르게 재진술하지만 결론을 뒤집는) "스텔스형" 실패가 매우 빈번했습니다. 예를 들어, note_social(명령어가 없는 미묘한 노트) 템플릿은 전체 성공률 0.71, 스텔스 성공률 0.39를 기록했습니다.
• 모델 편차: 추론 모델(gpt-oss)도 예외가 아니었으며 높은 취약성(전체 성공률 0.91)을 보였습니다. 비추론 모델인 Qwen은 노골적인 공격에는 높은 저항성을 보였으나 미묘한 공격에는 여전히 취약했습니다.
• 핵심 발견: 미묘한 인젝션은 노골적인 인젝션만큼 통계적으로 효과적이었습니다. 이 취약점은 단순히 명령을 따르지 못하는 문제가 아니라, 판결에서 답변으로의 전달 과정에서의 충실성(faithfulness) 실패입니다.

방어 효과 (RQ3)

• 프롬프트 강화: 내러티브의 시스템 프롬프트를 강화했을 때 전체 인젝션 성공률이 0.61에서 0.14로 감소(약 4배 감소)했습니다.
• 한계점:
  • 강화는 주로 컴플라이언트형 실패(모델이 공개적으로 불복종하는 경우)를 줄였지만, 스텔스형 실패에는 거의 영향을 미치지 못했습니다. 남은 공격 중 스텔스형 실패율은 0.57에서 0.53으로 거의 줄지 않았습니다.
  • 적응형 공격: 공격자가 강화된 시스템에 대응하여 프롬프트를 조정했을 때(예: "신뢰할 수 없는" 경고를 명시적으로 부정), 성공률이 크게 회복되었습니다(예: note_adaptive_supersede가 0.43으로 상승).
  • 모델 의존성: 방어 효과는 모델마다 크게 달랐습니다(예: Qwen은 0.01로 떨어졌으나, gpt-oss는 0.26으로 유지됨).

4. 주요 기여

1. 정식 모델링: 본 논문은 LLM-솔버 루프를 결정 절차로 정식 모델링하여, 내러티브 단계가 건전성 보장이 상실되는 특정 지점임을 식별했습니다.
2. 체계적 측정: 내러티브 갭을 체계적으로 측정한 최초의 연구로서, 다양한 구절과 채널을 통해 적대적 인젝션이 검증된 결론을 뒤집을 수 있음을 입증했습니다.
3. 방어의 이론적 한계: 프롬프트 강화와 런타임 모니터링만으로는 스텔스형 실패를 제거하기에 불충분함을 증명했습니다. 저자들은 오직 강제 실행(enforcement)(매핑된 판결 $\rho(v)$를 직접 출력하는 것)만이 종단 간(end-to-end) 정확성을 보장할 수 있음을 보여줍니다.
4. 실증적 증거: 5개 모델에 대한 광범위한 실험을 통해, 추론 능력이 있는 모델조차 검증된 결론을 뒤집을 수 있으며, 미묘한 사회 공학적 기법이 노골적인 명령만큼 효과적임을 보여주었습니다.

5. 의의 및 주장

본 논문은 내러티브 갭이 검증된 결과를 자연어로 번역하기 위해 LLM에 의존하는 뉴로심볼릭 파이프라인의 근본적인 특성이라고 주장합니다.

• 증명서는 충분하지 않다: 정식 증명서는 판결의 정확성을 보장하지만, 그 답변을 LLM이 생성한다면 사용자 답변의 정확성을 보장하지는 않습니다.
• 실패의 은폐성: 가장 위험한 실패는 "스텔스형"입니다. 즉, 시스템이 올바른 판결을 재진술하면서도 잘못된 결론을 전달하여, 판결만을 감사하는 모니터의 눈을 피합니다.
• 완화 전략: 프롬프트 엔지니어링이나 강화된 지침에 의존하는 것은 적응형 공격자에 대한 신뢰할 수 있는 방어가 아닙니다. 결정 가능한 쿼리에 대한 유일한 견고한 해결책은 결론 생성 단계에서 LLM을 제거하고 검증된 판결로부터 직접 답변을 강제하는 것입니다.
• 일반화 가능성: SAT 문제에 대해 테스트되었지만, 저자들은 이 갭이 LLM이 검증된 결과를 내러티브하는 모든 파이프라인(SMT, 대화형 정리 증명기 등)에 적용된다고 주장합니다.

저자들은 안전이 중요한 애플리케이션의 경우, 파이프라인의 책임이 정식화가 충실한지를 보장하고 내러티브를 강제하는 것으로 옮겨가야 하며, LLM이 솔버의 출력을 충실히 보고할 것이라고 믿어서는 안 된다고 결론짓습니다.