신경망에도 타입 시스템이 필요하다: 수학자가 본 딥러닝의 새로운 언어

신경망 코드는 왜 이렇게 버그가 잘 날까

파이토치나 텐서플로우로 모델을 짜본 분들은 공감하실 거예요. 텐서 차원 하나 잘못 맞추면 에러가 펑펑 나고, 배치 차원을 깜빡하면 학습은 되는데 결과가 이상하게 나오고요. 더 웃긴 건 코드는 멀쩡히 돌아가는데 수학적으로 말이 안 되는 연산을 하고 있는 경우도 많다는 거예요. 왜 이럴까요? 수학자 Bruno Gavranović가 최근에 쓴 "Types and Neural Networks"라는 글은 이 문제를 "우리가 신경망을 설명하는 언어 자체가 부족하다"는 관점에서 파고들어요. 좀 철학적으로 들릴 수 있는데, 실용적인 함의가 꽤 커요.

타입 시스템이 뭐길래

먼저 타입 시스템(type system) 이 뭔지 짚고 갈게요. 프로그래밍 언어에서 타입은 "이 변수에는 정수만 들어갈 수 있어", "이 함수는 문자열을 받아서 불리언을 돌려줘" 같은 제약이에요. 하스켈이나 러스트, 타입스크립트를 써본 분이라면 타입이 버그를 얼마나 막아주는지 아실 거예요. 컴파일 단계에서 말이 안 되는 연산을 미리 잡아주니까요.

근데 신경망에서 타입이라고 하면 보통 "float32냐 int64냐" 정도만 떠올려요. Gavranović가 말하는 건 그런 저수준 타입이 아니라, 텐서의 구조와 의미를 수학적으로 표현하는 타입 이에요. 예를 들어 어떤 텐서가 "배치 × 시퀀스 길이 × 임베딩 차원"을 나타낸다는 걸 타입에 박아두면, 배치 차원을 실수로 시퀀스 차원으로 바꿔 먹는 실수가 원천 차단돼요.

카테고리 이론과 신경망의 만남

글의 핵심은 카테고리 이론(category theory) 으로 신경망을 바라보는 관점이에요. 카테고리 이론은 쉽게 말해 "뭔가들 사이의 관계"를 추상적으로 다루는 수학 분야인데요, 함수형 프로그래밍 쪽에서는 모나드 같은 개념으로 익숙하죠. 최근 몇 년간 "Categorical Deep Learning"이라는 흐름이 생기면서, 신경망의 레이어들을 카테고리의 화살표(morphism)로 보고 합성 규칙을 따지는 연구가 활발해졌어요.

이 관점이 왜 유용하냐면, 신경망은 결국 함수의 합성 이거든요. 입력 → 레이어1 → 레이어2 → ... → 출력 이런 식이잖아요. 각 레이어가 어떤 타입의 텐서를 받아서 어떤 타입의 텐서를 내보내는지 정의해두면, 합성이 가능한지 아닌지 자동으로 판단할 수 있어요. 하스켈에서 f . g가 타입이 맞을 때만 되는 것처럼요. 여기에 파라미터화된 함수(parametrized function), 즉 학습 가능한 가중치를 가진 함수라는 개념을 더하면 역전파(backpropagation) 같은 학습 과정까지 수학적으로 깔끔하게 표현돼요.

의존 타입과 텐서 쉐이프

더 나아가 의존 타입(dependent type) 얘기가 나와요. 의존 타입은 "값에 의존하는 타입"이에요. 예를 들어 "길이가 n인 리스트"라는 타입이 있다면, 두 개를 이어붙인 결과의 타입은 "길이가 n+m인 리스트"가 되는 식이죠. 이걸 텐서에 적용하면 "shape이 (B, 768)인 텐서와 shape이 (768, 10)인 행렬을 곱하면 shape이 (B, 10)인 텐서가 나온다"를 컴파일러가 검증할 수 있어요. 차원이 안 맞으면 아예 컴파일이 안 되니까 런타임 에러가 사라지는 거죠.

이미 실험적인 라이브러리들이 있어요. JAX 생태계의 jaxtyping, 파이토치의 torchtyping, 구글의 Dex 언어, 그리고 Hasktorch 같은 하스켈 바인딩까지. einops의 rearrange처럼 차원 이름을 문자열로 적는 방식도 이 흐름의 한 갈래예요. 전부 "텐서 차원 에러를 런타임이 아니라 타입 단계에서 잡자"는 같은 목표를 향하고 있어요.

업계 맥락에서 보면

이 움직임은 딥러닝이 점점 "연구자의 장난감"에서 "엔지니어링 시스템"으로 넘어가고 있다는 신호예요. LLM 시대가 되면서 모델 파이프라인이 엄청나게 복잡해졌고, 한 번 학습에 며칠씩 걸리니까 사전에 오류를 잡는 비용 이 훨씬 중요해졌거든요. 학습 3시간째 차원 에러가 나서 처음부터 다시 돌리는 경험을 해보면 타입 시스템의 가치가 확 와닿아요.

DeepMind 쪽에서 카테고리 이론을 본격적으로 밀고 있고, 옥스퍼드의 Bob Coecke 같은 사람들은 아예 Categorical Quantum Mechanics 에서 출발한 다이어그램 기반 접근법으로 신경망을 새로 그리려 해요. 한편으로는 PyTorch 2.x의 torch.compile이나 JAX의 XLA처럼 컴파일러가 텐서 프로그램을 정적으로 분석해서 최적화하는 흐름도 강해지고 있고요. 이 두 흐름이 결국 만날 거라는 게 많은 연구자들의 예상이에요.

한국 개발자에게

당장 "우리 팀에 카테고리 이론 도입하자"는 실용성은 없어 보일 수 있어요. 솔직히 대부분의 실무에서는 jaxtyping이나 torchtyping처럼 shape 어노테이션 라이브러리 를 쓰는 정도가 현실적이죠. 근데 이 정도만 해도 효과가 커요. 함수 시그니처에 Float[Tensor, "batch seq dim"] 같은 타입을 적어두면 코드 리뷰 속도도 빨라지고, 협업하는 팀원이 모델 구조를 이해하기가 훨씬 쉬워져요.

더 장기적으로는 MLOps 쪽에서 이 접근이 표준이 될 가능성이 높아요. 모델 서빙할 때 입력 텐서 shape 검증, 학습 파이프라인의 데이터 증강 단계 검증 같은 데서 자연스럽게 들어오거든요. ML 플랫폼이나 프레임워크 개발에 관심 있는 분이라면 지금부터 카테고리 이론 기초를 조금씩 익혀두면 3~5년 뒤에 큰 자산이 될 거예요.