【Lean最適化】約40分かかっていたCIを劇的に改善した話

本記事は、Hashnodeに公開したTaming a 40-Minute Lean CI: Three Rounds, Three Wrong Suspectsの日本語版です

Lean 4 + mathlib のプロジェクトで、PR を出すたびに CI が 41 分かかっていました。今は、最も重いファイル群を全部再ビルドする最悪ケースでも 12 分、普通の PR なら差分ビルドで数分です。

改善対象	before	after
公理監査 (Kernel axiom audit)	7分11秒	11秒
通常の PR のビルド	41分(一律フルビルド)	数分(差分ビルド)
最悪ケース(最重量ファイル群を全再ビルド)	41分(同上)	12分

この記事は、その改善を 3 ラウンドに分けて記録したものです。各ラウンドを 課題 → 仮説 → 検証 → 解決 の順で書きます。先に種明かしをすると、3 回とも最初の仮説 — 直観が名指しした犯人 — は無実でした。改善の主役は個々のテクニックではなく、仮説を淡々と棄却していった計測です。

Lean 固有の概念は出てくるたびに説明するので、Lean を知らなくても読めるはずです。

そしてもう一つ。この 3 ラウンドの計測と実装は、ほぼすべて AI エージェントが行いました(Round 1・2 は人間が横にいる対話セッション、Round 3 は要求文書を渡した自律ループです)。人間(私)がやったのは、数値目標の承認と受け入れ判定だけです。後半では、その運用 — 特に AI を安易な解に逃がさない仕組み — についても書きます。

前提: どんなプロジェクトか

対象は、これまでの記事でも扱ってきた AlgebraicArchitectureTheoryV2 — ソフトウェアアーキテクチャ理論を Lean 4 で形式検証しているモノレポです。

この記事に登場する Lean の道具立ては、次の 5 つで全部です。

用語	何であるか
Lean 4	定理証明支援系。数学の証明を機械検査できるプログラミング言語。「証明をコンパイルが通る形で書く」言語だと思ってください
mathlib	Lean の巨大な数学ライブラリ。記事執筆時点で 150 万行超のコミュニティ資産で、これに依存すると「数学の標準ライブラリ」が使える代わりに、ビルドの規模も相応になる
lake	Lean のビルドツール。Rust の cargo、JS の npm に相当。ファイル(module)単位でビルドし、成果物として .olean ファイルを吐く
elaboration	Lean の「コンパイル」に相当する処理。型推論、暗黙引数の解決、証明の検査をまとめて行う。Lean のビルド時間のほとんどはこれ
宣言 (declaration)	定義や定理の 1 件 1 件。この記事では「監査対象 4,000 件超」のように数えている単位

規模感を先に共有しておくと、監査対象の宣言は 4,000 件超。その中に、代数幾何のスキーム構成を含む重量級ファイルがあり、これ単体のビルドに 38 分かかっていました。

CI は GitHub Actions で、lake build に加えて Kernel axiom audit(公理監査) — 全定理が本当に証明済みか、証明にズルがないかの機械検査 — を毎 PR で回しています。このゲート自体は外せません。中身は Round 1 で説明します。

Round 1: 公理監査 7分11秒 → 11秒

課題

Lean では、すべての定理は公理から論理的に導出され、その導出をカーネル(小さな検査器)が機械検査します。「証明が通った」とは、この検査に合格したという意味です。ここで重要なのは、Lean には sorry という抜け道があることです。sorry と書くと「この部分の証明は後で」という意味で、その場ではエラーになりません(エディタに警告は出ます)。内部的には sorryAx という公理を勝手に仮定したことになります。また、ユーザーが axiom で任意の命題を無証明のまま公理として追加することもできます。

つまり「CI が green」だけでは、「全部証明した」と「証明をサボって公理で埋めた」を区別できないのです。そこで各宣言について、依存を根までたどって 到達する公理の集合を計算し、それが Lean / mathlib が全体で受け入れている標準公理 3 つ — propext・Quot.sound・Classical.choice(いわゆる選択公理はこの最後の 1 つ)— だけであることを検査します。これが公理監査です。sorry の穴も、勝手に追加した公理も、ここで必ず露見します。形式検証プロジェクトを名乗るなら外せないゲートです。

Lean はこの「依存をたどって公理を集める」処理を collectAxioms という関数として提供しています(手元で #print axioms my_theorem と打ったときに動くのと同じ仕組みです)。私たちの CI はこれを全宣言 — 当時 1,207 件、現在は 4,300 件超 — に対して回していて、そのステップに毎回 7 分 11 秒かかっていました。ビルド本体より監査のほうが重い、という状態です。

仮説

監査の入口は、監査対象の全宣言を列挙した 5,000 行超の巨大ファイルです。直観はこう言います — 「こんな巨大ファイル、elaboration が重いに決まっている。分割すれば速くなるはずだ」。

検証

分割する前に、時間の内訳を測りました。結果は直観の全面否定でした。

• import の解決: 約 10 秒
• 宣言列挙 5,000 行の elaboration: 差分ゼロ(行数を大きく変えても監査時間が動かない)
• collectAxioms × 1,207 宣言: 約 5 分

犯人は巨大ファイルではなく、監査の呼び方でした。ある宣言が到達する公理を求めるには、その宣言が使っている定理、その定理が使っている定理…… と依存グラフを根までたどる必要があります。collectAxioms はこれを宣言 1 件ごとに最初から歩き直します。ところがプロジェクト内の宣言たちは mathlib という巨大な土台を共有しているので、1,207 件の宣言はほぼ同じグラフを 1,207 回歩いていたのです。計算量でいえば O(宣言数 × グラフ) です。ファイル分割はこの積のどちらの因子にも触りません。理屈の上でも効果がないのですが、実測が先にあったからこそ「効果なし」と一言で棄却して次へ進めました。

解決

監査を二相化しました。

1. 成功経路: 「一度訪れたノードは二度たどらない」訪問済み記録(visited set)を全宣言で共有し、グラフ全体を 1 回だけ走査します。知りたいのは「全宣言が到達する公理の和集合が標準公理に収まるか」なので、まとめて 1 回歩いても判定結果は宣言単位で歩いた場合と同値です
2. 失敗経路: 非標準公理が見つかったときだけ、従来の宣言単位走査に落ちて「どの宣言が犯人か」を従来と同じ形式のエラーで帰属します

O(宣言数 × グラフ) を成功時 O(グラフ) に潰し、エラーメッセージの質は落とさない構成です。グラフ探索の visited 共有という教科書的な手筋で、Lean 固有の魔法はありません。CI 実測で監査は 7 分 11 秒から 11 秒になり、当時の lake build job 全体は 9 分半から 2 分 12 秒になりました。

Round 1 の教訓: 「重いファイル」より「重い処理 × 回数」を疑う。そして、棄却された仮説(ファイル分割は効果なし)も計測の成果として記録しておく — 後続の誰かが同じ直観で同じ穴を掘り直さないために。

Round 2: 全 PR が 41 分 — キャッシュはビルドの「前」に保存されていた

課題

Round 1 は 7 月中旬の話で、当時の lake build job は 2 分強まで縮んでいました。ところがその後の 2 週間で重量級の代数幾何実装(Round 3 の主役もこのとき肥大しました)が続けてマージされ、気づけばどの PR も、1 ファイルしか触っていなくても、Lean のビルドが全ツリーのコールドビルド(約 41 分)になっていました。

Lean のビルドも、考え方は C++ や Rust と同じ増分方式です。ビルド成果物(.olean ファイル。.lake/build ディレクトリの下に module ごとに置かれます)が残っていれば、変更されたファイルとその下流だけを再ビルドすればいい。CI でこれを効かせるには、前回の成果物をキャッシュとして持ち越す必要があります。キャッシュは設定してあります。効いていないのです。

仮説

キャッシュが効かないと聞いて普通に疑うのは、キーのミスマッチか容量あふれです。toolchain の hash がずれている? 世代が evict されている?

検証

キーを疑う前に、CI ログのタイムスタンプを上から読みました。すると 1 秒差の 2 行が並んでいました。

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(ビルド直後)する
• キーは lean-toolchain + lake-manifest.json の hash を prefix に持たせ、toolchain / mathlib 更新時は正しくコールドビルドへフォールバック
• save は always() で、ビルド失敗時も部分成果物を保存する。red な PR を修正して push し直すたびに、失敗地点までの成果物が効くので反復が速い

実際の workflow は次の形です(抜粋)。ポイントは save をビルドの後ろに自分で置くこと、それだけです。

- name: Restore Formal build cache
  uses: actions/cache/restore@v5
  with:
    path: .lake/build
    key: formal-build-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-${{ github.sha }}
    restore-keys: |
      formal-build-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-

- name: Build
  run: lake build +Formal.AG

- name: Save Formal build cache
  if: always()
  uses: actions/cache/save@v5
  with:
    path: .lake/build
    key: formal-build-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-${{ github.sha }}

これで Geometry 系の重量ファイルに触らない PR は、cache hit + 差分ビルドの数分に収まるようになりました。

名誉のために付け加えると、lean-action 自体の cache は「ビルドまで action に任せる」標準的な使い方なら正しく機能します。build: false にしてビルドを外側に持つ、という私たちの構成が罠を踏んだのです。

Round 2 の教訓: 「キャッシュが効かない」は、キーを疑う前にタイムスタンプを読む。composite action は便利ですが、内部 step の実行順は自分の workflow の step 順と直交します。「保存は本当にビルドの後か」は目視する価値があります。

Round 3: 単体 38 分の Geometry.lean — 分割しても速くならなかった

課題

残った最大のボトルネックは単一ファイルでした。Geometry.lean、5,129 行・108 宣言。現代数学でも重量級の抽象であるスキーム(代数幾何の中心概念)を mathlib の上で実際に構成しているファイルで、CI 実測で単体 38.3 分、プロジェクト全体の CPU 時間の 46% を一人で占めます。キャッシュ(Round 2)があっても、このファイルの上流に触る PR は必ずこの 38 分を払います。

今回は着手前に数値目標を固定しました。最長 module 600 秒以下、対象 module 群の合計 1,800 秒以下。同一の GitHub Actions full build の表示時間で判定する、と測り方まで決めて、人間が承認してから実装に入ります。

仮説

38 分の巨大ファイルなのだから、依存の重心で複数 module に分割すれば、再ビルド範囲が縮んで速くなるはずだ — Round 1 で一度棄却された「分割すれば速くなる」仮説の、今度はビルド版です。elaboration は宣言ごとに走るので、今度は筋が良さそうに見えます。

検証

まず宣言別 profile を取りました。Lean には profiler が組み込まれていて、コマンド 1 本で「どの宣言のどの処理に何秒かかったか」まで出せます。今回使ったのはこれです。

lake env lean --profile --json \
  -Dprofiler.threshold=10 \
  -Dtrace.profiler=true -Dtrace.profiler.threshold=10 \
  -Dtrace.profiler.output=geometry-before-trace.json \
  Formal/AG/Examples/StandardGeometryReference/Geometry.lean

内訳は、kernel の型検査が 57%、defeq(2 つの項が定義上等しいかの判定)が 39% で、時間は上位十数個の宣言に極端に偏っていました。この重心と依存関係に従って、7 module の DAG に分割します。

RawGeometry
└─ SectionRings
   ├─ LeftRestriction
   ├─ RightRestriction
   ├─ OverlapLeftRestriction
   └─ OverlapRightRestriction   ※ この4つは相互 import なし = 並列ビルド可
      └─ Scheme

分割で壊していないことは機械的に証明します。Lean の #check は宣言の statement(定理の主張そのもの)を表示するコマンドです。旧ファイルの公開宣言 168 件について #check の出力(794 行)を分割前後で取り、同一 toolchain・同一表示設定のもとで SHA-256 が一致することを確認しました — つまり定理の主張は 1 文字も変わっていません。ファイル分割のような機械的リファクタリングでも、「数学的内容が保存されていること」を目視でなくハッシュで示せるのは、形式検証プロジェクトの気持ちいいところです。

そして CI で after を実測すると — 未達でした。最長 module 770 秒(目標 600 秒)、合計 2,483 秒(目標 1,800 秒)。分割は再ビルドの範囲を縮め、並列度を与えますが、elaboration の総量は 1 秒も減らしません。module 境界の overhead で、合計はむしろ増えました。

ここで profile を深掘りすると、真犯人が見えました。時間は行数に比例して薄く分布しているのではなく、特定の定義まわりの定義展開費用に集中していたのです。

定義展開について少し説明します。Lean では定義は「名前」と「中身」の対で、必要なら中身をその場に展開(unfold)できます — コンパイラのインライン展開に似ていますが、Lean はこれを型検査の最中に行います。「この式とあの式は同じ型か?」を判定するとき、表面上は違って見える 2 つの項を、定義を剥がしながら突き合わせるのです(unification)。普段はこの仕組みのおかげで証明が短く書けるのですが、中身の大きい定義が絡むと、剥がした先でさらに定義が現れ、項がどんどん膨らみます。

私たちのファイルでは、スキームの構成要素を実際に計算する関数(中身が大きい定義)と、その計算結果の正しさを述べる補題たちの検査で、この膨張が起きていました。profile で kernel 型検査と defeq に 96% が集中していたのは、まさにこの膨らんだ項の検査費用です。1 コマンドあたり 15〜104 秒級の操作が積み上がっていました。

行数は罪ではなかった — Round 1 と同じ構図です。5,129 行あることが重いのではなく、特定の定義の参照のされ方が重かったのです。

なお、この段階で「よくある高速化」も 2 案試しています(CommRingCat.hom_ext への置き換え、congrArg CommRingCat.ofHom の利用 — どちらも mathlib で定石とされる書き換えです)。どちらも計測値を改善せず、不採用としました。定石が効かないことも、profile の前では 1 つのデータです。

解決

profile が指した 1 点に外科手術をしました。方針は一貫していて、型検査器が定義を剥がさずに済む形へ書き換えることです。

• 値の定義と、その値の性質の証明を別の宣言に分離する。混ざっていると、証明部分の検査が値の中身の展開まで引きずってしまう
• 補題の主張を、展開済みの式ではなく名前付きの関数で型として固定する。名前で一致が取れれば、unification は中身を剥がす必要がない
• 4 本の定理に重複していた同型の証明パターンを共通補題へ集約し、同じ重い検査を 4 回払うのをやめる

効果は劇的で、単一ファイルだけを対象にした計測(focused build)で、最重量だった RawGeometry は 291 秒 → 11 秒。旧上位 15〜104 秒だった操作は、after では最大 57.5 ミリ秒です。

最終的な CI 実測(マージ commit の full build)は、7 module 合計 1,750 秒(29.2 分)≦ 目標 1,800 秒、最長 module 468 秒 ≦ 目標 600 秒。両目標を達成して完了です。

そして、このマージ commit の CI run 自体が、3 ラウンドの合成写真になっています。ログを見ると:

step	時間
Restore Formal build cache	3秒(cache hit — Round 2)
Build(7 module 全再ビルドを含む)	9分29秒(分割 DAG の並列 + 軽量化 — Round 3)
Kernel axiom audit	26秒(共有走査 — Round 1)
job 全体	11分57秒

最重量ファイル群を全部再ビルドして 12 分。これが現在のワーストケースです。

Round 3 の教訓: 分割は「速くする」手段ではなく、「並列化と再ビルド範囲縮小」の手段。総量を減らすのは、profile が指した 1 点への外科手術だけ。そして両者は別の改善なので、別々に計測して別々に判定する。

AIエージェントが軸となって改善をした

冒頭に書いたとおり、3 ラウンドの計測と実装はほぼすべて AI エージェントの仕事です。Round 1 と Round 2 は対話セッションの中で計測から実装まで、Round 3 は要求文書(PRD)を渡した自律ループが profile 取得から PR 作成、レビュー対応までを回しました。実装フェーズでの人間の仕事は 2 つだけです。

1. 着手前に、数値目標と測り方を承認する(Round 3 なら「最長 600 秒・合計 1,800 秒、同一 GHA full build の表示時間で判定」)
2. CI の実測値で受け入れを判定する

正直に言えば、その手前に「PRD を書く」という仕事もあります。ただしこれも別の AI との共同作業で、人間の実作業は方針の選択とレビューです。

PRD Loop という運用

Round 3 で使った自律ループを、私たちは PRD Loop と呼んでいます。エージェント(Codex)に SKILL(エージェント向けの手順書)として与えている運用で、骨子は次のとおりです。

• 入力は PRD 1 枚。冒頭に「問い」と Acceptance Criteria(受け入れ条件)が数値で書いてある。起動は人間がコマンド 1 行($prd-loop <PRDのパス>)を打つだけ
• 1 周は「ギャップ分析 → Issue 起票 → 実装 PR → 敵対レビュー → マージ → 台帳同期」。1 周 = 1 Issue = 1 PR の小さい単位で回る(1 つの目標が複数周にまたがるのは正常運転)
• 実装した本人とは別のレビューゲート(これも AI)が PR を判定する。Needs changes が 2 回続いたら、3 回目は用途特化のより厳格なゲート(Lean なら数学レビュー専用ゲート)に切り替え、それでも通らなければ stalled として人間に返す
• 進行状態はエージェントの記憶ではなく GitHub の Issue に置く。セッションが切れても、次のセッションが同じ地点から再開できる
• 全条件が満たされたように見えたら、最後に独立の完了監査が PRD を最初から読み直して全数照合する。これに合格するまで「完了」を名乗れない

Round 3 の「profile → 分割 → 未達 → 深掘り → 達成」は、この輪の上で PR 3 本(分割 / 削減 / クローズ)として回りました。ループの開始から完了まで 1 日弱。その間の人間の介入は、数値目標の承認と判定尺度の確認、あわせて GitHub コメント数件です。

ちなみに、完了した PRD はリポジトリから削除する規約です。要求文書は実装が終わった瞬間から現実とずれ始めるので、恒久的な記録は Issue / PR / CI ログに固定し、文書そのものは残しません。

安易な解に収束させない工夫

ただし、ループを素朴に回すと必ず起きることがあります。エージェントは与えられたインセンティブに忠実なので、放置すると**「マージが通る最も安い経路」に収束する**のです。実装せずにドキュメントの記載だけ変える。満たせない条件を「解釈」で満たしたことにする。困難な項目を黙って後続送りにする。どれも嘘とは言い切れません。しかし積み重なると、労力最小で「完了」を名乗れる均衡 — いわば手抜き均衡 — に落ち着きます。

だから私たちの SKILL は、手順書というよりメカニズムデザインとして書かれています。安い経路を一つずつ塞ぐルール群です。

• docs-only チェックの禁止: 実装・検証を要求する条件を、ドキュメントや台帳の記載だけの PR で「満たした」にできない
• 条件の再解釈・降格の禁止: 満たせない条件は、弱く読み替えるのではなく blocked として人間へエスカレートする。「止まることは失敗ではなく、ループの仕様である」と明文化してある
• PRD はループ中の不変条件: エージェントは自分の合格ラインを書き換えられない。PRD の欠陥を見つけたら、直さずに止まって報告する(試験の最中に問題用紙を書き換えさせない)
• チェックリストは証拠ではない: 進行中の「済」印は「過去の周回がそう主張した」以上の意味を持たない。最終監査は PRD から条件を独立に再抽出し、実体(コード・テスト・CI ログ)と突き合わせる
• 自己採点の禁止: 最終監査のエージェントには PRD へのパスと Issue 番号だけを渡し、ループを回した本体の「全部満たしたはず」という見込みは渡さない。レビューゲートが実行不能なら本体が代替せず、fail-closed で止まる

付け加えると、これらのルールは机上で設計したものではありません。初期のループを運用する中で、台帳の記載だけで条件を済ませようとする、安全側に倒してスコープを黙って縮める、といった挙動を実際に観測し、そのたびに 1 本ずつ追加されてきたものです。ガードレールを先回りで全部書けるほど、私たちは最初からエージェントに詳しかったわけではありません。

共通する設計思想は一つで、正直に止まることを、ごまかして進むより安くすることです。エージェントの善意に期待するのではなく、均衡点そのものを動かします。

一番よかった瞬間は「未達報告」

この運用で一番よかった瞬間は、Round 3 の未達報告です。分割 PR の時点で、エージェントは自分の PR にこう書きました — 「最長 770 秒、合計 2,483 秒。目標未達につき、本 PR で完了とせず、profile 駆動の削減を次の PR で続行する」。この報告に、人間は追加の指示を出していません。ループは次の周回で削減 Issue を自分で起票し、同じ日のうちに目標を達成する PR をマージしています。

「できました」と宣言して終わるのが最も楽な局面で、未達を未達と書いて続行する。これはエージェントの誠実さというより、上の仕掛けの構造的な帰結だと思っています。合格ラインが先に固定され、条件の再解釈が禁止され、独立監査が実測値で全数照合すると分かっていれば、宣言と実測がずれたとき、ずれる側は宣言です。逆に、基準を後から決める運用では「今回の結果に合わせた基準」への誘惑が人間側にも生まれます。

AI に最適化をやらせる予定のある方への、この記事でいちばん実用的な持ち帰りはたぶんこれです: コードを渡す前に、合格ラインと測り方を渡す。そして「正直に止まる」を最安の手にしておく。

まとめ

• 公理監査 7分11秒 → 11秒。犯人は巨大ファイルではなく、宣言ごとにグラフを歩き直す非共有走査だった
• 全 PR 41 分 → 差分ビルド数分。犯人はキャッシュキーではなく、ビルドの「前」に走るキャッシュ保存だった
• 単体 38 分のファイル → 合計 29 分・最長 8 分・ワースト run 12 分。分割では総量は減らず、犯人は定義展開費用だった

3 回とも、最初の仮説は外れました。それでも改善が進んだのは、外れた仮説を計測で棄却し、棄却の記録ごと次に渡したからです。「効果なし」も成果です。ファイル分割不採用(Round 1)、定石の書き換え不採用 2 件(Round 3)— これらの記録がなければ、誰かが(人間でも AI でも)同じ直観でもう一度掘っていたはずです。

AI 運用の面では、Round 3 のループは開始から完了まで 1 日弱・PR 3 本、人間の介入は GitHub コメント数件でした。

推測するな、計測せよ。古い格言ですが、AI がコードを書く時代には続きが要ると思います — 計測させよ、そして合格ラインは先に渡せ。