Prism is the first symbolic superoptimizer for tensor programs that uses sGraph for compact representation of program families, two-level search, e-graph equivalence checking, and auto-tuning to achieve up to 2.2x speedup over prior superoptimizers on LLM workloads.
hub
egg: Fast and extensible equality saturation
12 Pith papers cite this work. Polarity classification is still indexing.
12
Pith papers citing it
hub tools
citation-role summary
background 4
citation-polarity summary
roles
background 4polarities
background 4representative citing papers
Bonsai compiles queries to pruned tree traversals by deriving pruning conditions with extended symbolic interval analysis and fusing compound queries into single traversals.
Bayesian PLSs are special cases of non-stationary affine PIMs which are proven calibrated, and affine tracing automates construction of probabilistic iterative methods from classical code.
Refinement types are integrated as first-class citizens in Scala 3 with full participation in the type system, backed by a mechanized soundness proof in Rocq and a prototype compiler extension using an e-graph solver.
Tailwind introduces ALPs and ML-based planning to integrate workload-specific query accelerators into standard RDBMSes, achieving 1.38x average (up to 29x) speedup on TPC-H queries.
Nautilus auto-compiles math-like tensor descriptions into optimized GPU kernels, delivering up to 42% higher throughput than prior compilers on transformer models across NVIDIA GPUs.
A new abstract interpretation algorithm enables sound optimistic analysis of e-graphs during equality saturation, unifying it with non-destructive rewriting and improving precision on cyclic SSA programs.
Empirical comparison of equality saturation versus stochastic search on five benchmarks to evaluate if e-graphs are superior for rewrite-based optimization.
Applies egglog equality saturation and datalog rules to optimize higher-order function handling for LaTeX output and constraint detection in a lambda-calculus-based mathematical optimization modeler.
EggMind automates EqSat strategy synthesis via LLMs and EqSatL, cutting final cost 45.1% and peak RAM 69.1% versus full equality saturation on vectorization benchmarks while transferring to tensor compilers.
Aquas delivers a holistic hardware-software co-optimization framework on MLIR that models memory interfaces with cache effects and uses an e-graph retargetable compiler, achieving up to 15.61x speedup with 14.5% area overhead across four domains.
Novel optimization techniques for navigational graph queries achieve orders of magnitude performance gains over prior methods on diverse real-world workloads.
citing papers explorer
-
Prism: Symbolic Superoptimization of Tensor Programs
Prism is the first symbolic superoptimizer for tensor programs that uses sGraph for compact representation of program families, two-level search, e-graph equivalence checking, and auto-tuning to achieve up to 2.2x speedup over prior superoptimizers on LLM workloads.
-
Bonsai: Compiling Queries to Pruned Tree Traversals
Bonsai compiles queries to pruned tree traversals by deriving pruning conditions with extended symbolic interval analysis and fusing compound queries into single traversals.
-
Affine Tracing: A New Paradigm for Probabilistic Linear Solvers
Bayesian PLSs are special cases of non-stationary affine PIMs which are proven calibrated, and affine tracing automates construction of probabilistic iterative methods from classical code.
-
First-Class Refinement Types for Scala
Refinement types are integrated as first-class citizens in Scala 3 with full participation in the type system, backed by a mechanized soundness proof in Rocq and a prototype compiler extension using an e-graph solver.
-
Tailwind: A Practical Framework for Query Accelerators
Tailwind introduces ALPs and ML-based planning to integrate workload-specific query accelerators into standard RDBMSes, achieving 1.38x average (up to 29x) speedup on TPC-H queries.
-
Nautilus: An Auto-Scheduling Tensor Compiler for Efficient Tiled GPU Kernels
Nautilus auto-compiles math-like tensor descriptions into optimized GPU kernels, delivering up to 42% higher throughput than prior compilers on transformer models across NVIDIA GPUs.
-
Optimism in Equality Saturation
A new abstract interpretation algorithm enables sound optimistic analysis of e-graphs during equality saturation, unifying it with non-destructive rewriting and improving precision on cyclic SSA programs.
-
Rewrite System Showdown: Stochastic Search vs. EqSat
Empirical comparison of equality saturation versus stochastic search on five benchmarks to evaluate if e-graphs are superior for rewrite-based optimization.
-
Optimizing Optimizations, Declaratively: Optimizing the Higher-Order Functions in Mathematical Optimization with egglog
Applies egglog equality saturation and datalog rules to optimize higher-order function handling for LaTeX output and constraint detection in a lambda-calculus-based mathematical optimization modeler.
-
LLM-Guided Strategy Synthesis for Scalable Equality Saturation
EggMind automates EqSat strategy synthesis via LLMs and EqSatL, cutting final cost 45.1% and peak RAM 69.1% versus full equality saturation on vectorization benchmarks while transferring to tensor compilers.
-
Aquas: Enhancing Domain Specialization through Holistic Hardware-Software Co-Optimization based on MLIR
Aquas delivers a holistic hardware-software co-optimization framework on MLIR that models memory interfaces with cache effects and uses an e-graph retargetable compiler, achieving up to 15.61x speedup with 14.5% area overhead across four domains.
-
Optimizing Navigational Graph Queries
Novel optimization techniques for navigational graph queries achieve orders of magnitude performance gains over prior methods on diverse real-world workloads.