기술 요약: 해독 가능하지만 충실하지는 않음: 프로그래밍적 검증기와 자연어 근거의 결합

문제 정의

대규모 언어 모델(LLM)은 예측에 대해 그럴듯한 자연어 근거(rationale)를 생성할 수 있지만, 이러한 설명이 모델의 내부 의사결정 과정을 충실하게(faithfully) 나타내지 못하는 경우가 많습니다. 모델은 사후적으로 결정을 '합리화'하거나, 실제 근거를 누락하거나, 생성된 텍스트에는 보이지 않는 지름길(shortcut)을 활용할 수 있습니다. 선행 연구에 따르면 사고 사슬(chain-of-thought) 프롬프팅이 작업 정확도를 향상시키기는 하지만, 생성된 설명이 반드시 인과적 추론의 증거가 되는 것은 아닙니다.

외부 프로그래밍적 검증기(예: 정리 증명기, 게임 엔진, 코드 실행기)는 주장을 확인하는 메커니즘을 제공하지만, 현재의 사용 방식은 대개 결과 수준의 감독(최종 답변 확인)에 국한되어 있습니다. 여기에는 공백이 존재합니다. 모델이 올바른 주장을 생성하더라도 동반된 설명은 근거가 없을 수 있으며, 혹은 검증기 정보를 내부적으로 인코딩하면서도 이를 일관되게 언어화하지 못할 수 있습니다. 핵심 질문은 모델의 근거 표현이 검증기에 의해 해독(decodable)되도록 강제하는 것이 생성된 설명이 모델의 추론에 충실함을 보장하는가 하는 점입니다.

방법론: 검증기 결합 추론 (Verifier-Coupled Reasoning)

본 논문은 검증된 주장과 자연어 근거 사이의 간극을 좁히기 위해 **검증기 결합 추론(Verifier-Coupled Reasoning)**이라 불리는 프레임워크를 제안합니다.

시퀀스 형식 및 목적

모델은 자연어 근거($r$)와 명시적인 인라인 주장($c$)을 포함하는 시퀀스를 다음과 같은 형식으로 생성합니다: [CONTEXT] x [RAT] r [CLAIM] c [EOS]. 프로그래밍적 검증기 $V$는 타겟 레이블 $y = V(x)$를 제공합니다 (예: 증명 수락/거절, 승률 버킷, 복잡도 클래스).

보조 일관성 헤드(consistency head)(선형 분류기)는 근거 구간의 평균 풀링된 은닉 상태($z_{rat}$)로부터 검증기의 타겟 $y$를 예측하도록 훈련됩니다. 훈련 목적 함수는 표준 다음 토큰 예측($L_{LLM}$), 선택적 주장 감독($L_{claim}$), 그리고 일관성 손실($L_{cons}$)을 결합합니다:
$$L = L_{LLM} + \lambda_{claim}L_{claim} + \lambda_{cons}L_{cons}$$

정보 흐름 제약

클레임 헤드가 근거를 우회하여 정보를 얻는 것을 방기하기 위해, 저자들은 특정 실험에서 BEC(Board-Explanation-Claim) 어텐션 마스크를 사용합니다. 이는 구조적으로 클레임 토큰이 입력 컨텍스트 토큰을 참조하는 것을 방지하여, 클레임이 오직 설명 구간에만 의존하도록 강제합니다.

진단 사다리 (Diagnostic Ladder)

본 논문은 해독 가능성(검증기 정보가 표현에 존재하는가)과 충실성(생성이 해당 정보를 반영하는가)을 구분하기 위한 다단계 진단 프레임워크를 도입합니다:

1. 해독 가능성 (Decodability): 일관성 헤드의 정확도 (검증기 레이블을 근거의 은닉 상태로부터 선형적으로 해독할 수 있는가?).
2. 역사실적 추종 (Counterfactual Following): 교체된 구간(예: 다른 레이블을 가진 근거로 교체)이 헤드의 예측을 변화시키는가?
3. 인과적 영향 (Causal Influence): 활성화 패칭(activation patching, 근거 은닉 상태를 다른 잠재 상태의 것으로 교체)이 다운스트림 클레임 로짓을 변화시키는가?
4. 생성 품질 (Generation Quality): 모델이 일관되고 충실한 설명을 생성하는가?

실험 설정

이 프레임워크는 다섯 가지 설정에서 평가됩니다:

1. 합성(Synthetic): 메커니즘을 격리하고 활성화 패칭을 통한 인과적 개입을 테스트하기 위해 통제된 잠재 상태를 사용하는 검증.
2. LeanCheck: Lean 4를 이용한 형식적 정리 증명. 역사실적 충돌 상황에서 구간별 결합(근거 vs 증명)을 테스트함.
3. KataGo: 복잡한 보드 상태에 대해 조밀한 비이진 레이블(승률 버킷)을 제공하는 바둑 엔진.
4. 코드 결합 (Code Coupling): 불충실한 생성의 실패 모드가 가장 뚜렷하게 나타나는 알고리즘적 주장(시간/공간 복잡도, 알고리즘 클래스) 설정.
5. FEVER: 실제 언어 증거 검증을 통해, 원시 정확도와 증거 민감도 사이의 트레이드오프를 테스트함.

주요 결과

1. 해독 가능성–충실성 간극 (The Decodability–Faithfulness Gap)

핵-결론은 해독 가능성이 충실성을 보장하지 않는다는 것입니다.

• 합성 및 LeanCheck: 일관성 훈련은 검증기 정보를 해독 가능하고 인과적으로 영향력 있게 만드는 데 성공했습니다. LeanCheck에서 근거 전용 및 증명 전용 풀링은 역사실적 충돌 하에서도 완벽한 방향성 분리(교체된 구간의 레이블을 100% 따름)를 달 Achieve했습니다.
• KataGo: 자연어 해설 구간은 10단계 승률 버킷을 81.1%의 정확도로 인코딩하며, 이 방법이 조밀한 비이진 도메인에서도 확장 가능함을 보여줍니다.
• 코드 (결정적 실패 모드): 코드 설정에서 모델은 98.6%의 표현 결합(representation coupling)(은닉 상태가 검증기 주장을 완벽하게 인코딩함)을 달성했음에도 불구하고, 생성된 산문은 **불충실(unfaithful)**했습니다. 모델은 구조화된 클레임 태그(예: $O(n^2)$)를 정확하게 출력하면서도, 실제 구현과는 무관한 알고리즘(예: 선택 정렬을 구현하면서 "리스트의 합"을 설명함)을 설명하는 유창하고 문법적인 설명을 내뱉습니다.
  • 이 간극은 구조적이지, 용량 문제가 아닙니다: 사전 훈련된 GPT-2와 처음부터 훈련된 모델 모두에서 동일한 결과가 관찰되었습니다.
  • 이 간극은 가중치 기반이 아닙니다: 일관성 손실 가중치($\lambda_{cons}$)를 $10^4$까지 높여도 생성 품질은 개선되지 않았는데, 이는 일관성 손실이 생성된 토큰이 아닌 표현(representation)에 작용하기 때문입니다.

2. 진단 사다리 통찰

• 인과적 영향: 합성 설정에서 근거 상태의 0번 레이어 활성화 패칭은 일관성 훈련된 경우의 73~89%에서 클레임 동작을 변화시켰습니다(대조군 31% 대비). 이는 결합이 단순 상관관계가 아닌 인과적임을 확인시켜 줍니다.
• FEVER 트레이드오프: 실제 언어 설정에서 전체 시퀀스(클레임 텍스트 포함)를 풀링하면 거의 완벽한 정확도(99%)를 보이지만, 증거 민감도를 격리하는 데는 실패합니다. 증거 전용 풀링은 정확도는 낮지만(44%) 모델이 실제로 증거를 처리하는지 더 잘 격리하여, 표준 평가에 의해 숨겨진 정확도-민감도 트레이드오프를 드러냅니다.

3. 클레임별 분석

코드 설정에서 일관성 손실은 이진 클레임보다 미세한 클레임(예: 알고리즘 클래스, 핵심 연산)에 불균형적으로 유리하게 작용합니다. 이진 클레임은 코드 구조만으로도 부분적으로 학습 가능하지만, 미세한 클레임은 높은 정확도를 위해 일관성 목적 함수에 크게 의존합니다.

의의 및 주장

본 논문은 일관성 손실이 효과적인 진단 및 표현 형성 도구이지만, 충실한 추론을 위한 충분조건은 아님을 확립합니다.

• 표현 vs 생성: 이 메커니즘은 검증기 관련 정보를 인코딩하도록 내부 표현을 형성하는 데(해독 가능성) 성공했지만, 생성된 텍스트가 검증기와 일치하도록 보상하는 생성 수준의 목적 함수가 없으면 모델은 유창하지만 불충실한 설명을 내뱉을 수 있습니다.
• 프로빙(Probing)의 한러계: 높은 프로브 정확도(해독 가능성)를 충실한 추론과 동일시해서는 안 됩니다. 모델은 은닉 상태에서 정답을 '알고' 있을 수 있지만, 출력으로는 전혀 다른 것을 '말할' 수 있습니다.
• 향후 과제: 이 간극을 좁히려면 그래디언트가 생성된 토큰에 도달하고 이들이 검증기와 일치하도록 보상하는 목적 함수가 필요합니다. 저자들은 **검증 가능한 보상을 이용한 강화학습(RLVR)**을 자연스러운 도구로 제안하며, 여기서 모델은 보조 프로브가 아니라 실제로 생성한 체크 가능한 인라인 클레임을 바탕으로 보상을 받게 됩니다.

이 연구는 추론 시스템을 평가하기 위한 엄격한 진단 사다리를 제공하며, 우리가 모델의 표현 속에 진실을 강제할 수는 있어도, 그들이 진실을 '말하게' 만드는 데는 표현 측면의 제약 이상의 것이 필요함을 입증합니다.