LLMガイド付き戦略合成によるスケーラブルな等式飽和（Equality Saturation）

arXiv cs.AI / 2026/4/21

📰 ニュースDeveloper Stack & InfrastructureIdeas & Deep AnalysisModels & Research

共有:

要点

等式飽和（EqSat）を実用化するには、e-graph上での同値なプログラム表現を活かしつつ抽出段階で最小コスト案を選ぶための「戦略（strategy）」が重要だが、従来は多くが手作業で自動化の障壁になっている。
既存のルール合成は書き換え語彙を増やしてしまい、e-graphの爆発（explosion）をさらに悪化させるため、単純な自動化だけでは十分に機能しない。
EggMindはLLMをガイドにしつつ、EqSat戦略を明示・検査可能な成果物として表すドメイン特化DSL「EqSatL」と、証明に由来する書き換えモチーフのキャッシュや探索の実行可能性ガイダンス等の新手法で、高品質な戦略を効率的に合成する。
評価ではベクトル化ベンチマークで最終コストを45.1%削減し、ピークRAMを69.1%削減するなど資源と品質のトレードオフを改善し、XLAベースのテンソルコンパイラや論理合成のケーススタディにも有効であることが示されている。

Abstract

等価性飽和（EqSat）は、e-グラフ内で多くの同値なプログラムをコンパクトに表現し、抽出によって最小コストのプログラムが選択されるまでコミットを遅延させる、強力な最適化パラダイムである。したがってEqSatを有効にするには、ドメイン固有の書き換え規則だけでなく、ドメイン固有の戦略も必要となる。今日において、この戦略設計の多くはまだ手作業であり、e-グラフベースのコンパイラの自動化における大きな障害となっている。最近のルール合成フレームワークは、意味仕様から自動的に大規模な書き換え語彙を推論できるが、同時に書き換え空間を拡大し、さらにe-グラフの爆発を悪化させる。大規模言語モデル（LLM）によって自動戦略合成は現実的になるものの、バックエンドコードを直接進化させることは実運用上効果が低い。探索には再利用可能な戦略の抽象化が欠けており、実行可能なフィードバックも得られない。そのため、簡単にe-グラフの爆発を引き起こしたり、貧弱な設計に収束したりしてしまう。我々は、再利用可能なEqSat戦略を合成するための、LLMに導かれたエンドツーエンドの枠組み「EggMind」を提案する。EggMindの中核では、EqSat戦略を明示的で検査可能な成果物として表すためのドメイン固有言語「EqSatL」を導入する。さらに、証明に由来する書き換えモチーフのキャッシュと、可処理性（tractability）を導く指針といった新しい手法を備えた、LLMガイドのエージェント的ワークフローを提案し、e-グラフの成長下でも合成の安定性を保ちながら、高品質な戦略を効率よく探索する。評価の結果、EggMindはベクトル化ベンチマークにおけるリソースと品質のトレードオフを大幅に改善し、完全なEqSatに比べて最終コストを45.1%削減し、ピークRAMを69.1%削減することを示した。さらに、同じ手法がXLAベースのテンソルコンパイラにも効果的に移植できることを示し、書き換え空間を拡張したロジック合成のケーススタディにおいて、その実用的な可能性を実証する。