Machine Learning Guided Equality Saturation
summary
Equality saturation guides get generated by a small autoregressive tree transformer that decodes trees node‑by‑node with two cross‑attention encoders and disentangled attention to encode parent/child and sibling order. Training data comes from slicing proof traces produced by standard equality saturation, yielding about 8 million training tuples for the Rise language. The prototype trains in ~two days on a consumer GPU, produces useful short‑hop guides, and exposes token probabilities so uncertain subtrees can be replaced by sketches.
AI-written summary · about
chapters (13)
- 0:00ML-guided equality saturation intro
- 1:26Expert limits in equality saturation
- 3:12Replacing human guides with ML
- 4:35Choosing the right ML architecture for the task
- 6:44Tree transformer model
- 9:10Training data generation
- 10:18Implementation and training
- 11:43Evaluating guides and next steps
- 13:32Q&A: Training data
- 14:57Q&A: Sketches and patterns
- 17:03Q&A: Domain models vs pre-trained
- 18:29Q&A: Rewrite sets impact
- 19:56Closing remarks
related talks
13mMind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
30megg: Fast and Extensible Equality Saturation
21mImproving Equality Saturation for EDA via Semantic E-Graphs
20mEquality Saturation and Joins
24mOptimism in Equality Saturation
14mRewrite Rule Inference Using Equality Saturation
15mEquality Saturation Theory Exploration à la Carte
28mCERES: Making Equality Saturation Memory-Scalable