LLM이 증명을 대신 써준다면, 의존 타입 언어는 실용화될까

소프트웨어의 복잡한 불변식(invariant)은 대개 주석으로 남는다. 그리고 팀이 커질수록 그 주석은 잊히고, 서로 맞물려야 할 컴포넌트들이 미묘하게 어긋난다. 문제가 발견될 즈음이면 양쪽 모두 손대기 벅찰 만큼 커져 있기 마련이다. Coq(최근 Rocq으로 개명), Lean 같은 의존 타입(dependently-typed) 언어는 이런 불변식을 타입으로 형식화하고 기계가 검증하게 만들자는 오래된 유혹을 던져왔다. 임의로 정교한 조건을 타입 시스템 안에 인코딩할 수 있다는 것이다.

증명의 비용이라는 벽

문제는 강력한 타입 시스템에는 그만큼의 증명 노동이 따라온다는 점이다. 아주 단순한 명제 하나를 증명하는 데 하루를 통째로 쓰는 일이 흔하고, 몇 시간을 매달린 끝에 증명하려던 목표 자체가 거짓이었음을 깨닫는 허탈한 경험도 반복된다. 원문 필자가 인용한 seL4 프로젝트의 회고가 이 부담을 상징적으로 보여준다. 충분한 경험을 쌓은 엔지니어들조차 설계·구현 대비 약 10배의 시간을 증명에 썼고, 결과적으로 C 코드보다 20배 넘는 분량의 증명 코드를 남겼다.

이 오버헤드 때문에 의존 타입 프로그래밍은 극히 좁은 영역에 머물렀고, 이를 자동화하려는 시도도 이어졌다. 대표적인 것이 F*로, SMT 솔버가 증명 의무를 자동으로 처리하게 하는 방식이다. 단순한 경우엔 잘 작동하지만, 솔버가 몇 시간씩 끝나지 않고 헤매게 만드는 입력을 짜기도 너무 쉽다. 결국 숙련자들은 솔버가 만족할 조건을 감으로 익혀 그 주위에 모든 것을 맞춰 짜게 되는데, 이는 문제를 일종의 신비주의로 바꿔버린다.

증명 무관성과 LLM

여기서 핵심 사실 하나가 등장한다. 명제가 옳다면, 이론적으로 그 증명의 '내용'은 중요하지 않고 오직 '존재'만 중요하다는 증명 무관성(proof irrelevance)이다. 물론 완전히 그렇지는 않다. 코드가 바뀔 때 증명을 다시 맞추는 수고를 줄이려면 증명을 잘 구조화해야 하고(seL4 팀이 말한 '증명 엔지니어링'), 지나치게 복잡한 증명은 타입 체커 자체를 폭주시켜 막대한 메모리를 잡아먹기도 한다.

필자의 관측은 이렇다. 증명 무관성과 결합된 LLM은 매우 유능한 증명 자동화 수단이 될 수 있다. 자동화가 충분하다면 증명 엔지니어링에 그리 신경 쓰지 않아도 되고, 타입 체커 폭주는 여전히 피해야 하지만 제한된 테스트에서 LLM이 이를 회피할 수 있었다는 것이다. 즉 LLM이 의존 타입 시스템을 갑자기 훨씬 실용적으로 만들 잠재력이 있다는 얘기다. 다만 이는 '제한된 테스트'에 근거한 관찰이며, seL4가 보여준 대규모 시스템의 증명 유지 비용이 정말 사라지는지는 아직 실증된 바가 아니라는 점은 분명히 해둘 필요가 있다.

Zstandard, 그리고 FSE라는 흥미로운 조각

필자는 이 아이디어를 시험하려고 Lean으로 Zstandard 압축 해제기를 만들었다. Yann Collet이 Jarek Duda의 ANS 연구를 토대로 만든 Zstandard는 gzip을 대체하며 사실상 표준 자리를 차지해가고 있다. LZ77 계열이지만 더 나은 엔트로피 코딩과 세심한 설계로 인상적인 해제 속도를 낸다. RFC가 존재하나 상당히 압축적이어서, 필자도 4.1절을 대여섯 번 읽고서야 감을 잡았다고 한다.

가장 흥미로운 부분은 엔트로피 인코더다. 고전적인 허프만 코딩은 심볼당 정수 개수의 비트만 쓸 수 있다는 한계가 있다. 이상적으로 2.3비트가 필요한 심볼도 2비트나 3비트로 반올림해야 한다. Zstandard는 허프만도 쓰지만 FSE라는 더 높은 압축률의 인코더를 갖는다. FSE는 심볼보다 상태(state)가 더 많은 상태 기계로, 각 심볼은 출현 확률에 비례하는 만큼의 상태를 배정받는다. 각 상태는 (해당 심볼, 비트스트림에서 읽을 비트 수, 다음 상태를 계산할 기준값)을 갖는다. 상태 하나당 정수 비트를 읽지만, 어떤 심볼에 1.5비트를 배정하려면 그 심볼의 상태 절반은 1비트를, 절반은 2비트를 읽게 해 평균으로 목표에 맞춘다.

예를 들어 상태 16개로 4개 심볼을 다룬다면 확률을 16분의 몇으로 근사한다(zstd는 실제로 32개 미만의 상태는 쓰지 않는다). 확률 5/16인 심볼 B의 이상적 비트 수는 약 1.68비트인데, 2비트를 읽는 상태 셋과 1비트를 읽는 상태 둘의 사용 빈도를 가중 평균하면 근사 확률에 거의 정확히 맞는다. 핵심 트릭은 인코더가 심볼만 고르는 게 아니라 그 심볼의 '어느 상태'에 착지할지도 고른다는 점이다. 그 선택이 다음 심볼로 정보를 실어 나르고, 소수점 아래의 비트가 바로 그곳에 담긴다. 상태 표는 전송되지 않고 RFC의 알고리즘으로 확률에서 재구성되므로, 확률만 보내면 된다.

다만 FSE는 앞에서부터 인코딩할 수 없다. 어떤 심볼의 시작 상태는 그 뒤에 오는 심볼에 의해 결정되기 때문에, 시퀀스의 끝에서부터 거꾸로 인코딩해야 한다. 압축기는 심볼을 뒤에서 앞으로 인코딩하되 출력은 순차적으로 쓰므로, 해제기는 블록의 끝으로 이동해 비트를 거꾸로 읽어야 한다. 한편 FSE 자체는 심볼 간 상관(예: 영어에서 Q 뒤에 U가 잦다는 사실)을 활용하지 못하므로, 그 중복성은 전통적인 LZ77 구조가 처리한다. FSE는 주로 그 역참조의 오프셋과 길이를 효율적으로 부호화하는 데 쓰인다.

도구로서의 Lean

Lean은 의존 타입 언어답게, 예컨대 스트림에서 n바이트를 읽어 예외를 던지지 않으면 '길이가 n인' 바이트 배열을 돌려준다는 사실을 타입에 담을 수 있다. 첫 수가 소수이고 두 수의 합이 6으로 나누어지며 배열 길이가 둘 중 작은 수 이상이라는, 아무도 필요로 하지 않을 조건까지 타입으로 쓸 수 있을 만큼 표현력이 크다. 그래서 현재 Lean의 주된 용도는 수학을 형식적으로 기술하고 증명하는 것이다. Lean은 Haskell처럼 순수 함수형이지만 엄격(strict) 평가를 택한다는 점이 다르다. 인자를 호출 전에 미리 계산하는 방식으로, 필요할 때만 계산하는 Haskell의 지연 평가와 대비된다.

한국의 실무자 입장에서 이 이야기의 함의는 명확하다. 형식 검증이 안정성에 결정적인 커널·암호·압축 코덱 같은 영역에서, 증명 노동이 LLM으로 상당 부분 상쇄된다면 '주석으로 남기고 잊히던 불변식'을 실제로 강제하는 선택지가 열린다. 반대로 솔버든 LLM이든 자동화가 만들어내는 불투명함, 그리고 타입 체커의 자원 폭주 같은 실무적 제약은 그대로 남는다. 지금 단계에서 확실한 것은 방향성과 한 개인의 소규모 실험 결과이지, 대규모 프로덕션에서의 검증은 아니다.