pith. sign in

arxiv: 2605.19005 · v2 · pith:YAJND2TRnew · submitted 2026-05-18 · 💻 cs.PL

Rewrite System Showdown: Stochastic Search vs. EqSat

Qiantan Hong , Rupanshu Soi , Yihong Zhang , Alex Aiken This is my paper

Pith reviewed 2026-05-25 05:57 UTC · model grok-4.3

classification 💻 cs.PL
keywords equality saturationstochastic searche-graphsprogram optimizationrewrite systemsequational optimizationbenchmarks
0
0 comments X

The pith

Equality saturation using e-graphs is compared directly to stochastic search on five benchmarks to test whether it is actually good.

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

The paper observes that equality saturation has become the main method for equational program optimization even though it has never faced a rigorous head-to-head test against other techniques. It fills that gap by running equality saturation against stochastic search on five benchmarks. A reader would care because the outcome decides whether the field should keep building on e-graphs or should treat stochastic search as a serious competitor. The work supplies concrete performance data instead of relying on the prior assumption that e-graphs are superior.

Core claim

The paper performs a direct comparison of equality saturation and stochastic search across five benchmarks in order to answer whether e-graphs are actually good for equational program optimization.

What carries the argument

Head-to-head evaluation of equality saturation (EqSat) versus stochastic search on five shared benchmarks.

Load-bearing premise

The five chosen benchmarks are representative of the practical workloads where equational optimization matters.

What would settle it

Running the same two methods on a sixth benchmark that produces a clear and consistent winner absent from the original five would show the comparison does not yet settle the general question.

Figures

Figures reproduced from arXiv: 2605.19005 by Alex Aiken, Qiantan Hong, Rupanshu Soi, Yihong Zhang.

Figure 1
Figure 1. Figure 1: Showdown for matrix chain multiplication. 3 Showdown In this section, we present detailed results comparing EqSat and stochastic search for 5 applications. Experiments are run on servers with a 64-Core CPU with hyperthreading and 500 GB of memory. We give 10 seconds of wall-clock time to both techniques, except Section 3.5 where the time limit is set to 3 seconds. We use egg’s default BackOffScheduler for … view at source ↗
Figure 2
Figure 2. Figure 2: Showdown for trigonometric simplification. search as dom(LHS(cancel)) ⊊ dom(RHS(cancel)), so it can cause unsoundness only if applied right to left, which happens in EqSat because EqSat forgets the direction in which a rule was applied. Consequently, there is a proof in EqSat of 0 = 1 by relying on cancel and a few other (sound) rules: 1 ⇐ 𝑥 − 𝑥 𝑥 − 𝑥 ⇒ 0 𝑥 − 𝑥 ⇒ 0 To ensure the validity of solutions in th… view at source ↗
Figure 3
Figure 3. Figure 3: Number of proposals and benchmarks solved vs. number of threads for stochastic search on trigonometric simplification [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Showdown on compressing CAD expressions. plots use a similar format as before: the x-coordinate of a point gives the cost of the program found by stochastic search, and the y-coordinate gives the cost found by EqSat. The histograms show the distribution of the ratios between costs found by EqSat and by stochastic search. Overall, neither technique dominates the other—there are programs on which EqSat finds… view at source ↗
Figure 5
Figure 5. Figure 5: Cost distribution of unproved Halide inequalities. as well as max and min operators. We implemented the same set of rules with stochastic search, and evaluate both systems on Caviar’s “hard” dataset. Each test consists of an inequal￾ity over symbolic variables to be proved or disproved, e.g., max(𝑖, 2) < max(𝑖 + 3, 3). Results are shown in [PITH_FULL_IMAGE:figures/full_fig_p005_5.png] view at source ↗
read the original abstract

Equality saturation has become a dominant paradigm for equational program optimization. However, it has never been rigorously compared to another approach to the same problem, even though several exist, the most notable being stochastic search. In this paper, we compare equality saturation to stochastic search over five benchmarks to answer the question: are e-graphs actually good?

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

1 major / 1 minor

Summary. The paper claims that equality saturation (EqSat) has become the dominant paradigm for equational program optimization yet has never been rigorously compared to stochastic search. It performs an empirical comparison of the two approaches across five benchmarks to determine whether e-graphs are actually good.

Significance. If the comparison is methodologically sound and the benchmarks representative, the work would fill a notable gap by providing the first direct head-to-head evaluation of EqSat versus stochastic search, offering empirical guidance on when e-graphs are preferable in rewrite-based optimization.

major comments (1)
  1. [§4 and abstract] The central claim that the five-benchmark comparison suffices to answer whether e-graphs are good requires the benchmarks to be representative of practical equational-optimization workloads. No selection criteria, diversity metrics, or mapping to real compiler/optimizer use cases are provided (see §4 and the abstract). This is load-bearing for the headline conclusion.
minor comments (1)
  1. [Abstract] The abstract contains no mention of methodology, metrics, statistical tests, or results, which is atypical for an empirical comparison paper and hinders quick assessment of the contribution.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for highlighting the importance of benchmark representativeness for our central claim. We address this point below and will revise the manuscript to strengthen the presentation.

read point-by-point responses

  1. Referee: [§4 and abstract] The central claim that the five-benchmark comparison suffices to answer whether e-graphs are good requires the benchmarks to be representative of practical equational-optimization workloads. No selection criteria, diversity metrics, or mapping to real compiler/optimizer use cases are provided (see §4 and the abstract). This is load-bearing for the headline conclusion.

    Authors: We agree that explicit justification for benchmark selection is necessary to support the headline conclusion. The current manuscript presents the five benchmarks without detailing selection criteria, diversity metrics, or explicit mappings to real-world compiler workloads. In revision we will add a dedicated subsection in §4 that (1) states the criteria used to choose the benchmarks (coverage of distinct rewrite domains drawn from prior EqSat and stochastic-search literature), (2) reports simple diversity metrics (e.g., number of rules, expression sizes, and optimization objectives), and (3) discusses the extent to which each benchmark corresponds to documented use cases in production compilers. We will also adjust the abstract wording to reflect that the comparison provides evidence on the five chosen workloads rather than a universal claim. These changes directly address the load-bearing concern. revision: yes

Circularity Check

0 steps flagged

No derivation chain present; empirical comparison only

full rationale

The paper reports an empirical head-to-head evaluation of equality saturation versus stochastic search on five benchmarks. No equations, first-principles derivations, fitted parameters, or predictive claims appear in the abstract or stated methodology. The result is a direct experimental outcome rather than any reduction of a claimed prediction to its own inputs. Consequently the circularity patterns (self-definitional, fitted-input-called-prediction, self-citation load-bearing, etc.) have no purchase.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

No mathematical content, parameters, axioms, or invented entities are present in the abstract.

pith-pipeline@v0.9.0 · 5576 in / 930 out tokens · 25023 ms · 2026-05-25T05:57:24.177111+00:00 · methodology

Review history (2 revisions) →

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

32 extracted references · 32 canonical work pages · 1 internal anchor

  1. [1]

    Russel Arbore, Alvin Cheung, and Max Willsey. 2025. Optimism in Equality Saturation.arXiv preprint arXiv:2511.20782(2025)

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  2. [2]

    Anonymous Authors. 2025. Better E-Graphs for Imperative Programs (This ICFP Submission)

    work page 2025

  3. [3]

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

    work page

  4. [4]

    InProceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1(Rotterdam, Netherlands)(ASPLOS ’25)

    SmoothE: Differentiable E-Graph Extraction. InProceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1(Rotterdam, Netherlands)(ASPLOS ’25). Association for Computing Machinery, New York, NY, USA, 1020–1034. doi:10.1145/3669940.3707262

    work page doi:10.1145/3669940.3707262

  5. [5]

    Alessandro Cheli. 2021. Metatheory.jl: Fast and Elegant Algebraic Computation in Julia with Extensible Equality Saturation.Journal of Rewrite System Showdown: Stochastic Search vs. EqSat EGRAPHS ’26, June 15, 2026, Boulder, CO, USA Open Source Software6, 59 (2021), 3078. doi:10.21105/joss.03078

    work page doi:10.21105/joss.03078 2021

  6. [6]

    Chen Chen, Guangyu Hu, Dongsheng Zuo, Cunxi Yu, Yuzhe Ma, and Hongce Zhang. 2024. E-Syn: E-Graph Rewriting with Technology- Aware Cost Functions for Logic Synthesis. InProceedings of the 61st ACM/IEEE Design Automation Conference(San Francisco, CA, USA) (DAC ’24). Association for Computing Machinery, New York, NY, USA, Article 124, 6 pages. doi:10.1145/36...

    work page doi:10.1145/3649329.3656246 2024

  7. [7]

    Constantinides, and Theo Drane

    Samuel Coward, George A. Constantinides, and Theo Drane. 2023. Combining E-Graphs with Abstract Interpretation. InProceedings of the 12th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis(Orlando, FL, USA)(SOAP 2023). Association for Computing Machinery, New York, NY, USA, 1–7. doi:10.1145/3589250. 3596144

    work page doi:10.1145/3589250 2023

  8. [8]

    Persi Diaconis. 2009. The Markov Chain Monte Carlo Revolution.Bull. Amer. Math. Soc.46, 2 (2009), 179–205. doi:10.1090/S0273-0979-08- 01238-X

    work page doi:10.1090/s0273-0979-08- 2009

  9. [9]

    David Eppstein and Daniel Frishberg. 2023. Improved Mixing for the Convex Polygon Triangulation Flip Walk. In50th International Collo- quium on Automata, Languages, and Programming (ICALP 2023) (Leib- niz International Proceedings in Informatics (LIPIcs), Vol. 261), Kousha Etessami, Uriel Feige, and Gabriele Puppis (Eds.). Schloss Dagstuhl – Leibniz-Zentr...

    work page doi:10.4230/lipics.icalp.2023.56 2023

  10. [10]

    Kiran Gopinathan. 2025. Ego: An Extensible E-Graph Library for OCaml.https://github.com/verse-lab/ego. Accessed: 2026-04-06

    work page 2025

  11. [11]

    Stefan Heule, Eric Schkufza, Rahul Sharma, and Alex Aiken. 2016. Stratified synthesis: automatically learning the x86-64 instruction set. SIGPLAN Not.51, 6 (June 2016), 237–250. doi:10.1145/2980983.2908121

    work page doi:10.1145/2980983.2908121 2016

  12. [12]

    Qiantan Hong and Alex Aiken. 2024. Recursive Program Synthesis using Paramorphisms.Proc. ACM Program. Lang.8, PLDI, Article 151 (June 2024), 24 pages. doi:10.1145/3656381

    work page doi:10.1145/3656381 2024

  13. [13]

    Zhihao Jia, Oded Padon, James Thomas, Todd Warszawski, Matei Za- haria, and Alex Aiken. 2019. TASO: optimizing deep learning computa- tion with automatic generation of graph substitutions. InProceedings of the 27th ACM Symposium on Operating Systems Principles(Huntsville, Ontario, Canada)(SOSP ’19). Association for Computing Machinery, New York, NY, USA, ...

    work page doi:10.1145/3341301.3359630 2019

  14. [14]

    Jason R Koenig, Oded Padon, and Alex Aiken. 2021. Adaptive restarts for stochastic synthesis. InProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Imple- mentation. 696–709

    work page 2021

  15. [15]

    Smail Kourta, Adel Abderahmane Namani, Fatima Benbouzid-Si Tayeb, Kim Hazelwood, Chris Cummins, Hugh Leather, and Riyadh Baghdadi

    work page

  16. [16]

    InProceedings of the 31st ACM SIGPLAN International Conference on Compiler Construction(Seoul, South Korea)(CC 2022)

    Caviar: an e-graph based TRS for automatic code optimization. InProceedings of the 31st ACM SIGPLAN International Conference on Compiler Construction(Seoul, South Korea)(CC 2022). Association for Computing Machinery, New York, NY, USA, 54–64. doi:10.1145/ 3497776.3517781

    work page arXiv 2022

  17. [17]

    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

    work page doi:10.1145/3632900 2024

  18. [18]

    Rodrigo Mesquita. 2022. hegg: Fast Equality Saturation in Haskell. https://hackage.haskell.org/package/hegg. Hackage package, BSD-3- Clause license. Accessed: 2026-04-06

    work page 2022

  19. [19]

    Wilcox, Eva Darulova, Dan Grossman, and Zachary Tatlock

    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...

    work page doi:10.1145/3385412.3386012 2020

  20. [20]

    Wilcox, and Zachary Tatlock

    Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, and Zachary Tatlock. 2015. Automatically Improving Accuracy for Floating Point Expressions.SIGPLAN Not.50, 6 (June 2015), 1–11. doi:10.1145/2813885. 2737959

    work page doi:10.1145/2813885 2015

  21. [21]

    Eric Schkufza, Rahul Sharma, and Alex Aiken. 2013. Stochastic super- optimization. InProceedings of the Eighteenth International Conference on Architectural Support for Programming Languages and Operating Sys- tems(Houston, Texas, USA)(ASPLOS ’13). Association for Computing Machinery, New York, NY, USA, 305–316. doi:10.1145/2451116.2451150

    work page doi:10.1145/2451116.2451150 2013

  22. [22]

    Eric Schkufza, Rahul Sharma, and Alex Aiken. 2014. Stochastic opti- mization of floating-point programs with tunable precision.SIGPLAN Not.49, 6 (June 2014), 53–64. doi:10.1145/2666356.2594302

    work page doi:10.1145/2666356.2594302 2014

  23. [23]

    Saul Shanabrook. 2024. Egglog Python: A Pythonic Library for E- graphs. arXiv:2305.04311 [cs.PL]https://arxiv.org/abs/2305.04311

    work page arXiv 2024

  24. [24]

    Stan Seibert Siu Kwan Lam, Stuart Archibald. 2025. Numba v2: Towards a SuperOptimizing Python Compiler. InProceedings of the Python in Science Conference (SciPy). fncj2446. doi:10.25080/fncj2446

    work page doi:10.25080/fncj2446 2025

  25. [25]

    Rupanshu Soi, Benjamin Driscoll, Ke Wang, and Alex Aiken. 2025. Incremental Equality Saturation. InEGRAPHS. Seoul, South Korea. https://rupanshusoi.github.io/pdfs/egraphs-25.pdf

    work page 2025

  26. [26]

    Glenn Sun, Yihong Zhang, and Haobin Ni. 2024. E-Graphs as Circuits, and Optimal Extraction via Treewidth. arXiv:2408.17042 [cs.DS]https: //arxiv.org/abs/2408.17042

    work page arXiv 2024

  27. [28]

    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

    work page doi:10.1145/3771775.3786266 2026

  28. [29]

    Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2021. egg: Fast and exten- sible equality saturation.Proc. ACM Program. Lang.5, POPL, Article 23 (jan 2021), 29 pages. doi:10.1145/3434304

    work page doi:10.1145/3434304 2021

  29. [30]

    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]

    work page arXiv 2021

  30. [31]

    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

    work page doi:10.1109/cgo68049.2026.11395214 2026

  31. [32]

    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.Proc. ACM Program. Lang. 7, PLDI, Article 125 (jun 2023), 25 pages. doi:10.1145/3591239

    work page doi:10.1145/3591239 2023

  32. [33]

    Philip Zucker. 2025. Omelets Need Onions: E-graphs Modulo Theories via Bottom-up E-matching. arXiv:2504.14340 [cs.PL]https://arxiv.org/ abs/2504.14340

    work page arXiv 2025