우리의 Lean 4 + mathlib 프로젝트는 모든 PR(Pull Request)마다 CI(Continuous Integration)에서 41분을 소요하곤 했습니다. 오늘날 최악의 경우인 가장 무거운 파일들을 처음부터 다시 빌드하는 데 12분이 걸리며, 일반적인 PR은 증분 빌드(incremental build)를 통해 몇 분 안에 완료됩니다.

이 글은 세 번의 라운드에 걸친 개선 과정을 기록하며, 각 과정은 동일한 형태인 문제(problem) → 가설(hypothesis) → 검증(verification) → 해결(fix) 구조로 작성되었습니다. 미리 스포일러를 하자면, 세 번 모두 우리의 직관이 가리켰던 첫 번째 가설 — 즉 범인이라고 생각했던 것 — 은 무죄로 밝혀졌습니다. 이 이야기의 주인공은 어떤 개별적인 기술이 아닙니다. 우리의 가설을 차분하게 거부해 온 프로파일링(profiling)입니다.

Lean 관련 개념들은 등장할 때마다 설명되므로, Lean을 모르더라도 따라오실 수 있습니다.

한 가지 더 말씀드리자면, 이 세 라운드에서의 거의 모든 측정과 구현은 AI 에이전트(AI agents)에 의해 수행되었습니다 (라운드 1과 2는 사람이 참여하는 인터랙티브 세션으로 진행되었고, 라운드 3은 요구사항 문서에 의해 구동되는 자율 루프(autonomous loop)로 진행되었습니다). 사람인 저는 두 가지 일을 했습니다: 수치적 목표를 승인하고 결과를 수락하는 것입니다. 기사의 후반부에서는 그 작업, 특히 AI가 저렴한 해결책으로 수렴하지 않도록 유지하는 메커니즘에 대해 다룹니다.

배경: 프로젝트

대상은 AlgebraicArchitectureTheoryV2로, 제 이전 글들에서 다루었던 것과 동일한 모노레포(monorepo)입니다. 이는 Lean 4를 이용한 소프트웨어 아키텍처 이론의 형식 검증(formal verification) 프로젝트입니다.

이 글에 필요한 Lean 메커니즘의 전체 목록은 다음과 같습니다 — 총 다섯 가지 항목입니다:

규모를 말씀드리자면, 이번 감사는 4,000개 이상의 선언(declarations)을 대상으로 하며, 그중에는 대수 기하학(algebraic geometry)의 스킴(schemes) 구축을 다루는 매우 무거운 파일 하나가 포함되어 있는데, 이 파일 하나를 빌드하는 데만 38분이 소요되었습니다.

CI는 GitHub Actions에서 실행됩니다. lake build와 함께, 모든 PR은 **커널 공리 감사 (kernel axiom audit)**를 수행합니다. 이는 모든 정리가 속임수 없이 실제로 증명되었는지 기계적으로 확인하는 과정입니다. 이 관문은 타협할 수 없는 필수 사항이며, Round 1에서 이것이 실제로 무엇을 하는지 설명합니다.

Round 1: 공리 감사 (axiom audit), 7분 11초 → 11초

문제 상황

Lean에서 모든 정리는 공리(axioms)로부터 유도되며, 이 유도 과정은 커널(kernel, 작고 신뢰할 수 있는 검증기)에 의해 기계적으로 검증됩니다. "증명이 통과되었다"는 것은 이 검증을 통과했음을 의미합니다. 중요한 변수는 Lean에 sorry라고 불리는 탈출구(escape hatch)가 있다는 점입니다. sorry를 작성하는 것은 "이 부분은 나중에 증명하겠다"는 의미이며, 즉시 오류를 발생시키지는 않습니다 (에디터에 경고는 표시됩니다). 내부적으로는 sorryAx라고 불리는 공리를 조용히 가정합니다. 사용자들은 또한 axiom 키워드를 사용하여 증명되지 않은 임의의 명제를 공리로 추가할 수도 있습니다.

다시 말해, "CI가 통과(green)되었다"는 사실만으로는 "모든 것이 증명되었다"와 "누군가 공리로 빈틈을 메워두었다"를 구분할 수 없습니다. 따라서 각 선언에 대해 의존성(dependencies)을 끝까지 추적하여 **도달하는 공리 집합 (the set of axioms it reaches)**을 계산한 다음, 이 집합이 Lean과 mathlib 전반에서 수용되는 세 가지 표준 공리인 propext, Quot.sound, 그리고 Classical.choice (선택 공리) 범위 내에 있는지 확인합니다. 이것이 바로 공리 감사입니다. 숨겨진 sorry나 몰래 들여온 공리는 이 감사를 통과할 수 없습니다. 스스로를 형식 검증 (formal verification) 프로젝트라고 부른다면, 이 관문을 건너뛸 수는 없습니다.

Lean은 이러한 순회 및 수집 (walk-and-collect) 작업을 collectAxioms라고 불리는 함수로 노출합니다 (이는 #print axioms my_theorem을 입력할 때 실행되는 것과 동일한 메커니즘입니다). 우리의 CI는 모든 선언 (declaration)에 대해 이 함수를 실행했습니다. 당시에는 1,207개였고, 현재는 4,300개가 넘습니다. 그리고 이 단계는 매 실행마다 7분 11초가 소요되었습니다. 감사 (audit) 과정이 빌드 자체보다 더 무거웠던 것입니다.

가설 (Hypothesis)

감사의 진입점은 감사된 모든 선언을 나열한 5,000줄 이상의 거대한 파일입니다. 직관은 이렇게 말합니다. "이렇게 큰 파일은 정교화 (elaborate)하는 데 비용이 많이 들 것이다. 파일을 나누면 더 빨라질 것이다."

검증 (Verification)

무엇인가를 나누기 전에, 우리는 시간이 어디에 쓰이는지 측정했습니다. 결과는 직관과 정면으로 배치되었습니다:

• 임포트 (import) 해결: ~10초
• 5,000줄 분량의 목록 정교화 (elaborating): 차이 없음 (줄 수를 크게 변경해도 감사 시간은 변하지 않았습니다)
• collectAxioms × 1,207개 선언: ~5분

범인은 큰 파일이 아니었습니다. 문제는 감사가 호출되는 방식이었습니다. 하나의 선언이 도달하는 공리 (axioms)를 찾으려면, 의존성 그래프 (dependency graph)를 루트까지 순회해야 합니다. 즉, 해당 선언이 사용하는 정리 (theorems), 그리고 그 정리가 사용하는 또 다른 정리들을 따라가는 식입니다. collectAxioms는 모든 선언에 대해 이 순회를 처음부터 다시 수행합니다. 하지만 프로젝트의 모든 선언은 동일하고 거대한 기반인 mathlib을 공유합니다. 따라서 1,207개의 선언이 본질적으로 동일한 그래프를 1,207번 순회하고 있었던 것입니다. 복잡도 측면에서 보면 O(선언 수 × 그래프)입니다. 파일을 나누는 것은 이 곱셈의 어떤 요소도 건드리지 않습니다. 이론적으로도 효과가 없었지만, 측정값을 손에 쥐고 있었기에 우리는 이를 단 한 줄로 기각하고 다음 단계로 넘어갈 수 있었습니다.

해결책 (Fix)

우리는 감사를 2단계로 만들었습니다:

1. 성공 경로 (Success path): 모든 선언(declaration)에 걸쳐 "같은 노드를 두 번 걷지 않는다"는 원칙인 방문 집합(visited set)을 공유하여 그래프를 정확히 한 번만 순회합니다. 질문의 핵심은 "도달한 공리(axiom)들의 합집합이 표준적인 3개 이내로 유지되는가?"이므로, 공유된 단 한 번의 순회는 각 선언별로 순회했을 때와 동일한 판정을 내립니다.
2. 실패 경로 (Failure path): 비표준 공리가 나타날 때만, 정확히 원래 형식과 동일한 에러 메시지를 출력하며 어느 선언이 잘못되었는지 식별하기 위해 기존의 선언별 순회 방식으로 돌아갑니다.

이 방식은 에러 품질을 전혀 포기하지 않으면서도, 성공 경로에서 시간 복잡도를 O(선언 수 × 그래프)에서 O(그래프)로 압축합니다. 이는 그래프 순회(graph traversal)에서 사용하는 교과서적인 방문 집합(visited-set) 기법이며, Lean 특유의 마법 같은 기술은 전혀 들어가지 않았습니다. CI에서 측정한 결과, 감사(audit) 시간은 7분 11초에서 11초로 단축되었으며, 당시 전체 lake build 작업 시간은 약 9.5분에서 2분 12초로 줄어들었습니다.

라운드 1의 교훈: "무거운 파일"을 의심하기 전에 "무거운 연산 × 반복 횟수"를 먼저 의심하십시오. 그리고 기각된 가설(파일 분할: 효과 없음)을 그 자체로 하나의 결과로서 기록해 두십시오. 그래야 나중에 다른 사람이 똑같은 직관으로 똑같은 구덩이를 파는 일을 방지할 수 있습니다.

라운드 2: 모든 PR이 41분 소요됨 — 빌드 _전_에 캐시가 저장됨

문제 (Problem)

라운드 1은 lake build 작업이 2분 남짓으로 줄어들었던 7월 중순에 발생했습니다. 이후 2주 동안 일련의 무거운 대수기하학(algebraic-geometry) 구현체들이 추가되었고(라운드 3의 주인공이 이 기간 동안 비대해졌습니다), 어느 시점부터는 단 하나의 파일만 수정하더라도 모든 PR이 전체 트리의 풀 콜드 빌드(full cold build)를 수행하게 되었습니다. 약 41분이 소요되었습니다.

Lean 빌드는 C++나 Rust와 같은 정신으로 증분 빌드(incremental build)를 지원합니다. 빌드 결과물(.olean 파일, .lake/build 하위의 모듈별 저장)이 남아 있다면, 변경된 파일과 그에 의존하는 하위 파일들만 다시 빌드하면 됩니다. CI에서 이것이 작동하려면 이전 실행의 결과물들이 캐시(cache)로서 전달되어야 합니다. 캐시는 설정되어 있었습니다. 다만 작동하지 않았을 뿐입니다.

가설 (Hypothesis)

캐시가 "작동하지 않을" 때, 흔히 의심되는 원인은 키 불일치(key mismatch) 또는 제거(eviction)입니다. 툴체인 해시(toolchain hash)가 잘못되었을까요? 이전 세대(old generations)가 제거되고 있는 것일까요?

검증 (Verification)

키를 감사(audit)하기 전에, CI 로그의 타임스탬프를 위에서 아래로 읽어보았습니다. 1초 간격으로 떨어진 두 줄이 있었습니다:

23:19:35  Cache save   (lean-action의 마지막 내부 단계)
23:19:36  lake build +Formal.AG 시작

캐시는 저장되고 있었습니다. 프로젝트가 빌드되기 전에 말입니다.

우리는 build: false로 설정된 lean-action — 복합 액션 (composite action, 재사용 가능한 단계들의 번들) — 을 사용하여 Lean을 설정하고, 이후 단계에서 직접 빌드를 수행하도록 했습니다. 하지만 lean-action은 자체적인 마지막 내부 단계에서 .lake (빌드 아티팩트 디렉토리)를 캐시에 저장하며, 복합 액션의 내부 단계는 항상 사용자의 후속 단계보다 먼저 실행됩니다. 따라서 저장되고 있던 2.15 GiB는 의존성 아티팩트(mathlib)만을 포함하고 있었습니다. 프로젝트 자체의 .olean 파일들은 전혀 캐싱되지 않았던 것입니다. 모든 PR이 41분씩 걸렸던 것도 당연했습니다. 각 PR마다 모든 자체 코드를 백지 상태에서 다시 빌드해야 했기 때문입니다.

보너스 같은 발견도 하나 있었습니다. mathlib은 개별 사용자가 빌드하기에는 너무 크기 때문에, 커뮤니티에서는 Azure로부터 사전 빌드된 아티팩트를 배포합니다 (lake exe cache get; 저희 측정 결과 환경에 따라 약 15초 소요). 따라서 캐싱된 2.15 GiB는 어차피 15초면 가져올 수 있는 것이었으며, GitHub 캐시 내에서는 무가치했습니다. 설상가상으로, 2.15 GiB × 4세대를 계산하면 저장소의 10 GiB 캐시 할당량(quota)을 거의 다 써버리는 수준이었습니다. 쓸모없는 캐시가 유용한 캐시를 밀어내고 있었던 것입니다.

해결 (Fix)

우리는 캐시의 책임을 분리했습니다:

• lean-action의 GitHub 캐시를 비활성화 (use-github-cache: false); mathlib 아티팩트(artifacts)는 Azure 캐시로부터 계속 가져옵니다.
• (빌드 전) 명시적으로 복구(restore)하고, (빌드 직후) 프로젝트 자체의 .lake/build만 저장(save)합니다.
• 키(key)의 접두사(prefix)로 lean-toolchain + lake-manifest.json의 해시(hash)를 사용하여, 툴체인(toolchain)이나 mathlib이 업데이트되면 적절한 콜드 빌드(cold build)로 전환되도록 합니다.
• always()를 사용하여 저장함으로써, 빌드가 실패하더라도 부분적인 아티팩트(artifacts)가 유지되도록 합니다. 즉, 실패한 PR에 푸시(push)할 때마다 실패 지점까지 빌드된 모든 것을 재사용하여 반복 작업(iteration) 속도를 높입니다.

실제 워크플로(workflow)는 다음과 같습니다 (발췌). 가장 중요한 한 가지는: 저장(save) 단계를 빌드(build) 이후에 직접 배치하는 것입니다.

- name: Restore Formal build cache
  uses: actions/cache/restore@v5
  with:
...

이렇게 하면, 무거운 기하학(geometry) 파일을 건드리지 않는 PR은 캐시 히트(cache hit)와 증분 빌드(incremental build)로 처리되어 몇 분 내에 완료됩니다.

lean-action에 대해 공정하게 말하자면, 액션(action)이 빌드까지 실행하도록 두는 표준적인 사용 방식에서는 캐시가 올바르게 작동합니다. 함정에 빠진 것은 빌드를 외부에서 수행하도록 설정한 build: false라는 우리의 구성이었습니다.

Round 2의 교훈: "캐시가 작동하지 않을" 때는 키(keys)를 감사(audit)하기 전에 타임스탬프(timestamps)를 먼저 확인하세요. 복합 액션(Composite actions)은 편리하지만, 그 내부의 단계(step) 순서는 사용자의 워크플로 단계 순서와는 별개(orthogonal)입니다. "저장이 실제로 빌드 이후에 이루어지는가?"를 직접 눈으로 확인해 볼 가치가 있습니다.

Round 3: 38분이 걸리는 Geometry.lean — 파일을 분할해도 빨라지지 않았다

문제 (Problem)

남아 있는 가장 큰 병목(bottleneck)은 단 하나의 파일이었습니다: 5,129행, 108개의 선언(declarations)을 가진 Geometry.lean입니다. 이 파일은 mathlib 위에 실제 스킴(schemes) — 현대 수학 기준으로도 무거운 추상화인 대수 기하학(algebraic geometry)의 핵심 객체들 — 을 구축하며, CI에서 이 파일 하나만으로 38.3분이 소요되어 프로젝트 전체 CPU 시간의 46%를 차지했습니다. Round 2의 캐시가 있더라도, 이 파일의 상위(upstream)를 건드리는 모든 PR은 38분 전체를 고스란히 지불해야 했습니다.

이번에는 시작하기 전에 수치적 목표를 설정했습니다: 가장 긴 모듈 ≤ 600초, 대상 모듈들의 총합 ≤ 1,800초. 이는 동일한 GitHub Actions 전체 빌드에서 보고된 모듈 시간을 기준으로 판단했습니다. 측정 방법도 포함되었으며, 구현을 시작하기 전 사람의 승인을 받았습니다.

가설 (Hypothesis)

이 파일은 38분이 걸리는 거대한 파일입니다. 의존성 구조(dependency structure)에 따라 모듈로 분할하면 재빌드(rebuild) 시간이 줄어들고 속도가 빨라질 것입니다. 이는 Round 1에서 이미 한 번 거부되었던 "분할하면 빨라진다"는 가설의 빌드 시간 버전입니다. 선언(declaration)마다 정교화(elaboration)가 실행되므로, 이번에는 논리가 타당해 보입니다.

검증 (Verification)

먼저, 선언별 프로파일링(per-declaration profile)을 수행했습니다. Lean에는 내장 프로파일러(profiler)가 포함되어 있어, 명령어 하나로 어떤 선언의 어떤 처리 단계가 몇 초 걸렸는지 알 수 있습니다. 저희가 사용한 명령어는 다음과 같습니다:

lake env lean --profile --json \
  -Dprofiler.threshold=10 \
  -Dtrace.profiler=true -Dtrace.profiler.threshold=10 \
...

분석 결과: 커널 타입 체크(kernel type checking) 57%, defeq (두 항이 정의적으로 동일한지 결정하는 과정) 39%였으며, 시간은 10여 개의 선언에 엄청나게 집중되어 있었습니다. 이 무게 중심과 의존성을 따라 파일을 7개 모듈의 DAG(Directed Acyclic Graph)로 분할했습니다:

RawGeometry
└─ SectionRings
   ├─ LeftRestriction
...

저희는 분할이 아무것도 망가뜨리지 않았음을 기계적으로 증명했습니다. Lean의 #check는 선언의 문장(statement), 즉 정리(theorem)의 실제 주장(claim)을 출력합니다. 동일한 툴체인(toolchain)과 동일한 출력 설정 하에서, 분할 전후의 기존 파일 내 모든 168개 공개 선언(794행)에 대한 #check 출력을 가져와 SHA-256 해시값이 일치함을 확인했습니다. 정리 문장의 단 한 글자도 바뀌지 않았습니다. 기계적인 리팩터링(refactor)일지라도 눈이 아닌 해시를 통해 "수학적 내용이 보존되었다"는 것을 인증할 수 있다는 점은 형식 검증(formal verification) 프로젝트의 은밀한 즐거움 중 하나입니다.