기술 요약: 다음 토큰 예측을 좌측 중첩 직관주의 함의로 모델링하기

문제 정의

트랜스포머를 포함한 파운데이션 생성형 AI 모델들은 대규모 데이터셋을 통해 비지도 학습된 다음 토큰 예측에 의존한다. 효과적이기는 하나, 표준 트랜스포머 아키텍처는 시퀀스 예측의 논리적 구조를 은폐한다. 이는 토큰을 어텐션 메커니즘을 통해 혼합되는 가산적 임베딩(additive embeddings)으로 취급하며, 순서를 포착하기 위해 명시적인 위치 인코딩(positional encodings)을 필요로 한다. 이러한 접근 방식은 기호적 추론이나 구성적 증명 도출의 성격과 연결되는 설명력을 제한적으로 제공한다. 본 논문은 근본적인 질문을 던진다: 다음 토큰 예측을 직관주의 명제 논리의 증명 확장으로 이해할 수 있는가? 그리고 이러한 해석이 가산적 임베딩이나 명시적 위치 인코딩에 의존하지 않고도 실행 가능한, 순서 민감형 신경망 아키텍처를 산출할 수 있는가?

방법론

저자들은 직관주의 논리 해석에 기반한 다음 토큰 예측 모델인 **애로우 언어 모델(Arrow Language Model)**을 제안한다. 방법론은 기호 논리 유도, 정리 증명, 그리고 신경망 실현의 과정을 거친다.

1. 논리적 형식화: 좌측 중첩 함의

핵심 통찰은 토큰 시퀀스 $w_1, \dots, w_n$을 집합이나 (결합론 하에서 순열 불변인) 우측 중첩 체인이 아니라, **좌측 중첩 함의 체인(left-nested implication chain)**으로 표현하는 것이다:
$$L_n = ((((w_1 \to w_2) \to w_3) \to \dots) \to w_n)$$
직관주의 논리에서 이 구조는 순서 민감적이다. 즉, 토큰을 치환하면 전제의 함수적 타입(functional type)이 변한다.

• 모두스 포넨스(Modus Ponens)로서의 다음 토큰 예측: 접두사 $P$가 주어졌을 때 다음 토큰 $w$를 예측하는 것은 논리적 추론 $P \to w$에 대응한다. 만약 접두사가 함의 체인 $I_p$로 표현되고 전체 시퀀스가 $I_f = (I_p \to w)$라면, $w$를 도출하는 것은 모두스 포넨스의 한 사례가 된다.
• 커리-하워드 대응(Curry–Howard Correspondence): 이 동형 사상(isomorphism) 하에서 명제는 타입이며, 증명은 $\lambda$-항(term)이다. 접두사는 부분 적용된 $\lambda$-항이며, 다음 토큰을 예측하는 것은 추가적인 함수 적용을 가능하게 하기 위해 인자를 공급하는 것이다(함의 제거).

2. 정리 증명 및 기호적 검색

저자들은 (Roy Dyckhoff의 LJT 계산법을 구현하는) 특화된 Prolog 기반 정리 증명기를 사용하여 이러한 함의 체인의 속성을 검증한다.

• 정리: 이들은 좌측 중첩 체인이 단일 단계 및 다단계 예측을 모두 지원함을 입증한다. 예를 들어, 정리는 접두사가 어떻게 재사용 가능한 연속 연산자(continuation operators)로 "컴파일"될 수 있는지 보여준다 (예: $((E \to a) \to b) \to c$를 $b$를 생성한 후 $c$를 생성하는 규칙으로 변환).
• 정보 검색: 문장들을 함의 체인으로 저장하는 기호적 검색 메커니즘이 구현된다. 쿼리(부분 시퀀스)는 데이터베이스로부터 정확한 완성을 검색하기 위한 부분 공식(subformula) 역할을 수행하며, 이는 논리 기반의 베이스라인 역할을 한다.

3. 신경망 실현: 애로우 모델

논문의 논리적 구조를 반영하는 순환 신경망 아키텍처를 도출한다:

• 은닉 상태와 증명 문맥: 은해 상태 $h_t \in \mathbb{R}^d$는 접두사를 소비한 후 축적된 증명 문맥(proof context)을 나타낸다.
• 토큰으로서의 연산자: 가산적 벡터 대신, 각 토큰 $t$는 현재 상태를 변환하는 선형 연산자 $M_t$로 작의한다.
• 저계수 매개변수화(Low-Rank Parameterization): 거대 어휘집을 처리하기 위해, 연산자는 다음과 같은 저계수 업데이트로 정의된다:
  $$M_t = I + U \text{diag}(s_t) V^\top$$
  여기서 $U, V$는 공유 행렬이며, $s_t$는 임베딩 룩업에서 유도된 토큰 특이 게이트 벡터이다.
• 상태 업데이트 (모두스 포넨스): 이 순환 구조는 함의 제거를 구현한다:
  $$h_{t+1} = \text{LayerNorm}(h_t + U((V^\top h_t) \odot s_t))$$
  이 업데이트는 본질적으로 비가환적($M_a M_b \neq M_b M_a$)이며, 위치 인코딩 없이 순서를 내재적으로 인코딩한다.
• 학습: 모델은 교사 강요(teacher forcing)를 사용하여 표준 다음 토큰 교차 엔트로피로 학습된다. 손실은 일반 GPU에서 메모리를 관리하기 위해 스트리밍 방식으로 계산된다.

주요 기여

1. 논리 기반 유도: 본 논문은 좌측 중첩 직관주의 함의의 깊이와 순환 계산 단계 사이의 공식적인 대응 관계를 확립함으로써, 시퀀스 모델링에 대한 증명론적 토대를 제공한다.
2. 애로우 아키텍처: 토큰을 가산적 벡터가 아닌 상태 변환 연산자로 취급하는 특정 신경망 아키텍처를 도입하여, 유도 편향(inductive bias)을 "어텐션을 통한 검색"에서 "합성을 통한 변환"으로 전환한다.
3. 기호-신경 브릿지: 기호적 정리 증명(단일화를 통한 정확한 검색)과 신경적 예측(학습된 연속성 점수를 통한 근사적 검색) 사이의 긴밀한 연결을 보여준다.
4. 순서에 대한 이론적 분석: 좌측 중첩 함의는 순서를 자연스럽게 보존하는 반면, (위치 인코딩이 없는 표준 어텐션 공식에서 흔히 나타나는) 우측 중첩 함의는 그렇지 않음을 증명한다.

실험 결과

실험은 일반적인 벤치마크에서 최첨단 언어 모델과 경쟁하기보다는, 순서 민감형 패턴을 학습하는 아키텍처의 능력과 기호적 검색을 모방하는 능력을 검증하는 데 집중한다.

• 과적합/건전성 검사: 모델은 작은 데이터셋(Project Gutenberg 텍스트)에 대해 의도적인 과적합 회귀를 통해 테스트되었다. 학습 세트는 논리 수준의 검색(subformula retrieval)을 모방하기 위해 모든 연속적인 문장 파편들로 증강되었다.
• 성능: 모델은 작은 규모의 문서(예: 오즈의 마법사, 모비 딕)에 대해 단일 RTX 3090 GPU에서 몇 분 내에 거의 제로에 가까운 훈련 손실을 달성하며 성공적으로 과적합되었다.
• 검색 대 생성:
  • 기호적 베이스라인: Prolog 기반 검색은 저장된 함의 체인에 대해 쿼리에 대한 정확한 일치를 달성했다.
  • 신경적 모사: 애로우 모델은 접두사로 쿼리되었을 때, 학습된 연속성 점수를 바탕으로 후보 접미사 완성을 순위 매길 수 있었으며, 이는 논리적 검색 과정을 효과적으로 모사했다.
  • 자유 생성: 모델은 정확히 암기된 일치 항목 너머로 유창한 지속 문장을 생성할 수 있었으며, 이는 연산자 합성이 일반화 가능한 순차적 구조를 학습했음을 보여준다.
• 확장성: 모델의 훈련 처리량은 시퀀스 길이에 대해 선형적이었으며, 스트리밍 손실 계산 덕분에 책 한 권 분량의 코퍼스(예: 전쟁과 평화)까지도 관리 가능한 메모리 사용량으로 확장 가능했다.

의의 및 주장

본 논문은 유사도 기반의 어텐션이나 컨볼루션/상태 공간 대안과는 구별되는, 다음 토큰 예측을 위한 논리 우선적 기초를 제공한다고 주장한다.

• 내재적 순서: 연산자 합성을 통해 순서를 인코딩함으로써, 애로우 모델은 명시적 위치 인코딩의 필요성을 제거하고 아키텍처를 증명 확장의 구성적 성격에 더 가깝게 정렬한다.
• 설명 가능성: 이 아키텍처는 직관주의 논리와 직접적인 매핑을 제공하며, 여기서 상태 업데이트는 증명 단계(모두스 포넨스)에, 은닉 상태는 증명 문맥에 대응한다. 이는 더 해석 가능한 신경 모델로 가는 잠재적 경로를 제시한다.
• 대안적 패러다임: 이 연구는 자신을 트랜스포머 기반 파운데이션 모델의 실행 가능한 대안으로 위치시키며, 곱셈적 RNN(애로우 모델이 닮은 형태)이 시퀀스 예측에 대한 증명론적 해석으로부터 자연스럽게 발생함을 시사한다.

저자들은 현재의 실험이 정확한 연속적 부분 구조에 의존하고 있음을 언급하며, 노이즈가 있는 실제 프롬프트에 대한 일반화 능력에 대해서는 신중한 태도를 유지한다. 그들은 이 작업을 "트랜스포머에 대한 증명론적 설명"을 향한 단계로 규정하며, 어텐션 메커니즘이 근사적 함의 제거 및 소프트 가설 선택으로 해석될 수 있다는 향후 방향을 제시한다.