증명 도우미의 '최종 심판'이 더 단단해졌어요
Lean이라는 언어 들어보셨나요? 수학 정리를 컴퓨터로 증명하거나, 프로그램이 정말 의도대로 동작하는지 수학적으로 확인할 때 쓰는 '증명 도우미(proof assistant)'이자 프로그래밍 언어예요. Lean을 만든 레오나르도 드 무라(Leonardo de Moura)가 최근 블로그에 Lean이 이제 검증된 커널(verified kernel)을 함께 배포한다는 소식을 올렸어요.
이게 왜 지금 중요하냐면요, 요즘 Lean은 AI 수학의 표준 채점기가 됐거든요. 구글 딥마인드의 AlphaProof나 DeepSeek-Prover 같은 AI가 증명을 만들어내면, 그 증명이 진짜 맞는지는 Lean이 판정해요. 'AI는 그럴듯한 거짓말을 할 수 있지만 Lean은 속지 않는다'가 전제인 거죠. 그런데 이 전제가 성립하려면 Lean의 판정 부분 자체에 버그가 없어야 해요. 이번 발표는 바로 그 지점을 겨냥한 거예요.
커널이 뭐냐면: 시험 채점관이에요
Lean으로 증명을 쓸 때 우리는 simp, omega 같은 전술(tactic)을 써요. 전술은 '이런 식으로 증명해줘'라고 부탁하면 알아서 증명을 만들어주는 자동화 도구인데요, 코드량이 엄청 많고 복잡해요. 당연히 버그도 있을 수 있죠.
그래서 Lean은 구조를 둘로 나눠요. 전술과 엘라보레이터(사람이 쓴 코드를 내부 표현으로 바꾸는 번역기)가 최종적으로 '증명 항(proof term)'이라는 결과물을 만들면, 커널이라는 아주 작은 프로그램이 이걸 처음부터 끝까지 다시 검사해요. 학생이 계산기를 쓰든 참고서를 보든 상관없이, 마지막에 채점관이 답안을 한 줄씩 확인하는 구조라고 보면 돼요.
이 설계 철학을 드 브라윈 기준(de Bruijn criterion)이라고 불러요. '반드시 믿어야 하는 코드는 최대한 작게 유지하라'는 원칙이에요. 전술에 버그가 있어도 커널이 걸러주니까, 우리는 커널만 믿으면 되는 거죠.
문제는 Lean 4의 기본 커널이 C++로 작성돼 있고, 그 커널이 올바르다는 건 '열심히 테스트하고 리뷰했다' 수준의 신뢰였다는 거예요. 채점관이 실수하면 틀린 답안이 만점을 받을 수 있는 거죠. 실제로 여러 증명 도우미의 역사에서 커널이나 체커 버그 때문에 거짓 명제가 통과되는 사례가 종종 보고돼 왔어요.
'검증된 커널'은 어떻게 만드나요?
이 문제를 푸는 방법은 크게 두 갈래예요.
첫 번째는 독립 구현을 여러 개 두는 것이에요. 채점관을 한 명이 아니라 서로 다른 배경을 가진 여러 명으로 두는 거죠. Lean 커뮤니티에는 이미 Rust로 작성된 nanoda, Lean 자체로 작성된 lean4lean 같은 독립 타입 체커가 있었어요. 같은 증명을 서로 다른 언어, 다른 사람이 만든 커널로 검사하면 한쪽에만 있는 버그는 다른 쪽에서 걸리게 돼요.
두 번째는 커널 자체를 수학적으로 증명하는 것이에요. 커널을 Lean으로 작성하고, '이 커널이 통과시키는 증명은 Lean의 타입 이론 규칙에 맞는다'는 성질을 Lean 안에서 증명하는 거죠. 마리오 카네이로(Mario Carneiro)의 lean4lean 프로젝트가 이 방향의 연구를 이어왔어요.
제목에서 커널이 복수형(kernels)인 것도 이런 맥락으로 읽을 수 있어요. 기본 커널 하나에만 기대지 않고, 신뢰 수준이 높은 커널을 공식 배포판에 함께 넣어 교차 검사를 누구나 쉽게 할 수 있게 만든 거죠. 다만 각 커널이 어디까지 증명됐는지, 성능 차이는 어느 정도인지는 원문에서 꼭 확인해 보세요. '검증됐다'는 말은 무엇을 기준으로 어디까지 증명했느냐에 따라 의미가 꽤 달라지거든요.
다른 증명 도우미들은 어떨까요?
이 방향이 Lean만의 이야기는 아니에요. Coq(최근 Rocq로 이름을 바꿨어요) 진영에는 MetaCoq라는 프로젝트가 있어서, Coq의 타입 체커를 Coq 안에서 검증하는 작업을 오래 해왔어요. HOL Light 계열에서는 검증된 컴파일러 언어인 CakeML로 커널을 다시 구현한 Candle 같은 시도도 있었고요.
Lean의 합류가 특히 의미 있는 건 사용 규모 때문이에요. 수학 라이브러리 Mathlib은 수십만 개의 정리를 담고 있고, AI 증명 연구의 대부분이 Lean을 타깃으로 해요. 가장 많이 쓰이는 채점기의 신뢰도를 올리는 건 생태계 전체의 바닥을 다지는 일이에요.
한국 개발자에게는 어떤 의미일까요?
솔직히 일반적인 웹이나 앱 개발에 당장 영향을 주는 소식은 아니에요. 그래도 흘려듣기엔 아까운 이유가 있어요.
- AI 생성과 기계 검증의 분리: 'AI가 만들고, 기계가 검사한다'는 패턴이 수학을 넘어 소프트웨어로 퍼지고 있어요. AWS는 권한 정책 언어 Cedar의 명세와 핵심 성질을 Lean으로 증명하고 있거든요. 금융, 스마트 컨트랙트, 암호 라이브러리처럼 버그 하나가 큰 사고로 이어지는 분야라면 형식 검증은 점점 현실적인 선택지가 될 거예요.
- 신뢰 경계(trusted base)라는 사고방식: '우리 시스템에서 반드시 믿어야 하는 부분은 어디고, 그걸 얼마나 작게 만들 수 있나?'라는 질문은 보안 설계나 권한 시스템 설계에도 그대로 통해요.
- 입문 장벽이 낮아요: 브라우저에서 바로 해볼 수 있는 Natural Number Game이나 무료 책 'Functional Programming in Lean' 같은 자료가 잘 갖춰져 있어서 주말에 가볍게 시작해볼 만해요.
마무리
한 줄로 정리하면, Lean이 '증명을 검사하는 프로그램도 검사받아야 한다'는 마지막 퍼즐을 공식 배포판 차원에서 맞추기 시작했다는 소식이에요.
여러분은 AI가 짠 코드를 어디까지 믿고 계신가요? 테스트 코드로 충분하다고 보시나요, 아니면 언젠가는 형식 검증 같은 더 강한 보장이 필요해질 거라고 보시나요? 의견 나눠주세요!
🔗 출처: Hacker News