Lean定理証明器における等価飽和タクティクの革新とスロット付きe-グラフの理論的展開
インタラクティブ定理証明における自動化の歴史的転換点
計算機科学と数学の交差点において、インタラクティブ定理証明器（ITP）は、数学的言明の厳密な検証を可能にする究極のツールとして君臨してきた。Lean、Coq、Isabelle/HOLといったシステムは、表現力の高い依存型理論や高階述語論理を基盤とし、ソフトウェアの正当性証明や複雑な数学的定理の定式化において目覚ましい成果を上げている。しかし、これらのツールを用いる際の最大の障壁は、証明構築における手動操作の膨大さと、それに伴う専門的知識の要求である。特に等式的推理（Equational
Reasoning）は、人間にとっては自明な書き換えの連続であっても、形式的な証明においては冗長で退屈なステップを無数に要求することが少なくない^1
この課題に対し、自動定理証明（ATP）の技術をITPに統合する試みが長年続けられてきた。その中で、近年特に注目を集めているのが「等価飽和（Equality
Saturation）」という手法である。等価飽和は、与えられた項の集合に対して書き換え規則を非破壊的に適用し続け、到達可能なすべての等価な項を効率的に表現する「e-グラフ（Equivalence
Graph）」を構築する技術である^2^。この手法は、従来の破壊的な書き換えが直面していた「フェーズ順序問題（どの規則をどの順番で適用すべきかという問題）」を、可能なすべての書き換えを同時に保持することで解決する^2
ドレスデン工科大学（TU Dresden）のコンパイラ構築講座（Chair of Compiler
Construction）におけるMarcus Rosselの研究は、この等価飽和技術をLean
4という現代的な定理証明プラットフォームに統合することに焦点を当てている。Rosselの修士論文「An
Equality Saturation Tactic for
Lean」は、Rust言語で実装された高性能な等価飽和ライブラリであるeggをLeanのタクティクとして組み込み、数学者や計算機科学者が複雑な等式的証明を自動化するための道を切り拓いた^2^。本報告書では、Rosselの修士論文およびそれに関連する「スロット付きe-グラフ（Slotted
E-Graphs）」の革新的な研究、そしてそれらが大規模な数学プロジェクトである「Equational
Theories Project (ETP)」においてどのように結実したかを詳細に分析する。
等価飽和の理論的基盤とeggライブラリの役割
等価飽和の核心にあるのは、e-グラフというデータ構造である。e-グラフは、等価クラス（e-class）とe-ノード（e-node）の2つの構成要素から成る。各e-クラスは等価な項の集合を表し、e-ノードは演算子とその引数（引数はe-クラスへのポインタ）を表す。この構造により、指数関数的な数の等価な項を、高度な共有（Sharing）を通じてコンパクトに表現することが可能となる^2
等価飽和のプロセスは、以下のステップで進行する。まず、初期の項をe-グラフに挿入する。次に、定義された書き換え規則の集合を繰り返し適用する。この際、規則の適用によって新たな項が生成されるが、それは既存のe-グラフにマージされるだけで、以前の項が消去されることはない。このプロセスをグラフが「飽和」する（新しい等価性が発見されなくなる）か、計算資源の限界に達するまで継続する。最後に、目標とする項が同じe-classに含まれているかを確認し、含まれていれば、その間の書き換えパスを抽出して証明を構成する^2
Marcus Rosselが採用したeggライブラリは、Max
Willseyらによって開発された最新の等価飽和フレームワークであり、e-class解析や動的書き換えといった柔軟な拡張機能を備えている^2^。Rosselの貢献は、この汎用的な最適化エンジンを、Lean
4の厳密な型理論的枠組みの中に、健全性（Soundness）を保ったまま統合した点にある^6
Lean 4における表現言語と実装上の障壁
Lean 4の内部表現は、依存型$\lambda$計算である「構築の計算（Calculus
of
Constructions）」に基づいている。この言語において、データ型、値、命題、証明はすべて同一の項として扱われる^5
{width=“6.458333333333333in”
height=“0.5555555555555556in”}
ここで、
{width=“6.458333333333333in”
height=“0.15809820647419073in”}は抽象、
{width=“0.11214129483814524in”
height=“0.2344783464566929in”}は依存型積（Pi型）を表す^5
第一の課題は、Leanの「定義上の等価性（Definitional Equality,
{width=“0.15690069991251093in”
height=“0.24058180227471565in”}）」である。Leanにおいて、2つの項は、
{width=“0.11360673665791776in”
height=“0.2272123797025372in”}変換、
{width=“0.12475612423447069in”
height=“0.24951224846894138in”}簡約、
{width=“0.10742235345581802in”
height=“0.2578127734033246in”}変換といった簡約操作を通じて同一視される。しかし、標準的なe-グラフは構文的な同一性のみを前提とするため、例えば$(\lambda
x, x + 0) 1
{width=“0.20174212598425198in”
height=“0.2442136920384952in”}1$が等しいことを、書き換え規則なしには認識できない^5
第二の課題は、束縛変数の扱いである。ITPでは名前衝突を避けるためにデ・ブラウン・インデックスが多用されるが、項がバインダーを越えて移動するたびにインデックスをシフトさせる必要があり、これがe-グラフ内での共有を破壊し、グラフの爆発的な増大を招く^3
Rosselの修士論文は、これらの課題に対し、Leanの項をeggが理解できる構文に「低級化（Lowering）」し、飽和後に得られた「説明（Explanation）」をLeanの証明項へと「再構築（Reconstruction）」するパイプラインを構築することで対応した^2^。特筆すべきは、egg内での処理が一部不完全（Unsound）であったとしても、最終的な証明はLeanのカーネルによって検証されるため、システム全体の健全性は保証されるという設計思想である^6
eggタクティクの設計とメタプログラミングの統合
Marcus Rosselによって実装されたeggタクティクは、Lean
4の強力なメタプログラミング機能を活用して、ユーザーが自然な形式で自動証明を利用できるように設計されている。このタクティクは、現在の証明目標（Goal）と、ユーザーが指定した（あるいはライブラリから自動収集された）等式定理を受け取り、バックエンドのRustプロセスと通信して最短の書き換え経路を探索する^1
コンポーネント 役割 技術的特徴
フロントエンド ユーザーインターフェース Lean 4タクティク構文によるシームレスな統合 ^4^
コンバータ Lean項からegg構文への変換 デ・ブラウン・インデックスの処理と型情報の付与 ^5^
等価飽和エンジン 探索と最適化 Rust製eggライブラリによる高速なe-グラフ構築 ^2^
証明再構築器 証拠の生成 eggの説明機能を用いたLeanの書き換え証明（calc等）の生成
^4^
Rosselは修士論文のタスクとして、以下の機能を実装した。
-
eggライブラリおよびe-グラフに基づく等価飽和の深い理解と適用^2
-
Leanの表現言語およびメタプログラミング機能の統合^2
-
eggをLeanの証明タクティクとして統合し、自動等式証明を実現^2
-
テストスイートを用いたタクティクの有効性評価^2
-
（オプション項目）Aesop（自動証明探索フレームワーク）との統合および条件付き書き換え機能の拡張^2
特に「条件付き書き換え」は、特定の前提条件（例：除算における分母が非ゼロであること）が満たされる場合にのみ適用される規則を扱うものであり、実用的な定理証明において不可欠な要素である^2
変数表現の革新：スロット付きe-グラフ（Slotted E-Graphs）
Rosselの修士論文から派生した最も重要な学術的成果の一つが、PLDI
2025で発表された「スロット付きe-グラフ（Slotted
E-Graphs）」である。この研究は、Rosselに加え、Rudi Schneider、Andrés
Goens、Michel
Steuwerといったドレスデン工科大学およびバークハウゼン研究所（Barkhausen
Institute）の研究者らによる共同作業の結果である^3
従来のe-グラフにおいて、束縛変数は「永遠の難問」とされてきた。デ・ブラウン・インデックスを用いる場合、同じ意味を持つ部分項であっても、異なるバインダー深度に存在するとインデックス値が異なるため、別のe-classとして扱われてしまう。これにより共有が阻害され、メモリ消費が激増する。一方、名前をそのまま用いる手法は、名前の衝突（Variable
Capture）を避けるための複雑な管理を必要とする^3
スロット付きe-グラフは、変数をデータ構造の第一級オブジェクトとして扱うことで、この問題を根本から解決する。具体的には、e-classを「スロット（Slot）」でパラメータ化し、自由変数を抽象化する^3^。e-ノードがe-classを参照する際、現在の文脈における変数をターゲットe-classのスロットにマッピングするメタデータを付与する。これにより、名前が異なるだけの項（{width=“0.11360673665791776in”
height=“0.2272123797025372in”}等価な項）を同一のe-classで一意に表現することが可能となった^3
特徴 従来のe-グラフ（デ・ブラウン式） スロット付きe-グラフ
共有の度合い 低い（インデックスが異なれば別扱） 高い（{width=“0.11360673665791776in”
height=“0.2272123797025372in”}等価な項を統合） ^3^
書き換え規則 シフト処理のための複雑な規則が必要 簡潔な記述が可能 ^3^
メモリ効率 インデックスの重複により悪化しやすい 冗長な複製を排除 ^3^
実装の容易さ 解析処理（e-class analysis）が必須 ビルトインの置換機能で簡略化 ^3^
この技術革新により、Leanのような複雑な束縛構造を持つ言語における等価飽和のパフォーマンスは劇的に向上した。評価実験では、従来のデ・ブラウン方式では解けなかった複雑な定理証明の課題が、スロット付きe-グラフを用いることで実用的な時間内に解決可能であることが示されている^3
eggタクティクの定量的評価と性能分析
Marcus
Rosselは、開発したeggタクティクの性能を、Leanの標準ライブラリ（Mathlib等）から抽出した多数のテストケースを用いて厳密に評価した。評価の焦点は、成功率、実行時間、および既存のタクティク（simp等）との比較に置かれた^2
ライブラリテストの結果
評価結果によれば、eggタクティクは多くの標準的な等式的証明において極めて高い効率を示した。特に、成功したケースの99.7%が1秒以内に完了しているというデータは、インタラクティブな証明環境における実用性を裏付けている^2
指標 統計値
成功したテストの実行時間（1秒未満） 99.7% ^2^
平均証明ステップ数（説明の長さ） 4.3ステップ ^2^
最大証明ステップ数（ライブラリ内） 35ステップ ^2^
証明再構築の平均時間 81ms ^2^
一方で、詳細な時間配分の分析により、現在の実装におけるボトルネックも明らかになった。
フェーズ 時間占有率 内容
前処理（Preprocessing） 60.7% Lean項の精査、型推論、変換 ^2^
等価飽和（egg処理） 12.6% Rustによるe-グラフ構築と探索
^2^
証明再構築（Reconstruction） 26.7% 説明からLean証明項への変換 ^2^
このデータは、計算の主体である等価飽和そのものよりも、Leanとのインターフェース部分（特に項の精査やメタデータの処理）に多くの時間が費やされていることを示唆している。これは、ITPの自動化において、外部ツールとの通信オーバーヘッドやホスト言語の型システムの複雑さが、純粋なアルゴリズムの効率以上に重要であることを物語っている^2
複雑な等式への対応能力
Rosselの評価では、単一の等式だけでなく、複数の定理を組み合わせた複雑な推論能力もテストされた。
-
1つの等式を使用：テストの36.3% ^2^
-
2つの等式を使用：テストの25.8% ^2^
-
3つの等式を使用：テストの21.7% ^2^
-
10個以上の等式を使用：テストの1.5%未満 ^2^
多くの実用的な証明は数ステップの書き換えで解決するが、少数の極めて複雑な問題に対しても、eggは人間が手動で書き換え規則を探索する負担を大幅に軽減している^2
大規模数学プロジェクトへの応用：Equational Theories Project (ETP)
Marcus
Rosselの研究成果が最も劇的な形で結実したのが、2024年9月に開始された「Equational
Theories Project
(ETP)」である。このプロジェクトは、フィールズ賞受賞者のTerence
Taoらが主導し、普遍代数学における数千の等式的法則の間の含意関係を完全に解明することを目的に、世界中の数学者が協力したオンライン共同プロジェクトである^13
ETPの目標は、マグマ（単一の二項演算を持つ代数系）における最も単純な4,694個の等式的法則について、それぞれの間の含意関係をすべて特定することであった。これは、約2,200万（
{width=“1.2327504374453193in”
height=“0.24028215223097113in”}）通りの組み合わせを検証することを意味する^13
プロジェクト統計 詳細
対象となる法則数 4,694 ^13^
検証すべき含意の総数 22,028,942 ^13^
主要な使用ツール Lean 4, egg, 各種自動証明器 ^15^
完了日 2025年4月14日 ^13^
この膨大な作業を人間だけで行うことは不可能であり、Marcus
Rosselらが開発したeggタクティクを含む自動証明技術が決定的な役割を果たした。eggは、ある法則から別の法則が導かれる（あるいは導かれない）ことを高速に探索し、その証拠をLeanが検証可能な形式で出力した^8^。このプロジェクトにより、新しいマグマの構造が多数発見されたほか、有限マグマに限定した場合の影響など、多くの付随的な問いにも回答が与えられた^8^。ETPは、最新のITP自動化技術が、最先端の数学研究において「力仕事」を肩代わりし、数学者がより本質的な考察に集中できる環境を提供できることを実証した^1
バークハウゼン研究所とVerSAプロジェクトの文脈
Marcus
Rosselの研究は、単なるアカデミックな成果に留まらず、産業界における高信頼システムの開発という広範なビジョンの一部となっている。Rosselは修士課程修了後、バークハウゼン研究所の「検証済みシステム設計自動化（Verified
System Design Automation,
VerSA）」グループにおいて、ポストドクター研究員として活動している^1
VerSAグループは、高価な実機テストを数学的な論理推論に置き換えることを目指している。具体的には、CoqやLeanといった定理証明器を用いて、設計段階でシステムの機能的正当性やセキュリティを数学的に証明する「開発・検証共同設計（Development-Verification
Co-Design）」を提唱している^10
このグループにおける関連研究として、Max
Kurzeによる「Kôikaにおけるモジュール式・組成的な形式推論フレームワーク」が挙げられる。Kurzeの修士論文は、ハードウェア記述言語Kôikaのセマンティクスを拡張し、Hoare論理に基づく推論を可能にするもので、Rosselの論文と同様にドレスデン工科大学のコンパイラ構築講座の指導の下で行われ、高い評価（3m5
thesis award）を受けた^1
RosselとKurzeの研究は、ソフトウェア（Lean/等価飽和）とハードウェア（Kôika/検証）の両面から、信頼性の高いコンピューティング・スタックを構築するという共通の目標を支えている。Rosselが開発した等価飽和タクティクは、システムの仕様と実装の間の等価性を証明するための強力なエンジンとして、将来的に大規模なシステム検証プロジェクトに組み込まれることが期待されている^17
賞賛と学術的評価：N.-J. Lehmann-Stiftung賞
Marcus Rosselの修士論文「An Equality Saturation Tactic for
Lean」は、その理論的深度と実用的な貢献が認められ、N.-J.
Lehmann-Stiftung賞を受賞した。この賞は、計算機科学における「理論に焦点を当てた卓越した論文」に対して授与されるものである^1
受賞理由として、以下の点が挙げられている。
-
数学者や計算機科学者が等式をはるかに効率的に推論できるタクティクの構築^1
-
退屈で困難な作業を自動化し、ユーザーが証明の核心部分に集中できるようにした点^1
-
型理論、等価飽和、Leanのメタプログラミングという、高度に専門的な領域を統合した技術的能力^10
-
定理証明における変数表現という長年の課題に対する、スロット付きe-グラフという革新的なアプローチへの貢献^3
また、Rosselはこの研究成果を、プログラミング言語設計と実装の最高峰であるPLDI（Programming
Language Design and
Implementation）のワークショップであるEGRAPHSにおいて発表し、世界の研究コミュニティから高い評価を受けた^7
等価飽和と定理証明の融合：次なるフロンティア
Rosselの研究は、ITPの自動化における一つの到達点を示すと同時に、さらなる研究の方向性を提示している。今後の展望として、いくつかの重要な領域が挙げられる。
Aesopとの統合
Rosselの修士論文でも言及されているように、eggタクティクをAesop（Automated
Extensible Search Over
Proofs）のような他の自動証明フレームワークと統合することは、非常に有望な展開である^2^。Aesopはルールベースの探索（Rule-based
Search）に優れているが、等価飽和のような全域的な等価性探索の機能は持っていない。これらを組み合わせることで、論理的な推論と代数的な計算を同時に自動化する、より強力なタクティクが実現可能となる。
高階等価飽和と依存型への完全対応
現在のeggタクティクは、Leanの表現言語の大部分をサポートしているが、依存型が絡む複雑な等価性（例：型の等価性が項の等価性に依存する場合）の完全な自動化には、さらなる理論的拡張が必要である。スロット付きe-グラフは束縛変数の問題を解決したが、高階関数や複雑な再帰構造を含む項の効率的な表現と探索は、依然として活発な研究分野である^3
産業界への実装：自動コンパイラ検証
バークハウゼン研究所でのVerSAプロジェクトの文脈において、eggタクティクは「正しいコンパイラ」の自動構築に貢献する可能性がある。コンパイラの最適化パスは本質的に項の書き換えであり、その正当性（最適化前後で意味が変わらないこと）を等価飽和を用いて自動的に証明できれば、信頼性の高いソフトウェア開発プロセスが劇的に加速される^17
総括と結論
Marcus
Rosselによる「Leanのための等価飽和タクティク」の開発は、定理証明の自動化における重大なパラダイムシフトを象徴している。等価飽和という、元々はコンパイラ最適化のために洗練された技術を、形式的手法の厳格な世界に持ち込むことにより、人間による手動証明の負担を劇的に軽減し、Equational
Theories Projectのような大規模な数学的成果を支えることに成功した。
本報告書で詳述した通り、Rosselの研究は以下の三層の貢献から成る。
第一に、ツールとしての貢献である。eggをLean
4に統合し、実用的なパフォーマンスを持つタクティクを開発したことで、Leanユーザーコミュニティ全体がその恩恵を受けられるようになった^1^。
第二に、理論としての貢献である。スロット付きe-グラフという新しいデータ構造の考案に寄与したことで、e-グラフにおける束縛変数の扱いという計算機科学の長年の懸案事項に、一石を投じた^3^。
第三に、実証としての貢献である。ETPという前例のない規模の数学共同研究において、自動化が研究のスピードと範囲をいかに拡大できるかを示した^13
ドレスデン工科大学とバークハウゼン研究所の強力な研究ネットワークの下で育まれたこの成果は、今後の定理証明技術の標準を定義するものとなり得る。形式的検証が「専門家のための特殊なツール」から「すべての設計者と数学者のための標準的なインフラ」へと進化する過程において、Rosselが開発した自動化のエンジンは、その中心的な役割を果たし続けるであろう^10
引用文献
-
Marcus Rossel and Max Kurze receive thesis awards! - cfaed, 2月 4,
2026にアクセス、
[https://cfaed.tu-dresden.de/ccc-news/news_reader/marcus-rossel-and-max-kurze-receive-thesis-awards]{.underline} -
An Equality Saturation Tactic for Lean - cfaed, 2月 4,
2026にアクセス、
[https://cfaed.tu-dresden.de/files/Images/people/chair-cc/theses/2407_Rossel_MA.pdf]{.underline} -
Slotted E-Graphs: First-Class Support for (Bound … - Michel
Steuwer, 2月 4, 2026にアクセス、
[https://steuwer.info/files/publications/2025/PLDI-Slotted-E-Graphs.pdf]{.underline} -
marcusrossel/lean-egg: A (WIP) equality saturation tactic for … -
GitHub, 2月 4, 2026にアクセス、
[https://github.com/marcusrossel/lean-egg]{.underline} -
Bridging Syntax and Semantics of Lean Expressions in E-Graphs -
arXiv, 2月 4, 2026にアクセス、
[https://arxiv.org/pdf/2405.10188]{.underline} -
Bridging Syntax and Semantics of Lean Expressions in E-Graphs -
arXiv, 2月 4, 2026にアクセス、
[https://arxiv.org/html/2405.10188v1]{.underline} -
Bridging Syntax and Semantics of Lean Expressions in E-Graphs
(EGRAPHS 2024), 2月 4, 2026にアクセス、
[https://pldi24.sigplan.org/details/egraphs-2024-papers/11/Bridging-Syntax-and-Semantics-of-Lean-Expressions-in-E-Graphs]{.underline} -
Marcus Rossel’s research works | Barkhausen Institut and other
places - ResearchGate, 2月 4, 2026にアクセス、
[https://www.researchgate.net/scientific-contributions/Marcus-Rossel-2281856270]{.underline} -
[2405.10188] Bridging Syntax and Semantics of Lean Expressions in
E-Graphs - arXiv, 2月 4, 2026にアクセス、
[https://arxiv.org/abs/2405.10188]{.underline} -
Two BI Researchers Receive Awards for Outstanding Theses -
Barkhausen Institut, 2月 4, 2026にアクセス、
[https://www.barkhauseninstitut.org/en/two-bi-researchers-receive-awards-for-outstanding-theses]{.underline} -
Marcus Rossel - Google Scholar, 2月 4, 2026にアクセス、
[https://scholar.google.com/citations?user=qMvUOe4AAAAJ&hl=en]{.underline} -
Michel Steuwer, 2月 4, 2026にアクセス、
[https://steuwer.info/]{.underline} -
The Equational Theories Project: Advancing Collaborative
Mathematical Research at Scale - UVaDOC Principal, 2月 4,
2026にアクセス、
[https://uvadoc.uva.es/bitstream/handle/10324/80484/The%20equational%20theories%20project.%20Advancing%20collaborative%20mathematical%20research%20at%20scale%20%28arXiv%2C%202025%29%20-%20Tao%20et%20al.pdf?sequence=1&isAllowed=y]{.underline} -
The Equational Theories Project: Advancing Collaborative
Mathematical Research at Scale, 2月 4, 2026にアクセス、
[https://arxiv.org/html/2512.07087v1]{.underline} -
The Equational Theories Project: Advancing Collaborative
Mathematical Research at Scale, 2月 4, 2026にアクセス、
[https://arxiv.org/html/2512.07087v2]{.underline} -
News - cfaed, 2月 4, 2026にアクセス、
[https://cfaed.tu-dresden.de/ccc-news]{.underline} -
Verified System Design Automation - Barkhausen Institut, 2月 4,
2026にアクセス、
[https://www.barkhauseninstitut.org/en/research/research-groups/verified-system-design-automation]{.underline} -
Publications - cfaed - TU Dresden, 2月 4, 2026にアクセス、
[https://cfaed.tu-dresden.de/publications]{.underline} -
Marcus Rossel at EGRAPHS@PLDI - cfaed, 2月 4, 2026にアクセス、
[https://cfaed.tu-dresden.de/ccc-news/news_reader/marcus-rossel-at-egraphs-pldi]{.underline} -
Andrés GOENS | Professor (Assistant) | Doctor of Philosophy |
Technical University of Darmstadt, Darmstadt | TU | Research
profile - ResearchGate, 2月 4, 2026にアクセス、
[https://www.researchgate.net/profile/Andres-Goens-2]{.underline}