ImperialViolet

証明の自動化がついに手に入った（2026年7月26日）

Coq、Rocq、Lean といった依存型言語にはずっと惹かれてきた。任意の細かさの不変条件を符号化し、強制できる型システムを組み上げられる。そうした不変条件は、普通の言語ではコメントに落ち着くのがせいぜいで、チームが大きくなる頃には誰も覚えていない。そこから微妙な認識のずれが生まれ、噛み合わないコンポーネントが積み上がっていく。問題に気づく頃には、どのコンポーネントも揃えるのが億劫になるほど育ってしまっている。依存型はそこに誘いをかける。不変条件を形式的に書き下し、機械に検査させればいいのではないか、と。

（余談：Coq は名前を変えた！ 何年も前、プリンストンでの Coq の会議で、英語圏でプログラミング言語が Coq という名前なのは障害になると指摘してみたことがある。聴衆の反応はいまひとつだった。ついでに、Coq と Hoare が多すぎて発表の多くが Tyrion Lannister の演説に聞こえる、という冗談も飛ばした。我ながらうまいし時事にも合っていたが、完全に滑った。あのドラマの最終シーズン前で、みんなが記憶から消し去る前の話だ。）

問題は常に、型システムが強力になるほど証明のコストが上がることだった。かなり単純なことを証明するのに丸一日を溶かした経験なら何度もある。証明を書くのは楽しい。手応えがあって、対話的で、目標がはっきりしている。だがとにかく時間がかかる。私のように何をやっているのか分かっていない人間ならなおさらだ。数時間かけた末に、証明しようとしていた命題が実は_偽_だったと気づく、あの周期的に訪れる苛立ちもそう。この分野の古典的な結果が seL4 プロジェクトの回顧で、エンジニアが十分な経験を積むほどプロジェクトが大きくなっても、証明にかける時間は設計と実装のおよそ10倍だったという。最終的に証明コードの行数は C コードの20倍を超えた。

この負担が依存型言語のプログラミングを極めてニッチなものにし、自動化への試みを後押ししてきた。私が少し知っているのは F* で、SMT solver にこれらの義務を自動で片付けさせようとする。単純なケースは問題ないが、SMT solver が宇宙の彼方へ飛んでいって何時間も走り続け、終わるのかどうかも分からず待たされる状況は簡単に作れる。この手の言語の常用者たちが、solver が何を飲み込むかを第六感で見極め、それを前提にすべてを書くようになるのを何人も見てきた。効果はあるが、ある種の問題を占いにしてしまう。複雑で気まぐれな神に仕える羽目になるわけだ。

重要な事実として、少なくとも理論上は、命題が正しければ証明の中身はどうでもいい。意味があるのは存在だけだ。ただしこれは完全には成り立たない。複雑な要素が二つある。一つは seL4 チームが「証明エンジニアリング」と呼んだもので、コードを変更したときに証明を合わせ直す手間を減らすには、証明をきちんと組織化する必要がある。もう一つは、十分に複雑な証明は型チェッカーを爆発させ、大量のメモリを食い潰しうることだ。

ここで LLM が登場する。証明無関係性と組み合わせれば、極めて強力な証明自動化になりうる。自動化が十分にあれば、証明エンジニアリングにそれほど気を揉まなくて済むかもしれない。型チェッカーを爆発させないよう注意する必要は残るが、私が限られた範囲で試した限り、LLM はそこをうまく避ける。LLM は依存型システムを一気に実用的なものにする可能性がある。試してみたくて Lean で Zstandard の解凍器を書いた。Zstandard そのものにも興味があったのが主な理由だ。

gzip に代わって標準の圧縮ツールになる競争で、Zstandard が勝ちつつあるようだ。同じく LZ77 系の圧縮器だが、エントロピー符号化が優れ、設計にも気が配られていて、解凍速度は驚くほど速い。bzip2 のような美しさは決してないが、現実の実用上の利点を前にしては、Burrows–Wheeler 変換のまばゆい優雅さなど大したものではない。

（測定は標準的なリファレンスマシン、つまり著者が当時使っていたマシンで行われている。y 軸が対数スケールなのにも注意。gzip と Zstandard はそれぞれ別の速度帯にいる。これは Apple のマシンで、Apple の gzip は特別に最適化されている。他所なら gzip はもっと遅いはずだ。）

Zstandard（Yann Collet が開発し、Jarek Duda の先駆的な ANS の仕事の上に成り立っている）にはRFCがあるが、かなり簡潔に書かれている。解凍器を実装するのに必要な情報は揃っているが、圧縮にかなり詳しくないと、何が書いてあるのか飲み込むまで何度も読み返すことになると思う。少なくとも私は 4.1 節を6回読んで、ようやく掴めた気になった。気づくのが遅すぎたのだが、同僚の Nigel Tao が書いた Zstandard の解説は、私が書けたであろう何よりも優れている。Zstandard を理解したいなら、あれを読むべきだ。ここでは最も面白い部分、エントロピー符号化器だけを説明し、ついでに Lean を少し宣伝する。

エントロピー符号化器の仕事は、確率が一様でない記号の集合が与えられたとき、それらからなる列を最小のビット数で符号化することだ。古典的なのは Huffman 符号化器で、二分木を作り、記号を葉に置く。Huffman は最適な前置木を生成する非常に単純なアルゴリズムを示した。記号のリストを取り、確率が最小の二つを見つけ、それらを子として一つの木ノードを作る。この木ノードの確率は二つの子の確率の和で、記号が二つ減り木ノードが一つ増えた集合に対してアルゴリズムを繰り返す。明らかに、アルゴリズムを1ステップ実行するごとに要素の集合は一つ減るので必ず終了し、生成される木は最適だ。Huffman 木は非常に速い。次の n ビット（n は最長符号の長さ）を添字とする表を作ればいい。表の項目が、どの記号が復号されたか、何ビット戻すかを教えてくれる。Huffman 木の欠点は、各記号に整数ビットしか使えないことだ。ある記号が -log2(p) = 2.3 を満たすなら、理想的には 2.3 ビットで符号化したい。だが Huffman は 3 ビットに切り上げるか、切り下げるかを強いる。後者を選べば、他の記号が余分にビットを食うことになる。

Zstandard は Huffman 木を使うが、さらに圧縮率の高いエントロピー符号化器として FSE も持っている。FSE は状態機械だ。状態の数はシンボルの数より多く、各シンボルに割り当てられる状態の割合が、そのシンボルがデータストリーム中に現れる確率にちょうど対応する。たとえばあるシンボルが 50% の確率で現れると見込まれるなら、状態のおよそ 50% が割り当てられる。各状態は三つの値を持つ。その状態に対応するシンボル、その状態にあるときにビットストリームから読み取るビット数、そして基準状態番号——この番号に読み取ったビットを足すと次の状態になる。Huffman 木の問題は整数ビットしか使えないことで、これらの状態が読み取るのも整数ビットだ。だがここに工夫がある。あるシンボルに対して 1.5 ビット読み取りたいなら、その状態の半分は 1 ビットを読み、残りの半分は 2 ビットを読むようにすればいい。こうすれば_平均として_目標を達成できる。状態テーブルは決して転送されない。RFC がシンボル確率のリストからこのテーブルを構築するアルゴリズムを定めているので、転送するのは確率だけで済む。

例を挙げよう。四つのシンボルがあり、16 個の状態を使うとする。するとシンボルの確率は 1/16 の粒度で近似することになる。（より精度の高い確率近似が欲しければ状態を増やせばいい。zstd は実際には 32 個未満の状態を決して使わない。）

state	0	1	2	3	4	5	6	7	8	9	10	11	12	13	14	15
Symbol	A	A	B	D	A	B	C	A	B	C	A	B	C	A	A	B
Num_Bits	2	1	2	4	1	2	3	1	2	2	1	1	2	1	1	1
Baseline	12	0	4	0	2	8	8	4	12	0	6	0	4	8	10	2

どのシンボルの後にもどのシンボルが来てもおかしくないし、あるシンボルが状態を一つしか持たないこともある。だからどのシンボルもあらゆる状態に到達できなければならない。状態 3 を見てみよう。これはシンボル D の唯一の状態だ。唯一だからこそ、4 ビットを読み取る必要がある。それだけあれば他のどの状態も符号化できる。だがシンボル B のようなシンボルを見ると、その状態が要求する読み取りは 1 ビットか 2 ビットだけだ。とはいえ、16 個の可能な次の状態は、シンボル B のこれらの状態によってちょうど分割し尽くされている。つまり、ある特定の状態に対して、それを到達できるシンボル B の状態はちょうど一つある。

再びシンボル B を見ると、その確率は 5/16 だと先に述べた。このシンボルを符号化する理想的なビット数は -log2(5/16) = 1.68 だ。シンボル B には 2 ビットを読む状態が三つ、1 ビットを読む状態が二つある。これらの状態は同じ頻度で使われるわけではないが、使用頻度で重み付けした平均は、量子化された確率に対応する正しい値にほぼぴったり乗る。実際のシンボル確率をより正確に再現したければ、より大きなテーブルを使えばいい。

核心となる工夫はこうだ。より頻繁なシンボルに複数の状態を割り当てると、符号化器は単にシンボルを選ぶだけでなく、そのシンボルのどの状態に落ちるかも選ぶことになり、この選択が次のシンボルへ情報を伝える。小数ビットの情報はここに隠れている。それでもこのエントロピー符号化器はあくまでテーブルベースなので、非常に高速に動作する。

厄介なのは、前向きには導出できないことだ。C、D を符号化したいとしよう。どの C の状態から始めればいいのか。D には状態が一つしかないので、そこに到達できる C の状態しかありえない。D に複数の状態があれば、D の後に何が来るかを考えて、そのうち_どれ_が必要かを知らなければならない。FSE ではシーケンスの末尾から逆向きにたどらざるを得ない。（これはそれほど悪くない。シンボル確率の計算には通常そもそもシーケンス全体を知る必要があるからだ。）さらに、Zstandard の圧縮器はそのためシンボルを逆順に符号化するが、出力は逐次書き込まれるので、解凍器はブロックの末尾に位置を合わせてビットを逆方向に読み、つじつまを合わせなければならない！　これはフォーマットのもっとマクロな詳細に関わるので立ち入らない。詳しくは Nigel の記事を参照してほしい。

基本的なエントロピー符号化器はシンボル間の確率を気にしない。つまり、文字 Q の後に（英語では）U が不釣り合いほど頻繁に続くという事実を活かせない。この冗長性を利用するには別の符号化方式が必要だ。Zstandard ではそれが従来の Lempel–Ziv 構造であり、リテラルバイトや既に復号済みのデータへの後方参照を符号化する。だから FSE は主に、これらの後方参照のオフセットと長さを効率よく符号化するために使われる。

Lean

Lean について話そう。以前、これは依存型言語だと述べたが、この概念は複雑な定義よりも例で説明したほうがわかりやすい。以下はある関数の型だ。ストリームから n バイトを読み取り、例外を投げなければバイト配列を返す。型システムはその長さがちょうど n であることを把握している。

def IO.FS.Stream.readExact (st : Stream) (n : Nat) :
 IO {ba : ByteArray // ba.size = n} := …

次の関数は二つの数と一つのバイト配列を返す。最初の数が素数であること、二つの数の和が 6 で割り切れること、バイト配列の長さが二つの数のうち小さいほう以上であることが要求される。

def getResult :
 IO (Σ a b : Nat, { bytes : ByteArray //
 Nat.Prime a ∧
 6 ∣ a + b ∧
 Nat.min a b ≤ bytes.size }) := …

こんな型が実際に必要になる人はいない。ただ、ここまで自由に遊べるということを示しているだけだ。依存型言語は極めて複雑な数学的構造を符号化するのに十分であり、Lean の現在の主な用途は、数学を記述し証明するための形式言語だ。最近出版された The Proof in the Code は短く、文章も優れていて、Lean の来歴を語っている。著者は構成的数学について数段落にわたって完全に間違ったことを書いているが、それ以外は楽しく読めた！

Lean は Haskell と同じく純粋関数型言語だが、プログラミング言語として使う分には Haskell よりずっと便利になり得る特徴をいくつか備えている。まず、Lean は正格評価で、Haskell は遅延評価だ。正格評価では関数の引数は呼び出しの前に評価されるが、Haskell では引数の評価はその値が本当に必要になるまで先送りされる。おかげで Haskell では、重い式を気軽に書いて関数に渡せる。実際に使われるまで計算されないからだ。だがその代わり、計算がプログラムのかなり予想外の場所で起きることも意味する。賛否のある話題だが、遅延評価のエレガントさは認めるとしても、まったくもって性能の見通しが立ちにくくなる。

次に、Lean には便利な構文糖がかなりある。モナドのdo記法には for ループ、return 文、break 文が揃っている。命令的に書きたいなら、かなり快適に書ける。

最後に、Lean には最適化がある。オブジェクトの参照カウントが 1 であれば、そのオブジェクトを破壊的に更新するのだ。だから、他の場所で参照を握っていないよう注意しさえすれば、命令型言語と同じように効率よく配列をその場で書き換えられる。残念ながら、知る限り Lean に線形型の仕組みはなく、値の参照がひとつだけであることを保証してはくれない。ここは少し厄介な角落ちだ。コードの一見取るに足らない変更が、目立たないどこかで大きな配列の参照を握ったままだという理由で、性能を根こそぎ壊し得る。だが裏を返せば、何かの性能を最適化したいとき、手札はずっと多いということでもある。

以下は、私が書きかけの zstd デコーダからの一例だ。

while true do
 let some blockHeaderBytes ← input.readExactOrEof 3 | break
 let some blockHeader := BlockHeader.fromBytes blockHeaderBytes frameHeader
 | throw (.userError "invalid block header")
 let blockBytes ← input.readExact blockHeader.contentSize

 match hty : blockHeader.type with
 | .rle =>
 let b := blockBytes.val[0]'(by
 rw [blockBytes.property, blockHeader.contentSize_rle hty]; omega)

9 行目を見てほしい。配列のインデックスがあり、インデックスは暗黙の不変条件が潜む大好きな場所だ。blockBytes は空であってはならない。C 系の言語ならここで未定義動作になる。現代的な言語なら実行時に例外を投げるか、そもそもオプショナル値を返してこの問題を回避する。Lean にはもうひとつ選択肢がある。空でないことを証明するのだ。10 行目がそれをやっている。blockBytes.property とは、これが要求された読み取りと同じ長さ、つまりちょうど blockHeader.contentSize バイトであるという事実だ。blockHeader.contentSize_rle はこうなっている。

theorem BlockHeader.contentSize_rle (h : BlockHeader) (hty : h.type = .rle) :
 h.contentSize = 1 := by
 simp [contentSize, hty]

これは、型が rle のとき contentSize が常に 1 であることを証明している。これらの事実があれば、残りは Lean が自分で導いてくれる。

この証明は短く、おそらく私にも書けたはずだが、もっと高い目標を掲げよう。

私は RFC に従って FSE 表構築アルゴリズムを実装した。RFC には「テストベクタ」が付属している。与えられた確率に対する3 つのサンプル出力だ。もちろんこれは単体テストに入る。だが Lean では、この関数の普遍的な性質まで証明できる。

theorem ofDistribution_wellFormed (h : ofDistribution accuracyLog probs = some t) :
    t.entries.size = 2 ^ accuracyLog ∧
    (∀ s : Fin probs.size,
      t.entries.toList.countP (fun e => e.symbol == s.val) = probCells probs[s]) ∧
    (∀ (i : Nat) (hi : i < t.entries.size) (v : Nat), v < 2 ^ (t.entries[i]'hi).nbBits →
      (t.entries[i]'hi).baseline + v < 2 ^ accuracyLog) ∧
    (∀ (s : Fin probs.size), 0 < probCells probs[s] → ∀ x < 2 ^ accuracyLog,
      ∃! i : Nat, ∃ hi : i < t.entries.size,
        (t.entries[i]'hi).symbol = s.val ∧ (t.entries[i]'hi).baseline ≤ x ∧
          x < (t.entries[i]'hi).baseline + 2 ^ (t.entries[i]'hi).nbBits) := …

これを言葉で繰り返す。

表構築関数が与えられた「accuracy」定数とシンボル確率のリストから値を生み出せると仮定すると、

1. 表のサイズはその accuracy と一致する。
2. あるシンボルに対応する状態の数はその確率と一致する。
3. すべての状態について、nbBits ビットを読み、その状態のベースライン値を足した結果は正当な状態番号になる。
4. 確率が非ゼロのすべてのシンボル、およびすべての目標状態について、そのシンボルの下で目標状態に到達できる状態がちょうどひとつ存在する。

これらはまさに、最適化されたデコードの内側ループが依拠している暗黙の前提であり、表現力の乏しい型システムでは暗黙の取り決めかコメントとしてしか存在できないものだ。こうした強い命題を証明することこそ、seL4 の回顧記事が言う 10 倍の作業量の一部であり、依存型が普通のソフトウェアに広く普及しにくい主な障壁でもある。今では数個の LLM がこれを 20 分ほどで自動的にやってのけ、月 20 ドルの購読枠のごく一部しか消費しない。来年にはこれが基本要件になっているだろう。認めねばならないが、その際 LLM は表構築のコードを書き換える必要があった。私が Id.run（つまり命令的モードへの切り替え）を使いすぎていて、証明の仕組みが扱いにくくなっていたのだ。（もっとも Lean はこの点を改善しつつある。）証明が型検査を通り、sorry もないことは確認した。

依存型と LLM を組み合わせるのは新しい発想ではないが、この組み合わせを日常のソフトウェアエンジニアリングに使う仕事はまだ少ない。経験の蓄積が大量に必要だ。非常に強い型は変更の波及範囲を増幅させる。あらゆる派生型に沿って伝播させねばならないからだ。より大きなシステムでは、証明の作業量が耐え難いほど膨らみ、現代の LLM でも追いつかなくなるかもしれない。Lean は高水準言語であり、あらゆる場面に適しているわけではない。（私のおもちゃの Zstandard デコーダはコマンドラインで zstd より 10 倍遅い。）それでも、証明の自動化はすでに到来しており、実質的に使えるプログラミング言語の種類がひとつ増えた。これはわくわくする。

（コードは公開していない。正直に言うと、こういう小さくて明確な問題なら、LLM のほうが自分よりよほど上手くやるだろうから。Lean を少し学ぶためにやっただけで、自分の試行錯誤を手本にするつもりもない。着想は lean-zip から。あちらはもっと本格的で、圧縮器まで含んでおり、往復の一貫性も証明している！）

余談：検証済みアセンブリ

AWS は LNSym を作った。AArch64 の意味論とシミュレータだ。面白い。これを使えば、ある関数の最適化されたアセンブリ実装が Lean 版と等価であることを証明し、実行時にはアセンブリのコードをそのまま使えるのではないか？そうなれば LLM に最適化を任せても、機能上のバグは絶対に混入しない。検証済みアセンブリは暗号実装ではすでに成熟しているが、今ならそれが 安く なるかもしれない？

これには少し時間を費やした（大半は LLM の時間だが）。リポジトリにある小さな popcount の例は bv_decide を使っている。検証可能な SAT ソルバーだが、この例は自分のマシンのメモリ上限を超えてしまい、先が思いやられる。ごく小さな関数なら実際に通り、ごく小さな Lean 関数と等価だという証明が得られ、実行時には extern で呼び出せる！だが、自分も何人かの LLM も、これをより大きな規模に拡張することはできなかった。