EGRAPHS 2025
as the organisers put it
Research in the EGRAPHS Community has recently exploded in both quantity and diversity. The data structure that powers SMT solvers is now seeing use in synthesis, optimization, and verification via equality saturation and related techniques. In addition to recent advances in the core data structure and techniques, researchers and practitioners are applying e-graphs to domains such as compilers, floating point accuracy, test generation, computational fabrication, automatic vectorization, deep learning compute graphs, symbolic computation, and more. The fourth EGRAPHS workshop will bring tog ...
who it's for
e-graph researchers, compiler engineers, programming language researchers, verification engineers, formal methods engineers, machine learning for compilers researchers, high-level synthesis designers, homomorphic encryption engineers
topics
bottom-up e-matching; semantic eids canonicalization; tree-transformer rewrite guides; LLM-guided equality saturation; ahead-of-time e-graph compilation; incremental equality saturation; destructive e-graph rewrites; e-graph anti-unification; CEGAR with e-graphs; MLIR e-graph dialect; e-graph guided stochastic mutations; ILP-based extraction for FHE
| title | author | length |
|---|---|---|
| Omelets Need Onions: E-graphs Modulo Theories via Bottom Up E-Matching | Philip Zucker | 35m |
Claims that bottom-up e-matching plus semantic eids lets e-graphs incorporate domain theories by canonicalizing terms before matching, avoiding combinatorial… | ||
| Machine Learning Guided Equality Saturation | Nicole Heinimann, Thomas Koehler, Michel Steuwer | 20m |
Equality saturation guides get generated by a small autoregressive tree transformer that decodes trees node‑by‑node with two cross‑attention encoders and… | ||
| Equality Saturation Guided by Large Language Models | Wentao Peng, Ruyi Ji, Yingfei Xiong | 26m |
Introduces LLM-guided equality saturation (LGuess): LLMs propose sparse, high‑level rewrite checkpoints while e‑graphs supply the low‑level rewrite chains; a… | ||
| Oatlog: A performant ahead-of-time compiled e-graph engine | Loke Gustafsson, Erik Magnusson, Alejandro Luque Cerpa | 22m |
Oatlog compiles egglog theories ahead-of-time Rust proc macro into generated Rust code, represents e-nodes as rows in operator-specific relations, and… | ||
| Incremental Equality Saturation | Rupanshu Soi, Benjamin Driscoll, Ke Wang, Alex Aiken | 24m |
Introduces an incremental egraph with per–e-class versions and a top-K analysis (K=2) so rewrites only target e-classes created by the current version and… | ||
| Destructive E-Graph Rewrites | Paul Zhang, Yisu Remy Wang | 19m |
Implements destructive rewrites in egg by e‑matching each rule left hand side and deleting matching right hand side enodes rather than adding them, requiring… | ||
| Automated High-Level Synthesis Design Modularization via E-Graph Anti-Unification | Andy Wanna, Cong "Callie" Hao, Theo Drane | 30m |
Framework automatically finds shared HLS modules by combining e-graph anti-unification with polyhedral loop analysis via the ISL integer sets library… | ||
| Hatching Theory Instantiations with Yardbird | Cole Vick, Samuel Thomas | 16m |
Yardbird is a CEGAR framework that uses egg’s equality saturation engine to hatch array theory instantiations: axioms become rewrite rules, e-classes that… | ||
| eqsat: An Equality Saturation Dialect for Non-destructive Rewriting | Jules Merckx, Alexandre Lopoukhine, Samuel Coward, Jianyi Cheng, Bjorn De Sutter, Tobias Grosser | 19m |
An MLIR-based e-graph representation called eqsat dialect encodes e-classes and e-nodes as MLIR ops and uses MLIR graph regions to express cycles so equality… | ||
| Using Equality Saturation and Stochastic Mutations for Molecular Dynamics Code(…) | Oren Hecht, Yotam M. Y. Feldman, Barak Hirshberg, Hila Peleg | 22m |
Prototype framework combines equality saturation with random code mutations to optimize real Python molecular‑dynamics kernels, reproducing algebraic speedups… | ||
| Optimizing Optimizations: Case Study on Detecting Specific Types of Mathematical(…) | Hiromi Ishii, Taro Shimizu, Toshiki Teramura | 22m |
JijModeling separates symbolic formula from input data and uses e-graphs to detect structured constraints like SOS1 so solvers can use dedicated APIs… | ||
| Cut Tracing with E-Graphs for Boolean FHE Circuit Synthesis | Julien de Castelnau, Mingfei Yu, Giovanni de Micheli | 21m |
Proposes cut tracing that records replacement candidates from ESOP balancing and cut rewriting into an e-graph and then runs ILP-based extraction to jointly… | ||
| nothing matches | ||