Equality saturation (EqSat) is a powerful optimization paradigm that compactly represents many equivalent programs in an e-graph and delays commitment until extraction selects a lowest-cost program. Making EqSat effective, therefore, requires not only domain-specific rewrite rules but also domain-specific strategies. Today, much of this strategy design is still manual, making it a major obstacle to automating e-graph-based compilers. Recent rule-synthesis frameworks can automatically infer large rewrite vocabularies from semantic specifications, but they also enlarge the rewrite space and further exacerbate e-graph explosion. Although large language models (LLMs) make automated strategy synthesis plausible, directly evolving backend code remains ineffective in practice. The search lacks reusable strategy abstractions and actionable feedback, and can easily trigger e-graph explosion or converge to poor designs. We present EggMind, an LLM-guided, end-to-end framework for synthesizing reusable EqSat strategies. At its core, EggMind introduces a domain-specific language, EqSatL, to represent EqSat strategies as explicit and inspectable artifacts. It then proposes an LLM-guided agentic workflow, equipped with novel techniques including proof-derived rewrite motif caching and tractability guidance, to search efficiently for high-quality strategies while keeping synthesis stable under e-graph growth. Evaluation shows that EggMind substantially improves the resource-quality trade-off on vectorization benchmarks, reducing final cost by 45.1% and peak RAM by 69.1% relative to full EqSat. We further show that the same methodology transfers effectively to an XLA-based tensor compiler, and demonstrate its practical potential in a logic-synthesis case study with augmented rewrite spaces.
翻译:相等饱和(EqSat)是一种强大的优化范式,它能在e-graph中紧凑地表示许多等价程序,并延迟决策直到抽取步骤选择出成本最低的程序。因此,要使EqSat有效,不仅需要领域特定的重写规则,还需要领域特定的策略。目前,这类策略设计大多仍依赖人工完成,这成为自动化基于e-graph编译器的主要障碍。尽管近期提出的规则综合框架能根据语义规范自动推断大量重写词汇,但这也扩大了重写空间,进一步加剧了e-graph爆炸问题。虽然大语言模型(LLM)使得自动化策略综合成为可能,但在实践中直接演进后端代码仍效果不佳。该类搜索缺乏可复用的策略抽象和可操作的反馈,容易引发e-graph爆炸或收敛到低质量设计。我们提出EggMind——一个由LLM引导的、用于综合可复用EqSat策略的端到端框架。其核心创新在于引入领域特定语言EqSatL,将EqSat策略表示为显式且可检查的构件。在此基础上,我们提出一种LLM引导的智能体工作流,该工作流配备了包括源自证明的重写模式缓存和可处理性引导在内的多项新技术,能在保持综合过程在e-graph增长下稳定性的同时,高效搜索高质量策略。评估显示,EggMind在向量化基准测试上显著改善了资源-质量权衡——相较于完整EqSat,最终成本降低45.1%,峰值内存占用减少69.1%。我们进一步证明,该方法能有效迁移至基于XLA的张量编译器,并通过在增强重写空间下进行逻辑综合案例研究,展示了其实际应用潜力。