nano-lean은 Mathlib 검증을 11.85초로 줄였다

스티븐 딜(Stephen Diehl)은 새 Lean 커널 검사기 nano-lean이 Apple Silicon M5 Max에서 Mathlib의 선언 718,577개를 오류와 시간 초과 없이 11.85초 만에 다시 검사했다고 밝혔다. 그는 AI가 수학 증명을 빠르게 만들어내는 시대에 검증 속도와 신뢰성을 함께 높여야 한다고 주장한다.

딜은 지난 한 달 사이 페르마의 마지막 정리를 Lean으로 형식화한 결과, 나비에-스토크스 방정식 관련 결과, 새 수학 결과 372건 등이 나왔다고 소개한다. 그는 이런 결과가 늘어날수록 사람이 증명을 읽지 못하더라도 기계가 검증할 수 있어야 하며, 그 역할을 Lean 같은 의존 타입(dependent type) 기반 도구가 맡는다고 본다. 다만 검증기가 느려 검색 과정의 병목이 되면 신뢰 확인이 생략될 위험도 있다고 지적한다.

nano-lean의 검사 속도

딜이 공개한 nano-lean은 Rust로 작성한 Lean 커널 언어 검사기다. Lean 환경을 내보낸 파일을 읽어 귀납 타입, 양성성, 재귀자, 몫, 우주 수준 등 선언을 처음부터 독립적으로 검사한다. 함께 소개한 unbound는 바인더의 드 브루인 인덱스를 처리하는 라이브러리다.

속도 개선의 한 축은 텍스트 파싱을 없앤 것이다. Lean의 표준 내보내기 도구 lean4export는 줄마다 JSON 객체를 기록하지만, 대용량 JSON을 파싱하는 작업이 검사 시간의 상당 부분을 차지할 수 있다고 딜은 설명한다. 동반 도구 olean-export는 컴파일된 .olean 파일을 직접 읽고, 메모리 매핑에 맞춘 바이너리 형식인 blean을 생성할 수 있다. 이 형식은 postcard 인코딩을 사용하며, 검사기는 파일을 메모리에 매핑해 별도의 파싱 없이 읽는다.

딜이 제시한 수치는 M5 Max의 14개 스레드에서 각 라이브러리와 증명의 전체 가져오기 환경을 검사한 결과다.

Mathlib의 커널 검사 시간을 선언 수로 나누면 선언당 평균 10.5마이크로초라고 딜은 계산한다. 그는 대규모 탐색 과정에서 후보 증명을 반복 검사하는 경우 이 수치가 중요하다고 설명한다. 다만 nano-lean은 가능성을 보이기 위한 개념 증명이며, 딜은 자신이 일하는 OneChronos에서 더 큰 Lean 증명 검사에 사용한다고 밝혔다. 그는 수년간 검토된 공식 Lean 커널보다 신뢰성이 낮다고 덧붙였다. 공식 커널은 같은 라이브러리를 검사하는 데 약 15분이 걸린다고 한다.

검증기와 형식화의 신뢰

딜은 Lean의 작은 신뢰 기반인 커널도 오류가 없다고 보장할 수 없으며, 과거에도 건전성 버그가 있었다고 지적한다. AI 에이전트가 컴파일을 목표로 반복 탐색하면 커널의 취약점을 우연히 찾을 수도 있다는 우려다. 이에 대한 방안으로 그는 여러 사람이 서로 다른 언어와 표현 방식으로 만든 독립 커널을 함께 돌리고 결과가 일치하는지 확인하는 차등 검증을 제안한다. Csmith 연구는 여러 컴파일러에 무작위 C 프로그램을 적용해 수백 건의 버그를 발견한 사례로 언급된다. Lean 검사기 프로젝트로는 마리오 카르네이로(Mario Carneiro)의 lean4lean, 크리스 베일리(Chris Bailey)의 nanoda가 소개된다. nano-lean의 nl-mutate는 유효한 내보내기 파일을 변형해 검사기 간 불일치를 찾는다.

검사기가 증명 자체를 올바르게 확인해도, 정리가 애초에 의도한 명제를 나타내는지는 별도로 확인해야 한다. 딜은 공리 추가, sorry 삽입, 표기법 변경 등으로 증명의 대상이 약화될 수 있다고 경고한다. OpenAI 저장소가 사용하는 Comparator는 제출된 증명을 별도로 지정한 문제 명제와 대조한다. 결국 누군가는 추측을 형식화하고 그 형식화가 원래의 수학적 의미를 보존하는지 살펴야 한다는 것이 딜의 주장이다.

딜은 Tau Ceti를 사람과 AI가 역할을 나누는 사례로 든다. 사람은 로드맵과 검토 기준을 작성하고, AI는 코드를 만들고 변경 요청을 제출하며 AI 기반 검토를 거친다. 그는 Lean에 표준 포매터, 안정적으로 명세된 내보내기 형식, 독립 커널 검사, 반복 호출에 적합한 라이브러리 인터페이스, 대규모 환경을 위한 메모리 관리, 기계 작성 코드에 맞춘 린터와 검색 도구, 증명의 출처 기록이 필요하다고 제안한다.

딜은 수학 증명에서 시작된 이 방식이 정밀한 명세를 세울 수 있는 산업용 소프트웨어로 이어질 수 있다고 본다. 다만 AI가 만든 증명이 빠르게 늘어나는 만큼, 검증기와 명제 형식화의 신뢰성을 함께 확보해야 한다는 것이 글의 핵심이다.