기술 요약: (직관주의) 차기 토큰 예측의 논리

문제 제념

본 논문은 현재의 기초 생성형 AI 모델, 특히 트랜스포머(Transformer)가 가진 논리적 투명성의 결여 문제를 다룬다. 트랜스포머는 방대한 데이터셋에 대한 비지도 학습을 통해 차기 토큰 예측을 효과적으로 학습하지만, 위치 인코딩(positional encodings)과 유사도 기반 어텐션(attention) 메커니즘에 대한 의존도는 시퀀스 예측의 기저에 깔린 논리적 구조를 모호하게 만든다. 저자는 차기 토큰 예측 작업이 단순한 통계적 패턴 매칭이 아니라, 직관주의 함축 논리(intuitionistic implicational logic) 내에서의 구성적 증명 완성(constructive proof completion) 과제로 재해석될 수 있다고 상정한다. 핵심 과제는 어텐션 메커니즘을 순서를 본질적으로 인코딩하는 연산자 합성(operator composition)으로 대체하여, 논리적 해석을 자연스럽게 구현하는 신경망 아키텍처를 도출하는 것이다.

방법론

1. 논리적 형식론: 좌측 중첩 함축 (Left-Nested Implication)

저자는 토큰 시퀀스를 좌측 중첩 직관주의 함축으로 모델링할 것을 제안한다. 우측 중첩 함축(right-nested implications)이 결합(conjunction)으로 붕괴되어 순서 불변성을 갖는 것과 달리, 좌측 중첩 함축은 순서 민감성을 보존한다.

• 표현: 토큰 시퀀스 $w_1, \dots, w_n$은 $L_n = ((((w_1 \to w_2) \to w_3) \to \dots) \to w_n)$와 같이 인코딩된다.
• 추론 메커니즘: 차기 토큰 예측은 **긍정 논법(Modus Ponens)**으로 매핑된다. 접두사 함축 $I_p$와 전체 함축 $I_f = (I_p \to w)$가 주어졌을 때, $w$를 예측하는 것은 제거 단계 $I_f \to (I_p \to I_f) \to w$에 대응한다.
• 커리-하워드 대응 (Curry-Howard Correspondence): 이 동형 사상(isomorphism) 하에서 명제는 타입(type)이고, 증명은 $\lambda$-항(term)이며, 차기 토큰 예측은 함축적 타입을 점유하는 항을 구성하는 과정이다. 시퀀스를 예측하는 과정은 연속적인 $\beta$-축약(state updates)으로 간주된다.

2. 이론적 도구

저자는 명제 직관주의 논리의 함축 파편으로 제한된 시퀀트 계산법인 Roy Dyckhoff의 LJT 계산법을 활용한다. 저자는 다음을 수행하기 위해 특화된 프롤로그(Prolog) 기반 정리 증명기(lprove/2)를 구현하였다:

• 논리적 인코딩의 건전성(soundness) 검증.
• 좌측 중첩 체인에서 순서가 보존됨을 입증 (예: $((p \to q) \to r)$은 $((q \to p) \to r)$과 동등하지 않음).
• 문장 파편을 저장된 함축 체인의 부분 공식(subformula, 즉 접두사의 접미사)으로 취급하여 정보 검색 수행.

3. 신경망 아키텍처: 애로우 언어 모델 (The Arrow Language Model)

저자는 논리적 증명 구성을 수치적으로 구현한 재귀적 신경망 아키텍처인 **애로우 모델(Arrow Model)**을 도출한다.

• 은닉 상태로서의 증명 문맥 (Hidden State as Proof Context): 접두사를 처리한 후의 누적된 증명 문맥(가정 및 정당화)을 나타내는 은닉 상태 $h_t \in \mathbb{R}^d$.
• 연산자로서의 토큰 (Tokens as Operators): 각 토큰 $t$는 현재 상태를 변환하는 선형 연산자 $M_t: \mathbb{R}^d \to \mathbb{R}^d$로 작용하며, 이는 가산적 임베딩(additive embeddings) 대신 사용된다.
• 저계수 매개변수화 (Low-Rank Parameterization): 대규모 어휘집을 효율적으로 처리하기 위해, 연산자는 $M_t = I + U \text{diag}(s_t) V^\top$로 정의된다. 여기서 $U, V$는 공유 행렬이며 $s_t$는 임베딩으로부터 유도된 토큰 특화 게이트 벡터이다.
• 상태 업데이트 (Modus Ponens): 재귀 관계는 함축 제거를 구현한다:
  $$h_{t+1} = \text{LayerNorm}(h_t + U((V^\top h_t) \odot s_t))$$
  이 업데이트는 비가환적($M_a M_b \neq M_b M_a$)이며, 이는 연산자 합성의 대수(algebra)에 의해 토큰 순서가 본질적으로 인코딩됨을 의미한다. 따라서 명시적인 위치 인코딩이 필요 없다.
• 학습 (Training): 모델은 교사 강요(teacher forcing)를 사용하여 표준 차기 토큰 교차 엔트로피를 사용한다. 대규모 어휘집에 대한 메모리 관리를 위해 손실은 스트리밍 방식으로 계산된다.

주요 기여

1. 차기 토큰 예측의 논리적 해석: 본 논문은 차기 토큰 예측이 직관주의 함축 논리에서 구성적 증명 확장(Modus Ponens)과 동등하다는 공식적인 대응 관계를 확립한다.
2. 애로우 모델의 도출: 토큰을 정적 임베딩이 아닌 상태 변환 연산자로 기능하게 하는, 증명론적 해석에서 직접 도출된 새로운 재귀적 아키텍처를 제시한다.
3. 위치 인코딩 없는 순서 민감성: 비가환적 연산자 합성이 시퀀스 순서를 본질적으로 인코딩함을 보여줌으로써, 트랜스포머에서 사용하는 위치 인코딩 전략에 대한 대안을 제시한다.
4. 기호-신경 결합 검색 프레임워크: 기호적 검색(함축 체인에 대한 Prolog 정리 증명)과 신경적 검색(Arrow 모델)이 동일한 기저 논리 구조 위에서 작동하는 통합 프레임워크를 보여준다.

실험 결과

저자는 Project Gutenberg의 공공 도메인 텍스트를 사용하여 논리 기반 알고리즘과 그 신경적 등가물을 검증하는 실험을 수행하였다.

• 설정: 모델의 학습 능력과 아키텍처 효율성을 검증하기 위해 소규모 코퍼스(예: 오즈의 마법사, 모비 딕)에 과적합(overfit)되도록 설계된 "새니티 체크(Sanity Check)" 체제를 활용하였다.
• 데이터 증강: 논리 수준의 부분 공식 검색을 모사하기 위해, 모든 문장의 연속된 파편들을 학습 세트에 추가하였다.
• 성능:
  • 학습 효율성: 애로우 모델은 대규모 문서(예: 약 56만 단어의 전쟁과 평화)를 단일 소비자용 GPU(RTX 3090)에서 8분 미만 만에 학습하였다.
  • 추론: 검색 우선 파이프라인(후보 열거 후 신경망 점수 산출)은 쿼리당 0.1~0.3초의 추론 시간을 달성하였으며, 이는 전체 코퍼스의 크기와 거의 무관하였다.
  • 기호적 베이스라인: 프롤로그 기반 검색 시스템은 빠른 데이터베이스 초기화(1~2초)와 대화형 쿼리 시간(약 0.5초)을 보여주어, 논리 수준의 검색을 해석 가능한 베이스라인으로 사용하는 것이 타당함을 확인하였다.

의의 및 주장

본 논문은 애로우 언어 모델을 유사도 기반 어텐션(트랜스포머)이나 컨볼루션/상태 공간 대안과는 구별되는, 차기 토큰 예측을 위한 **논리 우선 기초(logic-first foundation)**로 제시한다.

• 설명력: 신경망 연산을 증명론적 개념(함축 제거, $\beta$-축약)에 매핑함으로써, 모델은 트랜스포머가 결여하고 있는 신경 역학과 기호적 추론 사이의 설명적 연결을 제공한다.
• 아키텍처적 관점: 애로우 모델은 순서 민감성과 구성적 증명 확장이 중요한 작업에 대한 논리 기반 대안으로 위치하지만, 저자는 이것이 아직 일반적인 환경에서 파운데이션 모델을 대체할 수 있는 즉각적인 교체 모델은 아니라고 명시한다.
• 한계: 저자는 현재의 연구가 정확한 연속적 하부 구조에 집중하고 있음을 인정한다. 오타 처리, 의역, 또는 비연속적 증거 처리와 같은 현대 언어 모델링의 강건성 요구 사항은 향후 과제로 남겨두었다.
• 향러 방향: 트랜스포머 방식의 추론(근사 매칭)을 유사한 논리 기반 기술로 에뮬레이션하는 것을 핵심적인 개방형 과제로 식별하였다.

이 연구는 시퀀스 예측의 논리적 구조가 직관주의 논리를 통해 명시적이고 구성적으로 만들어질 수 있다는 직관에 근거하여, 트랜스포머 기반 파운데이션 모델의 대안을 향한 한 단계로 제시된다.