pith. machine review for the scientific record. sign in

arxiv: 2604.17364 · v1 · submitted 2026-04-19 · 💻 cs.AI · cs.MA· cs.PL

Recognition: unknown

LLM-Guided Strategy Synthesis for Scalable Equality Saturation

Authors on Pith no claims yet

Pith reviewed 2026-05-10 06:15 UTC · model grok-4.3

classification 💻 cs.AI cs.MAcs.PL
keywords equality saturationstrategy synthesislarge language modelse-graphscompiler optimizationvectorizationtensor compilers
0
0 comments X

The pith

An LLM-guided framework synthesizes reusable strategies for equality saturation that improve program quality while using far less memory.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents EggMind, which lets large language models automatically discover compact strategies that guide equality saturation without applying every rewrite rule at once. It defines a domain-specific language called EqSatL so strategies become explicit and reusable objects rather than hidden backend code. The search is kept stable by caching common rewrite patterns taken from proofs and by giving the model ongoing signals about whether the underlying e-graph is staying tractable. On vectorization benchmarks the resulting strategies produce lower-cost outputs with 45.1 percent lower final cost and 69.1 percent lower peak memory than full equality saturation. The same workflow also transfers to an XLA-based tensor compiler and shows promise in logic-synthesis settings with enlarged rule sets.

Core claim

EggMind introduces the EqSatL domain-specific language to represent EqSat strategies as explicit and inspectable artifacts, then uses an LLM-guided agentic workflow equipped with proof-derived rewrite motif caching and tractability guidance to search efficiently for high-quality strategies while keeping synthesis stable under e-graph growth.

What carries the argument

EqSatL, a domain-specific language for writing EqSat strategies as inspectable artifacts, searched by an LLM agent that caches proof-derived rewrite motifs and receives tractability feedback to control e-graph growth.

If this is right

  • The synthesized strategies are reusable across multiple inputs within the same optimization domain.
  • The approach delivers 45.1 percent lower final program cost and 69.1 percent lower peak RAM usage on vectorization benchmarks relative to full EqSat.
  • The LLM-guided synthesis method transfers directly to an XLA-based tensor compiler.
  • The framework remains effective in logic-synthesis settings even after the rewrite vocabulary has been substantially enlarged.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Automating strategy design this way could lower the barrier to adopting equality saturation in new compiler domains where manual tuning has been prohibitive.
  • The rewrite-motif caching technique may transfer to other AI-assisted search tasks that face rapid state-space explosion.
  • Pairing EggMind with existing automatic rule-synthesis tools could produce a nearly complete pipeline for building domain-specific e-graph optimizers.
  • Because strategies remain readable in EqSatL, human experts could inspect, edit, or compose the automatically discovered guides.

Load-bearing premise

The LLM agent, when given motif caching and tractability signals, will reliably locate strategies that keep e-graph growth manageable and yield better final programs than exhaustive rule application.

What would settle it

A set of benchmarks in which the lowest-cost program found by any EggMind strategy has either equal or higher cost, or requires equal or higher peak memory, than the program extracted from a full-EqSat run on the same input.

Figures

Figures reproduced from arXiv: 2604.17364 by Chenyun Yin, Youwei Xiao, Yun Liang, Yuyang Zou, Yuze Luo.

Figure 1
Figure 1. Figure 1: An example comparing (a) full EqSat and (b) strategic EqSat, and (c) the spectrum for their resource–quality trade-off [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Challenges and EggMind’s solutions bottleneck in compiler construction shifts from rule discov￾ery to strategy synthesis, as larger rewrite spaces demand more sophisticated control to prevent e-graph explosion. EggMind addresses this need by synthesizing reusable EqSat strategies from representative workloads, overcoming the limitations of manual scheduling, external guidance, and instance-specific online … view at source ↗
Figure 3
Figure 3. Figure 3: gives an overview of EggMind. The system takes three primary inputs: a collection of cases for evolution, a Offline Strategy Synthesis Online Reuse Selected Strategy Agentic Workflow Rewrite Motif Caching Tractability Guidance EqSatL Cases Rules Cost Model Other Cases EqSat Engine EggMind Backend Per-case Optimization EqSat code Results §5 §4 LLM-Guided Synthesis [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: EqSatL: (a) formal syntax and (b) an example strategy. counterweight. Without it, redundant states accumulate and eventually exhaust the search budget. According to these two observations, we cast strategy design into three control questions: which rewrites may interact, how their interaction is organized over time, and how the e-graph is contracted afterward. EqSatL follows this decomposition through thre… view at source ↗
Figure 5
Figure 5. Figure 5: At each iteration of EggMind’s offline strategy synthesis, the agentic workflow on the right proposes and evaluates EqSat strategies, updating the candidate pool and rewrite motif cache from iteration 𝑖 to iteration 𝑖 + 1. Expr1 EqSat Expr2 Trans R1 Trans R2 Congr R3 MergeFn Congr Congr R4 Sym Congr ... A B Congr R5 Rewrite Motif T4 → T5 → T6 5.0 T5 → T2 3.0 T3 → T2 T1→ T2 2.5 3.0 T3 → T1 2.5 Measurable Co… view at source ↗
Figure 6
Figure 6. Figure 6: Proof-derived rewrite motif caching in EggMind. (a) A successful EqSat run. (b) The proof tree, with local regions highlighted for extraction. (c) Rewrite motifs after lifting and deduplication. (d) Utility-based cache curation. We model the rewrite vocabulary as a directed rule de￾pendency graph 𝐺 = (𝑅, 𝐸,𝑤), where each node 𝑟 ∈ 𝑅 is a rewrite rule and each weighted edge 𝑤𝑖𝑗 estimates how strongly rule 𝑟𝑖… view at source ↗
Figure 7
Figure 7. Figure 7: Comparison of the vectorization benchmarks. The x-axis lists representative evolution and test cases. 2d-3 2 /3 2 2d-4 2 /3 2 mm-4 2 2d-10 2 /2 2 2d-10 2 /3 2 mm-8 2 2d-3x5/3 2 2d-10 2 /4 2 mm-10 2 mm-16 2 0.0 1.0 2.0 3.0 4.0 Cost (Relative to Full EggMind) Generator-only No Motif-Caching No Repeat No Partitioner Full EggMind System 2d-3 2 /3 2 2d-4 2 /3 2 mm-4 2 2d-10 2 /2 2 2d-10 2 /3 2 mm-8 2 2d-3x5/3 2… view at source ↗
Figure 8
Figure 8. Figure 8: Ratios in the vectorization component-attribution study on representative cases. The x-axis lists representative evolution and test cases. Runtime ratios above 2.0 are truncated for readability and annotated with their exact values. minutes and requires 53 model requests, using 4.35M in￾put tokens and 36.6K output tokens, for an estimated cost of roughly $3.16 per synthesis run under current pricing. This … view at source ↗
Figure 9
Figure 9. Figure 9: Trade-off among simplification controls. indicating benefits beyond one-shot generation. Removing the rule partitioner worsens cost by 23.1% but reduces run￾time by 63.3%, with all cases faster and 10/15 worse in cost. This suggests that partitioning mainly improves optimiza￾tion quality by organizing interacting rewrites into effective schedules, and lower search cost is a secondary effect. Al￾though the … view at source ↗
Figure 10
Figure 10. Figure 10: EqMap carry-benchmark comparison for cost reduction and wall-clock runtime across five configurations. 6.2 XLA-Based Tensor Compiler To evaluate EggMind beyond the vectorization domain, we turn to tensor graph optimization. Initial experiments on standard workloads from prior work, such as Tensat [38] and rcmcts [13], showed limited room for strategy synthe￾sis: in many cases, unguided EqSat already reach… view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper presents EggMind, an LLM-guided end-to-end framework for synthesizing reusable EqSat strategies. It introduces the EqSatL DSL to represent strategies as explicit, inspectable artifacts and proposes an LLM-guided agentic workflow equipped with proof-derived rewrite motif caching and tractability guidance. This workflow searches efficiently for high-quality strategies while maintaining stability under e-graph growth. Evaluation on vectorization benchmarks shows EggMind strategies reduce final cost by 45.1% and peak RAM by 69.1% relative to full EqSat; the same methodology transfers to an XLA-based tensor compiler and is demonstrated in a logic-synthesis case study with augmented rewrite spaces.

Significance. If the results hold, the work meaningfully advances automation of e-graph-based compilers by tackling the manual strategy design bottleneck that arises with large automatically synthesized rewrite sets. The concrete resource-quality improvements, successful cross-domain transfer, and introduction of an inspectable DSL for strategies are strengths that could see adoption in compiler optimization research. The empirical grounding with benchmark descriptions, baseline definitions, and resource measurements supports practical relevance.

minor comments (3)
  1. Abstract: the reported 45.1% cost and 69.1% RAM reductions are presented without reference to the number of benchmarks or runs; a brief preview of these details would improve readability for readers who stop at the abstract.
  2. §3.1: the EqSatL syntax and semantics are defined formally, but including one short concrete strategy example in the main text (rather than only the appendix) would aid comprehension of how the DSL captures reusable patterns.
  3. §5.2: the vectorization and XLA transfer experiments are clearly described, yet the paper could add a short statement on whether the same LLM prompt templates and caching parameters were reused without modification to support the generalization claim.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary, significance assessment, and recommendation of minor revision. We appreciate the recognition that EggMind addresses the manual strategy design bottleneck in e-graph compilers through the EqSatL DSL, LLM-guided workflow, and techniques like proof-derived rewrite motif caching. No specific major comments were provided in the report.

Circularity Check

0 steps flagged

No significant circularity; empirical framework with independent benchmarks

full rationale

The paper introduces EggMind as an LLM-guided framework using the EqSatL DSL and an agentic workflow with motif caching and tractability guidance. Its central claims rest on empirical measurements (45.1% cost reduction, 69.1% RAM reduction versus full EqSat on vectorization benchmarks, plus transfer to XLA) rather than any derivation chain, equations, fitted parameters, or predictions. No load-bearing step reduces to a self-definition, fitted input renamed as prediction, or self-citation chain; the evaluation supplies concrete baseline definitions and resource measurements that remain externally falsifiable. The work is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

The central claim rests on the existence of reusable strategy abstractions and the ability of LLMs to search them effectively; no free parameters are mentioned.

axioms (1)
  • domain assumption Equality saturation represents many equivalent programs compactly in an e-graph and defers commitment until extraction.
    Stated as background in the opening sentences of the abstract.
invented entities (2)
  • EggMind no independent evidence
    purpose: End-to-end LLM-guided framework for synthesizing reusable EqSat strategies
    Core system introduced to automate strategy design.
  • EqSatL no independent evidence
    purpose: Domain-specific language to represent EqSat strategies as explicit and inspectable artifacts
    Introduced to provide reusable abstractions for the LLM agent.

pith-pipeline@v0.9.0 · 5598 in / 1348 out tokens · 53984 ms · 2026-05-10T06:15:46.650828+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

45 extracted references · 36 canonical work pages · 3 internal anchors

  1. [1]

    Jai Arora, Sirui Lu, Devansh Jain, Tianfan Xu, Farzin Housh- mand, Phitchaya Mangpo Phothilimthana, Mohsen Lesani, Praveen Narayanan, Karthik Srinivasa Murthy, Rastislav Bodik, Amit Sabne, and Charith Mendis. 2025. TensorRight: Automated Verification of Tensor Graph Rewrites.Proc. ACM Program. Lang.9, POPL, Article 29 (Jan. 2025), 32 pages. doi:10.1145/3704865

  2. [2]

    Peter Borovansky, Claude Kirchner, Hélène Kirchner, and Christophe Ringeissen. 2001. Rewriting with Strategies in ELAN: A Functional Semantics.International Journal of Foundations of Computer Science 12, 01 (2001), 69–95. doi:10.1142/S0129054101000412

  3. [3]

    Ian Briggs, Yash Lad, and Pavel Panchekha. 2024. Implementation and Synthesis of Math Library Functions.Proc. ACM Program. Lang.8, POPL, Article 32 (Jan. 2024), 28 pages. doi:10.1145/3632874

  4. [4]

    Yaohui Cai, Kaixin Yang, Chenhui Deng, Cunxi Yu, and Zhiru Zhang

  5. [5]

    InProceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1

    Smoothe: Differentiable e-graph extraction. InProceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1. Association for Computing Machinery, New York, NY, USA, 1020–1034. doi:10. 1145/3669940.3707262

  6. [7]

    Chen Chen, Guangyu Hu, Cunxi Yu, Yuzhe Ma, and Hongce Zhang

  7. [8]

    In2025 62nd ACM/IEEE Design Au- tomation Conference (DAC)

    E-morphic: Scalable Equality Saturation for Structural Ex- ploration in Logic Synthesis. In2025 62nd ACM/IEEE Design Au- tomation Conference (DAC). IEEE, San Francisco, CA, USA, 1–7. doi:10.1109/DAC63849.2025.11133110

  8. [9]

    Hongzheng Chen, Alexander Novikov, Ngân V˜u, Hanna Alam, Zhiru Zhang, Aiden Grossman, Mircea Trofin, and Amir Yazdanbakhsh. 2026. Magellan: Autonomous Discovery of Novel Compiler Optimization Heuristics with AlphaEvolve. arXiv:2601.21096 [cs.AI]https://arxiv. org/abs/2601.21096

  9. [10]

    Jianyi Cheng, Samuel Coward, Lorenzo Chelini, Rafael Barbalho, and Theo Drane. 2024. SEER: Super-Optimization Explorer for High-Level Synthesis using E-graph Rewriting. InProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2(La Jolla, CA, USA)(ASP- LOS ’24). Association for ...

  10. [11]

    Chris Cummins, Volker Seeker, Dejan Grubisic, Baptiste Roziere, Jonas Gehring, Gabriel Synnaeve, and Hugh Leather. 2024. Meta Large Lan- guage Model Compiler: Foundation Models of Compiler Optimization. arXiv:2407.02524 [cs.PL]https://arxiv.org/abs/2407.02524

  11. [12]

    Leonardo Mendonça de Moura and Nikolaj S. Bjørner. 2008. Proofs and Refutations, and Z3. InLPAR Workshops.http://ceur-ws.org/Vol- 418/paper10.pdf

  12. [13]

    Steven Eker, Narciso Martí-Oliet, José Meseguer, Rubén Rubio, and Alberto Verdejo. 2023. The Maude strategy language.Journal of Logical and Algebraic Methods in Programming134 (Aug. 2023), 100887. doi:10.1016/j.jlamp.2023.100887

  13. [14]

    Oliver Flatt, Samuel Coward, Max Willsey, Zachary Tatlock, and Pavel Panchekha. 2022. Small Proofs from Congruence Closure. In2022 Formal Methods in Computer-Aided Design (FMCAD). 75–83. doi:10. 34727/2022/isbn.978-3-85448-053-2_13

  14. [15]

    Jakob Hartmann, Guoliang He, and Eiko Yoneki. 2024. Optimizing Tensor Computation Graphs with Equality Saturation and Monte Carlo Tree Search. InProceedings of the 2024 International Conference on Parallel Architectures and Compilation Techniques(Long Beach, CA, USA)(PACT ’24). Association for Computing Machinery, New York, NY, USA, 40–52. doi:10.1145/365...

  15. [16]

    Guoliang He, Zak Singh, and Eiko Yoneki. 2023. MCTS-GEB: Monte Carlo Tree Search is a Good E-graph Builder. arXiv:2303.04651 [cs.AI] 12 LLM-Guided Strategy Synthesis for Scalable Equality Saturation https://arxiv.org/abs/2303.04651

  16. [17]

    Matthew Hofmann, Berk Gokmen, and Zhiru Zhang. 2025. EqMap: FPGA LUT Remapping using E-Graphs. In2025 IEEE/ACM Interna- tional Conference On Computer Aided Design (ICCAD). 1–9. doi:10. 1109/ICCAD66269.2025.11240672

  17. [18]

    Thomas Koehler, Phil Trinder, and Michel Steuwer. 2022. Sketch- Guided Equality Saturation: Scaling Equality Saturation to Complex Optimizations of Functional Programs. arXiv:2111.13040 [cs.PL]https: //arxiv.org/abs/2111.13040

  18. [19]

    Thomas Kundefinedhler, Andrés Goens, Siddharth Bhat, Tobias Grosser, Phil Trinder, and Michel Steuwer. 2024. Guided Equality Saturation.Proc. ACM Program. Lang.8, POPL, Article 58 (Jan. 2024), 32 pages. doi:10.1145/3632900

  19. [20]

    Cole Kurashige, Ruyi Ji, Aditya Giridharan, Mark Barbone, Daniel Noor, Shachar Itzhaky, Ranjit Jhala, and Nadia Polikarpova. 2024. CCLemma: E-Graph Guided Lemma Discovery for Inductive Equa- tional Proofs.Proc. ACM Program. Lang.8, ICFP, Article 264 (Aug. 2024), 27 pages. doi:10.1145/3674653

  20. [21]

    Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2021. egg: Fast and extensible equality saturation.Proceedings of the ACM on Programming Languages 5, POPL (Jan. 2021), 1–29. doi:10.1145/3434304

  21. [22]

    Jules Merckx, Alexandre Lopoukhine, Samuel Coward, Jianyi Cheng, Bjorn De Sutter, and Tobias Grosser. 2026. E-Graphs as a Persistent Compiler Abstraction. arXiv:2602.16707 [cs.PL]https://arxiv.org/abs/ 2602.16707

  22. [23]

    Benjamin Mikek, Danylo Vashchilenko, Bryan Lu, and Panpan Xu

  23. [24]

    Agentic Code Optimization via Compiler-LLM Cooperation

    Agentic Code Optimization via Compiler-LLM Cooperation. arXiv:2604.04238 [cs.PL]https://arxiv.org/abs/2604.04238

  24. [25]

    InProceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, Alastair F

    Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox, Eva Darulova, Dan Grossman, and Zachary Tatlock. 2020. Synthe- sizing structured CAD models with equality saturation and inverse transformations. InProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation(London, UK) (PLDI 2020). Association for Computi...

  25. [26]

    Chandrakana Nandi, Max Willsey, Amy Zhu, Yisu Remy Wang, Brett Saiki, Adam Anderson, Adriana Schulz, Dan Grossman, and Zachary Tatlock. 2021. Rewrite rule inference using equality saturation.Proc. ACM Program. Lang.5, OOPSLA, Article 119 (Oct. 2021), 28 pages. doi:10.1145/3485496

  26. [27]

    Abdul Rafae Noor, Dhruv Baronia, Akash Kothari, Muchen Xu, Charith Mendis, and Vikram S. Adve. 2025. MISAAL: Synthesis-Based Au- tomatic Generation of Efficient and Retargetable Semantics-Driven Optimizations.Proc. ACM Program. Lang.9, PLDI, Article 198 (June 2025), 24 pages. doi:10.1145/3729301

  27. [28]

    Alexander Novikov, Ngân V˜u, Marvin Eisenberger, Emilien Dupont, Po-Sen Huang, Adam Zsolt Wagner, Sergey Shirobokov, Borislav Kozlovskii, Francisco J. R. Ruiz, Abbas Mehrabian, M. Pawan Ku- mar, Abigail See, Swarat Chaudhuri, George Holland, Alex Davies, Sebastian Nowozin, Pushmeet Kohli, and Matej Balog. 2025. Al- phaEvolve: A coding agent for scientific...

  28. [29]

    Duckki Oe, Andrew Reynolds, and Aaron Stump. 2009. Fast and flexible proof checking for SMT. InProceedings of the 7th International Workshop on Satisfiability Modulo Theories(Montreal, Canada)(SMT ’09). Association for Computing Machinery, New York, NY, USA, 6–13. doi:10.1145/1670412.1670414

  29. [30]

    OpenXLA Project. 2026. XLA: Optimizing Compiler for Machine Learning.https://openxla.org/xla/tf2xla. Accessed: 2026-04-14

  30. [31]

    Anjali Pal, Brett Saiki, Ryan Tjoa, Cynthia Richey, Amy Zhu, Oliver Flatt, Max Willsey, Zachary Tatlock, and Chandrakana Nandi. 2023. Equality Saturation Theory Exploration à la Carte.Proc. ACM Program. Lang.7, OOPSLA2, Article 258 (Oct. 2023), 29 pages. doi:10.1145/ 3622834

  31. [32]

    Lei Qiu, Zi Yang, Fang Lyu, Ming Zhong, Huimin Cui, and Xiaobing Feng. 2026. Beyond Pass-by-Pass Optimization: Intent-Driven IR Optimization with Large Language Models. arXiv:2602.18511 [cs.PL] https://arxiv.org/abs/2602.18511

  32. [33]

    Brett Saiki, Jackson Brough, Jonas Regehr, Jesús Ponce, Varun Pradeep, Aditya Akhileshwaran, Zachary Tatlock, and Pavel Panchekha. 2024. Target-Aware Implementation of Real Expressions. doi:10.48550/arXiv. 2410.14025arXiv:2410.14025 [cs]

  33. [34]

    Amir Shaikhha, Mathieu Huot, and Shideh Hashemian. 2024. A Ten- sor Algebra Compiler for Sparse Differentiation. InProceedings of the 2024 IEEE/ACM International Symposium on Code Generation and Op- timization(Edinburgh, United Kingdom)(CGO ’24). IEEE Press, 1–12. doi:10.1109/CGO57630.2024.10444787

  34. [35]

    Samuel Thomas and James Bornholt. 2024. Automatic Generation of Vectorizing Compilers for Customizable Digital Signal Processors. In Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1 (ASPLOS ’24, Vol. 1). Association for Computing Machinery, New York, NY, USA, 19–34. doi...

  35. [36]

    Jonathan Van der Cruysse, Abd-El-Aziz Zayed, Mai Jacob Peng, and Christophe Dubach. 2026. Parallel and Customizable Equality Satu- ration. InProceedings of the 35th ACM SIGPLAN International Con- ference on Compiler Construction(Sydney, NSW, Australia)(CC ’26). Association for Computing Machinery, New York, NY, USA, 94–105. doi:10.1145/3771775.3786266

  36. [37]

    Lee, James Bornholt, and Adrian Sampson

    Alexa VanHattum, Rachit Nigam, Vincent T. Lee, James Bornholt, and Adrian Sampson. 2021. Vectorization for digital signal processors via equality saturation. InProceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS ’21). Association for Computing Machin- ery, New York, NY, USA,...

  37. [38]

    Eelco Visser. 2001. Stratego: A Language for Program Transformation Based on Rewriting Strategies System Description of Stratego 0.5. In Rewriting Techniques and Applications, Aart Middeldorp (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 357–361

  38. [39]

    Youwei Xiao, Chenyun Yin, Yitian Sun, Yuyang Zou, and Yun Liang

  39. [40]

    In Proceedings of the 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2(USA)(ASPLOS ’26)

    Finding Reusable Instructions via E-Graph Anti-Unification. In Proceedings of the 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2(USA)(ASPLOS ’26). Association for Computing Machinery, New York, NY, USA, 749–763. doi:10.1145/3779212.3790162

  40. [41]

    Youwei Xiao, Yuyang Zou, and Yun Liang. 2025. SkyEgg: Joint Im- plementation Selection and Scheduling for Hardware Synthesis using E-graphs. arXiv:2511.15323 [cs.PL]https://arxiv.org/abs/2511.15323

  41. [42]

    Yichen Yang, Phitchaya Mangpo Phothilimtha, Yisu Remy Wang, Max Willsey, Sudip Roy, and Jacques Pienaar. 2021. Equality Saturation for Tensor Graph Superoptimization. arXiv:2101.01332 [cs.AI]https: //arxiv.org/abs/2101.01332

  42. [43]

    Jiaqi Yin, Zhan Song, Chen Chen, Yaohui Cai, Zhiru Zhang, and Cunxi Yu. 2025. e-boost: Boosted E-Graph Extraction with Adap- tive Heuristics and Exact Solving. arXiv:2508.13020 [cs.PL]https: //arxiv.org/abs/2508.13020

  43. [44]

    Niansong Zhang, Chenhui Deng, Johannes Maximilian Kuehn, Chia- Tung Ho, Cunxi Yu, Zhiru Zhang, and Haoxing Ren. 2025. ASPEN: LLM-Guided E-Graph Rewriting for RTL Datapath Optimization. In 2025 ACM/IEEE 7th Symposium on Machine Learning for CAD (MLCAD) (Santa Cruz, CA, USA). IEEE Press, 1–9. doi:10.1109/MLCAD65511. 2025.11189222

  44. [45]

    Yihong Zhang, Derek Gerstmann, Andrew Adams, and Maaz Bin Safeer Ahmad. 2026. Pushing Tensor Accelerators beyond MatMul in a User-Schedulable Language. In2026 IEEE/ACM International Symposium on Code Generation and Optimization (CGO). 242–254. doi:10.1109/CGO68049.2026.11395214 13 Chenyun Yin, Youwei Xiao, Yuze Luo, Yuyang Zou, and Yun Liang

  45. [46]

    Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, and Max Willsey. 2023. Better Together: Unifying Datalog and Equality Saturation.http://arxiv.org/ abs/2304.04332arXiv:2304.04332 [cs]. 14