こんにちは、チェシャ猫です。
先日開催された BuriKaigi 2026 で、定理証明支援系 Lean を用いたコンパイラの証明について登壇してきました。公募 CFP 枠です。
講演概要
近年、生成 AI を利用したシステム開発はもはや特殊な選択肢ではなく、一般のプログラマでも十分に活用しうる水準の技術となりました。一方、生成 AI が高速かつ大量に、しかしハルシネーションを含んだ出力を行うことにより、その正しさを改めて確認する側の人間の負担感も様々な場所で聞かれ、AI Slop などと呼ばれています。ちなみに Slop とは「泥水」のことで、低品質な出力を例えた表現です。
今回の講演では、このような状況に対して「検証可能な仕様記述」が重要になるのではないか、という洞察を出発点とします。すなわち、記述として曖昧性を持たず、実装がその仕様を満足しているかどうかが明確かつ機械的に判定できるような仕様です。
広くシステム開発で用いられる通常の単体テストでは、バグの検出力はテスト設計に強く依存します。単体テストによる仕様の検査は、個別のテストケースに対する主張しか持ちません。例えば「入力が空リストの場合」「入力が長さ 1 のリスト [42] の場合」といった主張です。テストが失敗すればそのテストケースが仕様を満たさないことはわかります。しかし逆に全てのテストケースが成功したとしても、たまたま不具合を含むケースを含まなかったのではないか、という疑いが残ります。まさにかつて Dijkstra が述べた通り「テストはバグが存在することを示すためには使えるが、存在しないことは示すためには使えない」のです[Dij70]。
これに対してプロパティベーステストや定理証明では、「任意のリストに対して」という全称命題を検査することができます。このうち、プロパティベーステストが実際に保証するのはあくまでも多数のランダムなテストケースに対する主張であり、テストケースの体系的な生成によりカバレッジを確保します。しかし定理証明では、主張したい命題を型として表現し型検査を行うことで、「任意の型の値を要素とする、任意のリストに対して」という真に全称的な主張を検査できます。このような強い主張が可能な仕様記述・検査手法である定理証明、特にツールとしての Lean を用いたコンパイラの正当性証明が講演のテーマです。
ここで強調しておきたいこととして、今回証明するのは「個別のプログラムのコンパイル結果が正しく動くこと」ではありません。コンパイルのアルゴリズムそれ自体の正当性を示すため、「どんなプログラムであっても、そのコンパイル結果が正しく動くこと」を示す必要があります。タイトルにも含めた通り、この「正しく動く」という主張をどのようにして表現するかが鍵であり、今回は弱模倣の概念を用いて定式化を行います。
今回 Lean で実装したコンパイラとその証明には元ネタがあります。コンパイラの定理証明として非常に有名な仕事として、証明付きの C コンパイラである CompCert が知られています[Ler06]。またプロジェクトのリードである Leroy が担当した EUTypes サマースクール 2019 において、CompCert の証明の骨子を残して単純化したものが教材として使用されています[Ler19]。この CompCert やサマースクールは Coq を使用しています。そこで証明を Lean で書き直し、さらに追加でパーサやエントリポイントも含めて実装して実際にコンパイラとして動かしてみよう、というのが今回の発表の趣旨になります
質問への回答
当日の持ち時間には質疑応答は含まれなかったのですが、講演後の Ask the Speaker、および X（旧 Twitter）のハッシュタグ検索で見つけた質問への回答をまとめておきます。
数学的証明として成り立ってるのでテストが不要って話なのかな…？わかってない気がする…#burikaigi_b #burikaigi
— まじまっちょ (@majimaccho_) 2026年1月10日
「テストが不要」というよりは、「テストより強い内容が保証が得られる」という方が適切だと思います。
今回の講演では明示的に説明しませんでしたが、Lean による証明内容のチェックは、通常のプログラミング言語における型検査に相当するものです。特定の論理体系において「型と、その型を持つ項」および「命題と、その命題の証明」は完全に読み替えが可能であることが知られており、この関係は Curry-Howard 対応として知られています。Lean では証明したい命題に対応する証明項を構築することによって証明を行いますが、これは Curry-Howard 対応により、欲しい型の値を構築することと同じことです。記述された証明が正しくない場合、型エラーによりコンパイル時点で弾かれます。
聞いた範囲ではこれで無限ループ扱えるのに対して納得してないので手動かして追ってみないとわからんなあ #burikaigi #burikaigi_b
— sylph01 / G4きゅーぶ (@s01) 2026年1月10日
ご本人と懇親会でお話ししたのですが、これは非常に良い質問です。実際、今回述べた形の弱模倣の定義には、模倣されるべき遷移 s -> ... -> s' に「途中でちょうど一回、観察可能な出力を行う」という条件が入っているため、模倣される側が τ 遷移（出力を伴わないような遷移）を無限に繰り返す状況をうまく扱うことができません。一方、後のスライドに乗せた Lean の記述は以下のようになっています。
theorem simulation_step : ∀ (code : Code) (l : Label) (ist1 ist2 : ItpState) (vst1 : VMState), itpStep ist1 l ist2 → match_state code ist1 vst1 → ∃ (vst2 : VMState), vmWeakStep code l vst1 vst2 ∧ match_state code ist2 vst2
この l : Label は観察可能な出力と観察不可能な τ 遷移との両方を含むため、主張としては弱模倣の定義として述べられているスライドより真に強いものです。結論として、インタプリタが τ 遷移のみのループを持っていても、やはり VM はその動作を追従することができます。ちなみにこの「τ 遷移のみのループ」は、通常の言葉でいえば要するにライブロックに相当するものです。
講演中で「インタプリタ」と読んでいたものは、いわゆる「インタプリタ言語」といったときの「インタプリタ」と同じものですか？
基本的にはその通りです。現実のプログラミング言語のインタプリタは内部に JIT が入っていたりして話がややこしいですが、最もナイーブな、構文木を直接簡約するタイプのインタプリタ処理系を想像してもらえばそれで合っています。
ただし、Lean とはちょっと別の話として、「インタプリタ言語」「コンパイル言語」という分類は意味を持たないことに注意すべきです。現実のモダンなインタプリタが両方の性質を併せ持つから、という理由ではなく、処理系がインタプリタであるかどうかは「言語の性質」ではないからです。
少なくとも自分の捉え方では、という前置きの下ですが、プログラミング言語は構文と意味論から成ります。前者はどのような文字列がプログラムとしてみなされるかを規定し、後者は実行したときに何が起こるかを規定します。操作的意味論による意味論の定義はほぼインタプリタの実装とイコールになりがちではありますが、その「何が起こるか」を実現する方法は、実際にインタプリタ処理系である必要はありません。
その意味では、操作的意味論がインタプリタの簡約規則として定義されたときに、コンパイルして VM で動かす第二の処理系の動作が「操作的意味論の見本」たるインタプリタ処理系と一致することこそ、今回述べたかった「コンパイラの正しさ」であるもいえます。
インタプリタを実装することと、操作的意味論を Lean で書き下すこととの間にはどの程度のギャップがあるのか？
ほぼないです。
無論、実務的なインタプリタにはパフォーマンスを考えた最適化が入っているのが普通なので、いわゆる操作的意味論とはイコールにはなりません。ただ、そういう話を除いて少なくとも今回例にしたようなトイ言語であれば、ほぼ迷わず機械的に翻訳できると言い切ってしまって良いレベルだと思います。インタプリタを実装できる人間であれば、簡約規則を Lean の Prop 型を用いて関係の形で書いたものも理解できるはずです。
例えば、以下がインタプリタのステップ実行の関数です。
def stepExec (st : ItpState) : Option (Label × ItpState) := match st with | (.assign x a, k, s) => .some (.tau, (.skip, k, update x (aEval s a) s)) | (.seq c1 c2, k, s) => .some (.tau, (c1, .kSeq c2 k, s)) | (.ifThenElse b c1 c2, k, s) => .some (.tau, if bEval s b then c1 else c2, k, s) | (.while_ b c, k, s) => if bEval s b then .some (.tau, (c, .kWhile b c k, s)) else .some (.tau, (.skip, k, s)) | (.skip, .kSeq c k, s) => .some (.tau, (c, k, s)) | (.skip, .kWhile b c k, s) => .some (.tau, (.while_ b c, k, s)) | (.print a, k, s) => .some (.out (aEval s a), (.skip, k, s)) | (.skip, .kStop, _) => .none
そして以下が簡約規則を関係の形で記述したものです。証明の際には、部分関数の扱いの煩雑さを避けるため、こちらの形の方がよく使われます。
inductive itpStep : ItpState → Label → ItpState → Prop where | itpStep_assign : ∀ (x : Ident) (a : AExp) (k : Cont) (s : Store), itpStep (.assign x a, k, s) .tau (.skip, k, update x (aEval s a) s) | itpStep_seq : ∀ (c1 c2 : Com) (s : Store) (k : Cont), itpStep (.seq c1 c2, k, s) .tau (c1, .kSeq c2 k, s) | itpStep_ifThenElse : ∀ (b : BExp) (c1 c2 : Com) (k : Cont) (s : Store), itpStep (.ifThenElse b c1 c2, k, s) .tau (if bEval s b then c1 else c2, k, s) | itpStep_while_done : ∀ (b : BExp) (c : Com) (k : Cont) (s : Store), bEval s b = false → itpStep (.while_ b c, k, s) .tau (.skip, k, s) | itpStep_while_true : ∀ (b : BExp) (c : Com) (k : Cont) (s : Store), bEval s b = true → itpStep (.while_ b c, k, s) .tau (c, .kWhile b c k, s) | itpStep_skip_seq : ∀ (c : Com) (k : Cont) (s : Store), itpStep (.skip, .kSeq c k, s) .tau (c, k, s) | itpStep_skip_while : ∀ (b : BExp) (c : Com) (k : Cont) (s : Store), itpStep (.skip, .kWhile b c k, s) .tau (.while_ b c, k, s) | itpStep_print : ∀ (a : AExp) (k : Cont) (s : Store), itpStep (.print a, k, s) (.out (aEval s a)) (.skip, k, s)
両者はほぼ同じ形をしているのがわかると思います。なお、実装の正しさを主張するためには、この両者が一致することも証明すべきであり、実際に証明が可能です。
まとめ
以上、簡単ではありますが、BuriKaigi 2026 での登壇を備忘録としてまとめました。
内容としては、Coq による EUTypes 2019 サマースクールで述べられたコンパイラの証明技法を出典として、Lean で置き換えたものを実装・解説しました。特に、出典となった資料にはない展開として、Lean の特性を活かして実際に動作可能なコンパイラを実装し、簡単なプログラムのコンパイルと実行の例を追加しています。
ところで、このサマースクールの資料はこの後も続き、コンパイル時の定数伝搬やデッドコード削除についても扱われています。こちらについても引き続き Lean で実装したいところですが、それはまた別の話。
参考リンク
- [Dij70] Edsger W. Dijkstra. 1970. “Notes on Structured Programming.” EUT Report 70-WSK-03 (EWD 249), Technische Hogeschool Eindhoven. Accessed 2026-01-15.
- [Ler06] Xavier Leroy. 2006. “Formal certification of a compiler back-end, or: programming a compiler with a proof assistant.” POPL 2006, pp. 42–54.
- [Ler19] Xavier Leroy. 2019. “Proving the correctness of a compiler.” EUTypes 2019. Accessed 2026-01-15.
