본 기사는 Hashnode에 공개한 Taming a 40-Minute Lean CI: Three Rounds, Three Wrong Suspects의 일본어판입니다.

Lean 4 + mathlib 프로젝트에서 PR을 제출할 때마다 CI가 41분 걸리고 있었습니다. 지금은 가장 무거운 파일군을 전부 재빌드하는 최악의 경우에도 12분, 일반적인 PR이라면 차분 빌드(incremental build)로 몇 분 만에 끝납니다.

이 기사는 그 개선 과정을 3라운드로 나누어 기록한 것입니다. 각 라운드를 과제 → 가설 → 검증 → 해결 순서로 작성합니다. 미리 결론을 말씀드리자면, 3번 모두 첫 번째 가설 — 직관이 지목한 범인 — 은 무죄였습니다. 개선의 주역은 개별 테크닉이 아니라, 가설을 담담하게 기각해 나간 계측(measurement)입니다.

Lean 고유의 개념은 등장할 때마다 설명하므로, Lean을 모르더라도 읽을 수 있을 것입니다.

그리고 한 가지 더. 이 3라운드의 계측과 구현은 거의 모두 AI 에이전트가 수행했습니다 (Round 1·2는 인간이 옆에 있는 대화 세션, Round 3는 요구 문서를 전달한 자율 루프입니다). 인간(나)이 한 것은 수치 목표의 승인과 수용 판정뿐입니다. 후반부에서는 그 운용 — 특히 AI가 안이한 해답으로 도망치지 않게 만드는 메커니즘 — 에 대해서도 쓰겠습니다.

대상은 지금까지의 기사에서도 다루어 온 AlgebraicArchitectureTheoryV2 — 소프트웨어 아키텍처 이론을 Lean 4로 형식 검증(formal verification)하고 있는 모노레포(monorepo)입니다.

이 기사에 등장하는 Lean의 도구는 다음 5가지가 전부입니다.

규모를 먼저 공유하자면, 감사 대상 선언은 4,000건 이상입니다. 그중에는 대수기하학의 스킴 구성(scheme construction)을 포함한 중량급 파일이 있으며, 이것 단독 빌드에 38분이 걸리고 있었습니다.

CI는 GitHub Actions를 사용하며, lake build에 더해 Kernel axiom audit (공리 감사) — 모든 정리가 정말로 증명되었는지, 증명에 편법이 없는지를 기계 검사하는 과정 — 을 매 PR마다 실행합니다. 이 게이트 자체는 제거할 수 없습니다. 내용은 Round 1에서 설명하겠습니다.

Lean에서는 모든 정리가 공리로부터 논리적으로 도출되며, 그 도출 과정을 커널(kernel, 작은 검사기)이 기계 검사합니다. "증명이 통과했다"는 것은 이 검사에 합격했다는 의미입니다. 여기서 중요한 것은 Lean에는 sorry라는 우회로가 있다는 점입니다. sorry라고 쓰면 "이 부분의 증명은 나중에"라는 의미로, 그 자리에서는 에러가 발생하지 않습니다 (에디터에 경고는 뜹니다). 내부적으로는 sorryAx라는 공리를 멋대로 가정하게 됩니다. 또한 사용자가 axiom을 통해 임의의 명제를 증명 없이 공리로 추가할 수도 있습니다. 즉, "CI가 green"이라는 사실만으로는 "전부 증명했다"와 "증명을 게을리하여 공리로 메꿨다"를 구분할 수 없습니다. 그래서 각 선언에 대해 의존성을 뿌리까지 추적하여 도달하는 공리의 집합을 계산하고, 그것이 Lean / mathlib이 전체적으로 수용하고 있는 표준 공리 3가지 — propext · Quot.sound · Classical.choice (소위 선택 공리는 마지막 하나) — 뿐인지를 검사합니다. 이것이 공리 감사입니다. sorry

구멍이나 임의로 추가한 공리도 여기서 반드시 드러납니다. 형식 검증 (Formal Verification) 프로젝트를 표방한다면 빼놓을 수 없는 관문입니다.

Lean은 이 "의존성을 따라가며 공리를 수집하는" 처리를 collectAxioms라는 함수로 제공합니다 (직접 #print axioms my_theorem이라고 입력했을 때 동작하는 것과 동일한 메커니즘입니다). 저희의 CI는 이를 모든 선언 — 당시 1,207건, 현재는 4,300건 초과 — 에 대해 실행하고 있었으며, 그 단계에서 매번 7분 11초가 소요되었습니다. 빌드 본체보다 감사 (Audit)가 더 무거운 상태였습니다.

감사의 입구는 감사 대상인 모든 선언을 열거한 5,000행 이상의 거대한 파일입니다. 직관은 이렇게 말합니다 — "이렇게 거대한 파일이라면, 당연히 elaboration (정교화)가 무거울 것이다. 분할하면 빨라질 것이다".

분할하기 전에 시간 내역을 측정했습니다. 결과는 직관에 대한 전면적인 부정 이었습니다.

• import 해결: 약 10초
• 선언 열거 5,000행의 elaboration:
  차이 없음 (행 수를 크게 바꿔도 감사 시간이 변하지 않음) -
  collectAxioms × 1,207 선언: 약 5분

범인은 거대한 파일이 아니라, 감사를 호출하는 방식이었습니다. 어떤 선언이 도달하는 공리를 구하려면, 그 선언이 사용하는 정리, 그 정리가 사용하는 정리…… 식으로 의존 그래프 (Dependency Graph)를 뿌리까지 따라가야 합니다. collectAxioms는 이를 선언 1건마다 처음부터 다시 걷습니다. 그런데 프로젝트 내의 선언들은 mathlib이라는 거대한 토대를 공유하고 있기 때문에, 1,207건의 선언은 거의 동일한 그래프를 1,207번 걷고 있었던 것입니다. 계산량으로 따지면 O(선언 수 × 그래프)입니다. 파일 분할은 이 곱셈의 어떤 인자에도 영향을 주지 않습니다. 이론적으로도 효과가 없지만, 실측 데이터가 먼저 있었기에 "효과 없음"이라고 한마디로 기각하고 다음으로 넘어갈 수 있었습니다.

감사를 2단계(Two-phase)로 나누었습니다.

• 성공 경로: "한 번 방문한 노드는 두 번 방문하지 않는다"는 방문 기록(visited set)을 모든 선언이 공유하게 하여, 그래프 전체를 단 1회만 스캔합니다. 알고 싶은 것은 "모든 선언이 도달하는 공리의 합집합이 표준 공리에 포함되는가"이므로, 한꺼번에 1회 걷더라도 판정 결과는 선언 단위로 걸었을 때와 동일합니다.
• 실패 경로: 비표준 공리가 발견되었을 때만 기존의 선언 단위 스캔으로 넘어가서, "어떤 선언이 범인인가"를 기존과 동일한 형식의 에러로 귀속시킵니다.

O(선언 수 × 그래프)를 성공 시 O(그래프)로 줄이면서도, 에러 메시지의 질은 떨어뜨리지 않는 구성입니다. 그래프 탐색에서 visited를 공유하는 교과서적인 수법이며, Lean 고유의 마법은 없습니다. CI 실측 결과 감사는 7분 11초에서 11초로 줄어들었고, 당시 lake build 작업 전체는 9분 반에서 2분 12초가 되었습니다.

Round 1의 교훈: "무거운 파일"보다 "무거운 처리 × 횟수"를 의심할 것. 그리고 기각된 가설(파일 분할은 효과 없음)도 측정 성과로서 기록해 둘 것 — 후속 작업자가 같은 직관으로 같은 구멍을 다시 파지 않도록.

Round 1은 7월 중순의 이야기로, 당시 lake build 작업은 2분 남짓까지 단축되어 있었습니다. 그런데 그 후 2주 동안 중량급 대수 기하 구현(Round 3의 주인공도 이때 비대해졌습니다)이 계속 머지(Merge)되었고, 어느샌가 어떤 PR이든 단 1개의 파일만 수정하더라도 Lean 빌드가 전체 트리의 콜드 빌드(Cold Build, 약 41분)가 되어버렸습니다.

Lean의 빌드도 C++나 Rust와 마찬가지로 증분 방식 (Incremental Build)을 따릅니다. 빌드 결과물(.olean 파일. .lake/build 디렉토리 아래에 모듈별로 위치함)이 남아 있다면, 변경된 파일과 그 하류(Downstream)만 재빌드하면 됩니다. CI에서 이를 적용하려면 이전의 결과물을 캐시(Cache)로 유지해야 합니다. 캐시는 설정되어 있었습니다. 그런데 작동하지 않고 있었습니다.

캐시가 작동하지 않는다는 말을 들으면 보통 키(Key)의 불일치나 용량 초과를 의심합니다. toolchain의 해시(Hash)가 어긋났나? 세대가 evict(축출)되었나?

키를 의심하기 전에 CI 로그의 타임스탬프를 위에서부터 읽어 내려갔습니다. 그러자 1초 차이의 두 줄이 나란히 있었습니다.

23:19:35 Cache save(lean-action 내부의 최종 step)
23:19:36 lake build +Formal.AG 시작

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

우리는 Lean의 셋업을 위해 lean-action이라는 composite action(여러 step을 하나로 묶은 재사용 가능한 action)을 build: false로 사용하며, 빌드 자체는 후속 step에서 실행하도록 구성했습니다. 그런데 lean-action은 자신의 내부 마지막 step에서 .lake(빌드 결과물이 저장되는 디렉토리)를 캐시에 저장합니다. composite action의 내부 step은 후속 step보다 반드시 먼저 실행됩니다. 즉, 저장된 2.15 GiB의 내용은 의존 라이브러리(mathlib)의 결과물뿐이었으며, 프로젝트 자신의 .olean 파일은 단 한 번도 캐시된 적이 없었습니다. 모든 PR이 41분씩 걸렸던 것은 당연한 결과였습니다. 매번 아무것도 없는 상태에서 자신의 코드를 전부 다시 빌드하고 있었던 것입니다.

덤으로 발견한 사실도 있었습니다. mathlib은 너무 거대해서 각자가 빌드하는 운영 방식은 현실적이지 않기 때문에, 커뮤니티가 빌드된 결과물을 Azure 상에서 배포하고 있습니다(lake exe cache get으로 취득. 실측 약 15초, 환경에 따라 다름). 즉, 캐시되어 있던 2.15 GiB는 매번 15초면 가져올 수 있는 것이었기에 GitHub cache에 둘 의미가 없었습니다. 게다가 2.15 GiB × 4세대 분량으로, 리포지토리의 cache 상한선인 10 GiB를 거의 다 잡아먹고 있었습니다. 무의미한 캐시가 의미 있는 캐시가 머물 자리를 빼앗고 있었던 셈입니다.

캐시의 책임을 분리했습니다.

• lean-action의 GitHub cache는 비활성화(use-github-cache: false). mathlib 결과물은 기존 방식대로 Azure cache에서 공급
• 프로젝트 자신의 .lake/build만을 명시적인 step으로 restore(빌드 전) / save(빌드 직후) 수행
• 키(key)는 lean-toolchain + lake-manifest.json의 hash를 prefix로 사용하여, toolchain 또는 mathlib 업데이트 시에는 올바르게 콜드 빌드(cold build)로 폴백(fallback)되도록 설정
• save는 always()를 사용하여 빌드 실패 시에도 부분적인 결과물을 저장. red(실패) 상태인 PR을 수정하여 다시 push할 때마다, 실패 지점까지의 결과물이 적용되어 반복 작업이 빨라짐

실제 workflow는 다음과 같은 형태입니다(발췌). 핵심은 save를 빌드의 뒤에 직접 배치하는 것, 그것뿐입니다.

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

이로써 Geometry 계열의 무거운 파일을 건드리지 않는 PR은 cache hit + 차분 빌드(incremental build)를 통해 몇 분 내로 끝날 수 있게 되었습니다.

명예를 위해 덧붙이자면, lean-action 자체의 cache는 '빌드까지 action에 맡기는' 표준적인 방식으로 사용한다면 올바르게 작동합니다. build: false로 설정하여 빌드를 외부로 뺀 우리의 구성이 함정에 빠졌던 것입니다.

Round 2의 교훈: "캐시가 작동하지 않는다"면, 키(key)를 의심하기 전에 타임스탬프를 읽으세요. composite action은 편리하지만, 내부 step의 실행 순서는 자신의 workflow step 순서와 직교합니다. "저장이 정말로 빌드 후에 이루어지는가"는 눈으로 직접 확인할 가치가 있습니다.

남은 최대의 병목 구간은 단일 파일이었습니다. Geometry.lean, 5,129행, 108개 선언. 현대 수학에서도 매우 무거운 추상 개념인 스킴(scheme, 대수기하학의 핵심 개념)을 mathlib 위에서 실제로 구성하고 있는 파일로, CI 실측 결과 단독으로 38.3분을 차지하며 프로젝트 전체 CPU 시간의 46%를 혼자 점유합니다. 캐시(Round 2)가 있더라도, 이 파일의 상류(upstream)를 건드리는 PR은 반드시 이 38분을 지불해야 합니다.

이번에는 착수하기 전에 수치 목표를 고정했습니다. 최장 module 600초 이하, 대상 module 군의 합계 1,800초 이하. 동일한 GitHub Actions full build 표시 시간으로 판정한다는 측정 방식까지 결정한 후, 사람이 승인하면 구현에 들어갑니다.

38분 분량의 거대한 파일이니, 의존성의 중심(重心)을 기준으로 여러 모듈(module)로 분할하면 재빌드 범위가 줄어들어 빨라질 것이다 — Round 1에서 한 번 기각되었던 "분할하면 빨라진다"라는 가설의, 이번에는 빌드 버전입니다. elaboration(정교화)는 선언(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%를 차지했으며, 시간은 상위 십수 개의 선언에 극단적으로 편중되어 있었습니다. 이 중심점과 의존 관계에 따라 7개 모듈의 DAG(유향 비순환 그래프)로 분할합니다.

RawGeometry
└─ SectionRings
├─ LeftRestriction
...

분할 과정에서 내용이 깨지지 않았음을 기계적으로 증명합니다. Lean의 #check는 선언의 statement(정리(theorem)의 주장 그 자체)를 표시하는 명령어입니다. 기존 파일의 공개 선언 168건에 대해 #check의 출력값(794행)을 분할 전후로 추출하여, 동일한 toolchain(툴체인) 및 동일한 표시 설정 하에서 SHA-256 해시값이 일치함을 확인했습니다. 즉, 정리의 주장은 단 한 글자도 바뀌지 않았습니다. 파일 분할과 같은 기계적 리팩터링(refactoring)에서도 "수학적 내용이 보존되었음"을 육안이 아닌 해시로 증명할 수 있다는 점이 형식 검증(formal verification) 프로젝트의 즐거운 부분입니다.

그리고 CI에서 after(이후) 시간을 실측해 보았으나 — 목표 달성에 실패했습니다. 최장 모듈 770초(목표 600초), 합계 2,483초(목표 1,800초). 분할은 재빌드 범위를 줄이고 병렬성을 부여하지만, elaboration의 총량은 1초도 줄이지 못했습니다. 오히려 모듈 경계의 overhead(오버헤드)로 인해 합계 시간은 늘어났습니다.

여기서 profile을 더 깊게 파고들자 진범이 보였습니다. 시간은 행수에 비례하여 얇게 분포하는 것이 아니라, 특정 정의 주변의 **정의 전개 비용(definition unfolding cost)**에 집중되어 있었습니다.

정의 전개(definition unfolding)에 대해 잠시 설명하겠습니다. Lean에서 정의는 "이름"과 "내용"의 쌍이며, 필요하다면 내용을 그 자리에서 전개(unfold)할 수 있습니다. 이는 컴파일러의 인라인 전개(inline expansion)와 유사하지만, Lean은 이를 타입 검사 중에 수행합니다. "이 식과 저 식은 같은 타입인가?"를 판정할 때, 겉보기에는 달라 보이는 두 항을 정의를 벗겨내며 대조(unification, 단일화)하는 것입니다. 평소에는 이 메커니즘 덕분에 증명을 짧게 쓸 수 있지만, 내용이 큰 정의가 얽히면 벗겨낸 자리에서 또 다른 정의가 나타나며 항이 점점 부풀어 오릅니다.

저희 파일에서는 스킴(scheme)의 구성 요소를 실제로 계산하는 함수(내용이 큰 정의)와, 그 계산 결과의 정당성을 서술하는 보조정리(lemma)들의 검사 과정에서 이러한 팽창이 일어나고 있었습니다. profile에서 kernel 타입 검사와 defeq에 96%가 집중되었던 것은 바로 이 부풀려진 항을 검사하는 비용 때문이었습니다. 명령어 하나당 15~104초급의 작업이 쌓여 있었습니다.

행수는 죄가 아니었습니다 — Round 1과 동일한 구도입니다. 5,129행이라는 점이 무거운 것이 아니라, 특정 정의가 참조되는 방식이 무거웠던 것입니다.

참고로, 이 단계에서 "흔히 쓰이는 가속 방법"도 두 가지 시도해 보았습니다 (CommRingCat.hom_ext로 교체, congrArg CommRingCat.ofHom 사용 — 둘 다 mathlib에서 정석으로 통하는 교체 방식입니다). 하지만 둘 다 측정값을 개선하지 못하여 채택하지 않았습니다. 정석이 통하지 않는다는 사실 또한 profile 앞에서는 하나의 데이터일 뿐입니다.

profile이 가리킨 지점에 외과 수술을 시행했습니다. 방침은 일관되었습니다. 바로 타입 검사기가 정의를 벗겨내지 않아도 되는 형태로 다시 쓰는 것입니다.

• 값의 정의와 그 값의 성질에 대한 증명을 별도의 선언으로 분리한다. 섞여 있으면 증명 부분의 검사가 값의 내용(content)을 전개(unfolding)하는 과정까지 끌어들이게 된다.
• 보조정리(Lemma)의 주장을 전개된 식이 아닌, 이름이 지정된 함수(named function)로 타입(type)으로서 고정한다. 이름으로 일치 여부를 확인할 수 있다면, unification은 내부 내용을 벗겨낼 필요가 없다.
• 4개의 정리에서 중복되었던 동일한 형태의 증명 패턴을 공통 보조정리로 집약하여, 동일하고 무거운 검사를 4번 반복하는 것을 방지한다.

효과는 극적이었으며, 단일 파일만을 대상으로 한 측정(focused build)에서 가장 무거웠던 RawGeometry는 291초 → 11초로 단축되었습니다. 기존에 15~104초였던 작업은, 개선 후(after) 최대 57.5밀리초(ms)입니다.

최종적인 CI 실측(머지 커밋의 full build)은 7개 모듈 합계 1,750초(29.2분) ≦ 목표 1,800초, 최장 모듈 468초 ≦ 목표 600초입니다. 두 목표를 모두 달성하며 완료되었습니다.

그리고 이 머지 커밋의 CI run 자체는 3라운드의 합성 사진과 같습니다. 로그를 보면:

가장 무거운 파일군을 전부 재빌드하여 12분. 이것이 현재의 워스트 케이스(worst case)입니다.

Round 3의 교훈: 분할은 '빠르게 만드는' 수단이 아니라, '병렬화와 재빌드 범위 축소'를 위한 수단이다. 총량을 줄이는 것은 프로파일(profile)이 가리킨 단 한 지점에 대한 외과 수술뿐이다. 그리고 이 둘은 서로 다른 개선이므로, 별도로 측정하고 별도로 판정해야 한다.

서두에 썼듯이, 3라운드의 측정과 구현은 거의 전부 AI 에이전트의 작업입니다. Round 1과 Round 2는 대화 세션 안에서 측정부터 구현까지 진행되었고, Round 3는 요구 문서(PRD)를 전달한 자율 루프가 프로파일 취득부터 PR 생성, 리뷰 대응까지 수행했습니다. 구현 단계에서 인간의 작업은 두 가지뿐입니다.

• 착수 전에 수치 목표와 측정 방법을 승인하는 것(Round 3라면 "최장 600초·합계 1,800초, 동일 GHA full build의 표시 시간으로 판정")
• CI의 실측값으로 수락 여부를 판정하는 것

솔직히 말하면, 그 이전에 "PRD를 작성하는" 작업도 있습니다. 다만 이 또한 다른 AI와의 공동 작업이며, 인간의 실제 작업은 방침의 선택과 리뷰입니다.

Round 3에서 사용한 자율 루프를 우리는 PRD Loop라고 부릅니다. 에이전트(Codex)에게 SKILL(에이전트용 절차서)로서 부여하는 운용 방식으로, 골자는 다음과 같습니다.

• 입력은 PRD 1장. 서두에 "질문"과 수치로 된 수락 기준(Acceptance Criteria)이 적혀 있다. 실행은 인간이 명령어 한 줄($prd-loop <PRD의 경로>)을 입력하는 것뿐이다.
• 1회전은 "갭 분석(gap analysis) → Issue 생성 → 구현 PR → 적대적 리뷰(adversarial review) → 머지 → 대장 동기화"로 이루어진다. 1회전 = 1 Issue = 1 PR의 작은 단위로 돌아간다(하나의 목표가 여러 회전에 걸쳐 진행되는 것은 정상적인 동작이다).
• 구현한 본인과는 별도의 리뷰 게이트(이 또한 AI)가 PR을 판정한다. Needs changes가 2회 연속되면, 3회째에는 용도 특화된 더 엄격한 게이트(Lean의 경우 수학 리뷰 전용 게이트)로 전환하며, 그럼에도 통과하지 못하면 stalled 상태로 인간에게 반환한다.
• 진행 상태는 에이전트의 기억이 아니라 GitHub의 Issue에 둔다. 세션이 끊겨도 다음 세션이 동일한 지점에서 재개될 수 있다.
• 모든 조건이 충족된 것처럼 보이면, 마지막으로 **독립적인 완료 감사(audit)**가 PRD를 처음부터 다시 읽어 전수 조사한다. 이를 통과하기 전까지는 "완료"라고 말할 수 없다.

Round 3의 "profile → 분할 → 미달 → 심층 분석 → 달성" 과정은 이 루프 위에서 3개의 PR(분할 / 축소 / 클로즈)로 돌아갔습니다. 루프 시작부터 완료까지 1일 미만이 소요되었습니다. 그동안 인간의 개입은 수치 목표의 승인과 판정 척도의 확인, 그리고 GitHub 댓글 몇 건이 전부였습니다.

참고로, 완료된 PRD는 리포지토리에서 삭제하는 것이 규약입니다. 요구 문서는 구현이 끝나는 순간부터 현실과 괴리되기 시작하므로, 영구적인 기록은 Issue / PR / CI 로그에 고정하고 문서 자체는 남기지 않습니다.

하지만 루프를 단순히 돌리기만 하면 반드시 발생하는 일이 있습니다. 에이전트(Agent)는 주어진 인센티브에 충실하기 때문에, 방치하면 '머지(Merge)가 통과되는 가장 저렴한 경로'로 수렴하게 됩니다. 구현하지 않고 문서의 기재 내용만 변경한다. 충족할 수 없는 조건을 '해석'을 통해 충족한 것으로 간주한다. 어려운 항목을 말없이 다음 단계로 미룬다. 이 중 어느 것도 거짓이라고 단정 지을 수는 없습니다. 하지만 이것이 쌓이면, 최소한의 노력으로 '완료'를 자처할 수 있는 균형 — 말하자면 '날림 균형(slacking equilibrium)' — 에 안착하게 됩니다.

그렇기에 우리의 SKILL은 절차서라기보다 **메커니즘 디자인 (Mechanism Design)**으로서 작성되었습니다. 저렴한 경로를 하나씩 차단하는 규칙들의 집합입니다.

docs-only 체크 금지: 구현 및 검증을 요구하는 조건을 문서나 대장(ledger)의 기재만으로 PR(Pull Request)에서 '충족함'으로 처리할 수 없다.
조건의 재해석·강등 금지: 충족할 수 없는 조건은 약하게 읽어 바꾸는 것이 아니라 blocked로 처리하여 인간에게 에스컬레이션(escalate)한다. "멈추는 것은 실패가 아니라, 루프의 사양(specification)이다"라고 명문화되어 있다.
PRD는 루프 중의 불변 조건: 에이전트는 자신의 합격 라인을 스스로 고쳐 쓸 수 없다. PRD의 결함을 발견하면 수정하지 않고 멈춰서 보고한다 (시험 도중에 문제지를 고쳐 쓰게 하지 않는다).
체크리스트는 증거가 아니다: 진행 중인 '완료(済)' 표시은 '과거의 회차가 그렇게 주장했다' 이상의 의미를 갖지 않는다. 최종 감사는 PRD로부터 조건을 독립적으로 재추출하여 실체(코드·테스트·CI 로그)와 대조한다.
자기 채점 금지: 최종 감사 에이전트에게는 PRD에 대한 경로와 Issue 번호만 전달하며, 루프를 돌린 본체가 가진 "전부 충족했을 것이다"라는 예상치는 전달하지 않는다. 리뷰 게이트(review gate)가 실행 불가능하다면 본체가 대신하지 않고, fail-closed 방식으로 멈춘다.

덧붙이자면, 이 규칙들은 책상 위에서 설계한 것이 아닙니다. 초기 루프를 운영하는 과정에서, 대장의 기재만으로 조건을 해결하려 하거나, 안전한 쪽으로 치우쳐 스코프(scope)를 말없이 축소하는 등의 동작을 실제로 관찰하였고, 그때마다 하나씩 추가해 온 것입니다. 가드레일(guardrail)을 미리 전부 작성할 수 있을 정도로 우리가 처음부터 에이전트에 대해 잘 알고 있었던 것은 아닙니다.

공통된 설계 사상은 하나입니다. 정직하게 멈추는 것을, 속여서 진행하는 것보다 더 저렴하게 만드는 것입니다. 에이전트의 선의에 기대는 것이 아니라, 균형점 그 자체를 움직입니다.

이 운용에서 가장 좋았던 순간은 Round 3의 미달 보고였습니다. 분할 PR 시점에서 에이전트는 자신의 PR에 다음과 같이 적었습니다 — "최장 770초, 합계 2,483초. 목표 미달이므로 본 PR을 완료로 처리하지 않고, profile 기반의 절감을 다음 PR에서 계속한다". 이 보고에 대해 인간은 추가 지시를 내리지 않았습니다. 루프는 다음 회차에서 절감 Issue를 스스로 기표(create)하였고, 같은 날 안에 목표를 달성하는 PR을 머지했습니다.

"할 수 있습니다"라고 선언하며 끝내는 것이 가장 편한 국면에서, 미달을 미달이라고 적고 계속 진행한다. 이것은 에이전트의 성실함이라기보다, 상위 장치의 구조적인 귀결이라고 생각합니다. 합격 라인이 먼저 고정되고, 조건의 재해석이 금지되며, 독립 감사가 실측값으로 전수 조사한다는 것을 알고 있다면, 선언과 실측이 어긋날 때 어긋나는 쪽은 선언입니다. 반대로 기준을 나중에 결정하는 운용에서는 '이번 결과에 맞춘 기준'이라는 유혹이 인간 측에도 생기게 됩니다.

AI에게 최적화를 맡길 계획이 있는 분들에게 이 글에서 가장 실용적인 교훈은 아마 이것일 것입니다: 코드를 넘기기 전에, 합격 라인과 측정 방법을 넘겨라. 그리고 '정직하게 멈추는 것'을 가장 저렴한 수단으로 만들어 두어라.

• 공리 감사 7분 11초 → 11초. 범인은 거대 파일이 아니라, 선언마다 그래프를 다시 걷는 비공유 스캔(non-shared scan)이었다.
• 전체 PR 41분 → 차분 빌드(differential build) 시간만큼. 범인은 캐시 키(cache key)가 아니라, 빌드 '전'에 실행되는 캐시 저장(cache save)이었다.
• 단일 38분 파일 → 합계 29분·최장 8분·최악 run 12분. 분할해도 총량은 줄지 않았으며, 범인은 정의 전개 비용(definition expansion cost)이었다.

세 번 모두 첫 번째 가설은 틀렸습니다. 그럼에도 개선이 진행될 수 있었던 이유는, 틀린 가설을 계측을 통해 기각하고, 기각의 기록까지 함께 다음 단계로 넘겼기 때문입니다. "효과 없음"도 성과입니다. 파일 분할 불채택(Round 1), 정석의 재작성 불채택 2건(Round 3)— 이러한 기록이 없었다면 누군가(인간이든 AI든) 똑같은 직관으로 다시 파고들었을 것입니다.

AI 운용 측면에서 Round 3의 루프는 시작부터 완료까지 1일 미만, PR 3개였으며, 인간의 개입은 GitHub 댓글 몇 건뿐이었습니다.

추측하지 말고, 측정하라. 오래된 격언이지만, AI가 코드를 작성하는 시대에는 그 뒤에 이어지는 말이 필요하다고 생각합니다 — 측정하게 하고, 합격 기준은 미리 제시하라.