논문 요약: 범주화된 신경 아키텍처에서 초지수적 증명 이론으로 (From Categorized Neural Architectures to Subexponential Proof Theory)

1. 연구 배경 및 문제 정의

기존의 범주론적 머신러닝 연구는 주로 학습 시스템의 합성 (composition) 과 역전파 (backpropagation) 를 범주론적 의미론으로 설명하는 데 초점을 맞추어 왔습니다. 또한, 범주론적 논리 (Categorical Logic) 는 범주의 구조적 특성이 어떻게 논리 체계나 증명 시스템으로 이어지는지 연구해 왔습니다.

그러나 신경 아키텍처에서 직접적으로 논리를 추출하는 연구는 부족했습니다. 대부분의 접근법은 이미 완성된 논리 체계 (예: 선형 논리) 를 가정하고 이에 맞는 의미론을 찾는 방식이었습니다. 본 논문은 이러한 방향을 반대로 전환하여, 리소스 민감성 (resource-sensitivity) 을 가진 신경 아키텍처의 범주론적 구조에서 출발하여, 해당 구조가 강제하는 논리적 규칙 (증명 이론) 을 추출하는 것을 목표로 합니다.

주요 문제는 다음과 같습니다:

• 신경 아키텍처의 다양한 메모리 및 컨텍스트 행동 (예: 정보의 재사용, 폐기, 선형적 사용, 영역 간 강제 변환) 을 어떻게 범주론적으로 모델링할 것인가?
• 이 모델링된 구조에서 어떻게 초지수적 (subexponential) 논리 서명 (signature) 을 추출할 수 있는가?
• 추출된 증명 시스템이 원래 아키텍처의 구조적 제약을 정확히 반영하는지 (정합성, Soundness) 어떻게 증명할 것인가?

2. 방법론: 아키텍처 → 범주 → 논리 파이프라인

저자는 다음과 같은 4 단계의 구성 과정을 제시합니다:
신경 아키텍처 패밀리 → 범주화된 아키텍처 → 초지수적 서명 → 증명 이론

2.1. 범주화된 아키텍처 (Categorized Architectures)

• 타입 리소스 컨텍스트 (Typed Resource Context): 각 입력/출력에 '영역 (Zone, $z$)' 레이블이 붙은 타입의 리스트로 정의됩니다. 이는 메모리, 컨텍스트, 현재 관측치 등 서로 다른 역할을 구분합니다.
• 파라미터화된 리소스 블록 (Parametrised Resource Block): 입력 컨텍스트를 받아 출력 컨텍스트로 변환하는 계산 블록으로, 파라미터 객체 $P$와 사상 $\phi: P \times [[\Gamma]] \to [[\Delta]]$로 정의됩니다.
• 아키텍처 범주 ($Arch_Z$): 위 블록들의 동치류 (isomorphism classes) 를 사상으로 하는 범주를 정의합니다. 이 범주는 대칭 모노이달 (symmetric monoidal) 구조를 가지며, 블록의 직렬 및 병렬 합성을 지원합니다.

2.2. 일관된 영역 규율 (Coherent Zone Discipline)

단순한 범주 구조만으로는 논리적 규칙 (약화, 축소 등) 을 결정할 수 없으므로, 아키텍처가 허용하는 구조적 연산을 명시하는 규율 (Discipline) 을 도입합니다.

• 영역 순서 (Preorder): 영역 간의 강제 변환 (coercion, $\chi_{z,z'}$) 을 정의합니다.
• 허용된 구조적 연산:
  • 폐기 (Weakening/Discard): 특정 영역 $z$에서 정보를 버릴 수 있는지 ($\omega_{z,A}$).
  • 축소 (Contraction/Diagonal): 특정 영역 $z$에서 정보를 복제할 수 있는지 ($\delta_{z,A}$).
• 이 규율은 아키텍처 설계자가 "어떤 영역의 정보는 재사용 가능하고, 어떤 것은 일회성인지"를 범주론적으로 인코딩합니다.

2.3. 초지수적 서명 추출 (Extraction of Subexponential Signature)

정의된 규율 ($Lic$) 에서 초지수적 서명 (Subexponential Signature) $\Sigma_{Lic} = (Z, \preceq, W, C)$을 자동으로 추출합니다.

• $Z$: 영역 집합.
• $\preceq$: 영역 간의 순서.
• $W$: 약화 (Weakening) 가 허용되는 영역 집합 (폐기 가능).
• $C$: 축소 (Contraction) 가 허용되는 영역 집합 (복제 가능).
• 핵심 결과: 이 서명은 외부에서 강제된 것이 아니라, 아키텍처의 구조적 허가 (licensed structural families) 에서 정확히 재구성 (reconstructed) 됩니다.

2.4. 추출된 증명 이론 (Extracted Proof Theory)

추출된 서명 $\Sigma_{Lic}$을 기반으로 텐서 시퀀트 계산 (Tensorial Sequent Calculus, $TZ_{\Sigma}$) 을 정의합니다.

• 단어: 원자, 텐서 단위 ($I$), 텐서 곱 ($\otimes$).
• 규칙:
  • 표준 규칙: 공리, 텐서 곱의 도입/소거, 단위 규칙.
  • 영역 인덱스된 구조 규칙: $z \in W$인 경우에만 약화 규칙 ($W_z$), $z \in C$인 경우에만 축소 규칙 ($C_z$) 이 적용됩니다.
• 절단 제거 (Cut Elimination): 이 계산 시스템에서 절단 (cut) 규칙이 제거 가능함을 증명합니다.

3. 주요 기여 및 결과

1. 범주론적 아키텍처의 정의 및 대칭 모노이달성 증명:

   • $Arch_Z$ 범주를 정의하고, 이것이 대칭 모노이달 범주임을 증명했습니다. 이는 신경 블록의 합성이 범주론적으로 잘 정의됨을 의미합니다.

2. 일관된 영역 규율과 구조적 서명의 정합성:

   • 아키텍처에 부여된 규율 ($Lic$) 에서 약화/축소 영역을 추출했을 때, 원래 의도된 영역 집합과 정확히 일치함을 증명했습니다 (Theorem 2.18). 즉, 논리적 서명은 아키텍처의 구조적 제약에서 자연스럽게 도출됩니다.

3. 절단 제거 (Cut Elimination) 증명:

   • 추출된 텐서 계산 시스템 $TZ_{\Sigma}$에서 모든 도출 가능한 시퀀트에 대해 절단 없는 증명이 존재함을 증명했습니다. 이는 시스템의 일관성과 계산적 의미를 보장합니다.

4. 정합성 (Soundness) 정리:

   • 추출된 증명 시스템의 모든 도출 (derivation) 이 원래 범주화된 아키텍처의 허용된 다이어그램 (licensed diagrams) 에 의해 해석됨을 증명했습니다.
   • 특히, 논리적 규칙 (약화, 축소) 은 아키텍처에서 명시적으로 허가된 폐기 및 복제 사상과 직접적으로 매핑됩니다.

5. 구체적 예시 (Two-Block Neural Architecture):

   • 지속적 메모리 (Persistent), 관련성 있는 컨텍스트 (Relevant), 선형 입력 (Linear) 을 가진 간단한 신경 아키텍처를 예로 들어, 아키텍처의 리소스 정책이 어떻게 특정 논리 규칙 (예: 지속적 메모리는 복제/폐기 가능, 선형 입력은 불가능) 으로 변환되는지를 구체적으로 보여주었습니다.

4. 의의 및 결론

이 논문은 **"신경 아키텍처 → 범주 → 논리"**라는 새로운 연구 프로그램의 첫 번째 엄밀한 단계를 제시합니다.

• 방향성의 전환: 기존의 "논리 → 의미론" 접근이 아니라, "아키텍처 → 범주 → 논리" 접근을 취함으로써, 신경망의 구조적 제약이 어떤 논리적 법칙을 강제하는지를 규명했습니다.
• 리소스 민감성의 정량화: 신경망의 다양한 입력 유형 (메모리, 컨텍스트, 관측치) 을 '영역 (Zone)'으로 구분하고, 각 영역의 리소스 사용 정책 (재사용, 폐기, 선형성) 을 논리 규칙으로 정밀하게 매핑했습니다.
• 수학적 엄밀성: 단순한 유추를 넘어, 범주론적 구조에서 증명 이론을 추출하고 그 정합성을 수학적으로 증명했다는 점에서 이론적 기여가 큽니다.

한계 및 향후 과제:
현재 연구는 텐서 곱과 단위, 그리고 구조 규칙 (약화/축소) 만을 다룹니다. 향후 연구에서는 선형 함의 (Linear Implication) 를 포함하기 위해 내부 호모 (internal hom) 나 선형 - 비선형 쌍대 (linear-nonlinear adjunction) 같은 추가 범주 구조를 도입하고, 더 복잡한 신경 아키텍처 패밀리 (예: 트랜스포머) 에 대한 적용을 확장할 필요가 있습니다.

요약하자면, 이 논문은 신경 아키텍처의 설계 결정이 단순히 공학적 선택이 아니라, 내재된 논리적 구조를 가진다는 것을 보여주며, 이를 통해 아키텍처와 논리의 통합적 이해를 위한 기초를 마련했습니다.