SPORES: Sum-Product Optimization via Relational Equality Saturation for Large Scale Linear Algebra
机器学习算法通常在线性代数（LA）中指定。LA表达式可以重写成更有效的形式，通过利用输入属性，如稀疏性，以及程序属性，如公共子表达式和可融合运算符。这些属性之间复杂的交互对执行开销的影响给编译器的优化带来了挑战。现有的编译器采用复杂的语法，使代码库复杂化，增加了维护成本，但无法搜索等价LA表达式的大空间，以找到最便宜的一个。我们介绍了一种通用的LA表达式优化技术，通过将LA表达式转换为关系代数（RA）表达式，优化后者，然后将结果转换回（优化）LA表达式。这种方法的一个主要优点是它是完整的，这意味着可以使用RA中的等价规则找到任何等价的LA表达式。挑战是搜索空间的主要大小，我们通过采用和扩展编译器中使用的技术来解决这个问题，称为相等饱和。我们将优化器集成到SystemML中，并在一系列机器学习任务中对其进行经验验证;我们表明，我们可以在SystemML中导出所有现有的手工编码优化，并执行新的优化，使速度从1.2倍提高到5倍。
2020-12-22 cs.DB cs.PL
E-Graphs as a Persistent Compiler Abstraction
Ghent University（根特大学）；University of Cambridge（剑桥大学）；University College London（伦敦大学学院）；University of Edinburgh（爱丁堡大学）
本文提出了一种在编译器中间表示中原生表示e-graph的方法，通过引入eqsat方言，实现等价饱和在不同中间表示层次上的统一应用，提升编译器优化能力。
2026-08-04 cs.PL
Rewrite Rule Inference Using Equality Saturation
许多编译器、合成器和定理证明器依赖重写规则来简化表达式或证明等价性。开发重写规则可能是困难的：规则可能是微妙的不正确的，有利可图的规则很容易错过，并且每当语义被调整时，规则集必须重新检查或扩展。大型规则集的应用也具有挑战性：冗余规则会减慢基于规则的搜索速度，并阻碍调试。本文探讨了如何平等饱和，一个有前途的技术，使用电子图应用重写规则，也可以用来推断重写规则。E-图可以复杂地表示指数大的枚举项和潜在的重写规则的集合。我们发现，平等饱和有效地缩小两个集，导致更快的合成更小，更一般的规则集。我们在一个名为ruler的工具中原型化了这些策略。与基于CVC 4构建的类似工具相比，ruler可以以25倍的速度合成5.8倍的小规则集，而不会影响验证功能。在一个端到端的案例研究中，我们展示了规则合成的规则，这些规则的性能与领域专家制作的规则一样好，并解决了一个流行的开源工具中的一个长期存在的问题。
2021-08-23 cs.PL
Metatheory.jl: Fast and Elegant Algebraic Computation in Julia with Extensible Equality Saturation
我们引入Metatheory.jl：一种轻量级和高性能的通用符号和元编程框架，旨在简化编写复杂Julia元程序的行为，并基于最先进的等式饱和技术和动态第一类抽象树（AST）模式匹配系统，利用本机项重写系统显著增强Julia，其中AST系统可以以代数方式动态组合，充分利用语言强大的反射能力。我们的贡献允许执行通用的符号数学，操作，优化，合成或分析语法上有效的Julia表达式与一个干净简洁的编程接口，无论是在编译或执行程序。
2021-02-15 cs.PL cs.SC
E-Path: Equality Saturation for Control-Flow Graphs
提出E-Path数据结构，通过将指令序列作为等价基本单元，在控制流图上实现等式饱和优化，避免破坏性重写并同时保留多个等价程序变体。
2026-05-27 cs.PL
Equality Saturation Guided by Large Language Models
本文提出LLM引导的等式饱和框架LGuess，通过引入e-graphs作为中间层，结合LLM预测重写检查点，解决了LLM生成可靠重写链困难的问题，在多元多项式分解任务上表现优异。
2025-11-01 cs.PL
Better Together: Unifying Datalog and Equality Saturation
本文提出 egglog，统一 Datalog 与等式饱和的定点推理系统，通过重写两个实际应用验证其更快、更简单且修复原有缺陷。
2023-05-15 cs.PL
Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations
最近的程序合成技术帮助用户定制CAD模型（例如，用于3D打印），将低级三角形网格反编译为构造性实体几何（CSG）表达式。如果没有循环或函数，编辑CSG可能需要许多协调的更改，并且现有的网格反编译器使用可能混淆高级结构的语法。本文提出了第二个反编译阶段，强大的“收缩”非结构化CSG表达式到更多的可编辑程序与地图和折叠操作。我们提出Szalinski，一个工具，使用平等饱和与语义保持CAD重写有效地搜索较小的等效程序。Szalinski依赖于逆变换，这是求解器推测性地将等价物添加到E图的一种新方法。我们定性评估Szalinski的案例研究，显示它如何与现有的网格反编译器组成，并证明Szalinski可以在几秒钟内缩小大型模型。
2020-04-12 cs.CG cs.PL
Latent Idiom Recognition for a Minimalist Functional Array Language using Equality Saturation
本文提出用极简函数式数组语言结合等式饱和自动识别代码惯用法，匹配BLAS和PyTorch核心函数，实现1.46倍几何平均加速。
2023-12-29 cs.PL
Equality saturation theory exploration à la carte
University of Washington（华盛顿大学）；University of Pennsylvania（宾夕法尼亚大学）；University of California, Berkeley（加利福尼亚大学伯克利分校）；Certora Inc.（Certora公司）
本文提出Enumo，一种可编程领域特定语言，通过核心操作符和快进策略，实现可扩展、可组合的等式饱和规则推断，在多个领域超越现有方法，甚至匹配手动规则集效果。
2026-09-21 cs.PL
Scaling Program Synthesis Based Technology Mapping with Equality Saturation
本文提出Churchroad技术映射器，将等价饱和与程序综合工具结合，解决FPGA映射中草图编写困难及SMT求解器乘法处理弱的问题，可处理更大更复杂的设计且无需用户提供草图。
2024-11-19 cs.AR cs.PL
Equality Saturation: A New Approach to Optimization
传统编译器中的优化是顺序应用的，每个优化都破坏性地修改程序以产生转换后的程序，然后将其传递到下一个优化。我们提出了一种新的方法来构造编译器的优化阶段。在我们的方法中，优化采用相等分析的形式，将相等信息添加到公共中间表示中。优化器通过重复应用这些分析来推断程序片段之间的等价性，从而使中间表示充满等式。一旦饱和，中间表示编码输入程序的多个优化版本。在这一点上，盈利性启发式从饱和表示中表示的各种程序中挑选最终优化的程序。我们提出的结构优化器的方法比以前的方法有各种好处：我们的方法避免了需要担心优化排序，使使用一个全局优化启发式，选择完全优化的程序，并可用于执行翻译验证，即使在编译器比我们自己的。我们提出了我们的方法，形式化，并描述了我们选择的中间表示。我们还提出了实验结果表明，我们的方法是实用的时间和空间开销方面，是有效的发现复杂的优化机会，并有效地执行翻译验证一个现实的优化。
2011-03-25 cs.PL
Equality Saturation for Optimizing High-Level Julia IR
开发了基于 e-graphs 和等式饱和的系统，允许领域专家通过重写规则优化 Julia 代码，支持控制流、副作用、多重派发约束及类型传播，并提出 ILP 公式和 CFG 骨架松弛技术。
2025-07-13 cs.PL cs.SE
Rewrite System Showdown: Stochastic Search vs. EqSat
Stanford University（斯坦福大学）；University of Washington（华盛顿大学）
本文通过五个基准测试比较等式饱和与随机搜索在等式程序优化中的性能，以评估e-graphs的实际效果。
2026-05-22 cs.PL
Small Proofs from Congruence Closure
可满足性模理论（SMT）求解器和等式饱和引擎必须从基于e图的同余闭包过程生成证明证书，以实现验证和冲突子句生成。较小的证明证书加快了这些活动。虽然生成最小尺寸的证明的问题是NP完全的，现有的证明最小化算法的同余闭包生成不必要的大证明，并引入渐近开销的核心同余闭包过程。在本文中，我们引入了一个O（n^5）时间算法，该算法在一个新的放松的“证明树大小”度量下生成最佳证明，该度量直接限制了证明大小。然后，我们放松这种方法进一步到一个实用的O（n \log（n））贪心算法，产生小的证明，没有渐近开销。我们在egg equality saturation toolkit中实现了我们的技术，产生了第一个验证equality saturation引擎。我们表明，我们的贪婪的方法在鸡蛋快速生成大大小于国家的最先进的Z3 SMT求解器上的3760基准语料库的证明。
2022-09-07 cs.PL
SkyEgg: Heterogeneity-Aware Hardware Synthesis via Equality Saturation
Peking University（北京大学）
SkyEgg提出异构感知的FPGA硬件综合框架，通过等式饱和统一代数重写与资源映射，联合调度优化，平均加速Vitis HLS 3.12倍、Altera HLS 3.18倍。
2026-09-15 cs.CL cs.PL
LLM-Guided Strategy Synthesis for Scalable Equality Saturation
Peking University（北京大学）；School of Integrated Circuits（集成电路学院）
本文提出EggMind框架，通过领域特定语言EqSatL和LLM引导的代理工作流，高效合成可重用的等式饱和策略，提升资源质量平衡，减少成本和内存消耗。
2026-04-19 cs.AI cs.MA cs.PL
HEC: Equivalence Verification Checking for Code Transformation via Equality Saturation
本文提出基于e-graph和MLIR的等价性检查框架HEC，能够全面验证源到源代码变换的正确性，在PolyBenchC上成功验证循环展开、分块和融合，并发现mlir-opt中的两个关键编译错误。
2025-06-06 cs.AR cs.PL
Finding models through graph saturation
我们给出了一个程序，可以用来自动满足一定形状的不变量。这些不变量可以用运算交集、合成和二元关系上的转换以及这些运算上的相等来写。我们称这些不变量为\tr{}，我们解释了图。对于通过这些句子集合陈述的问题，本文给出了一个半判定过程，我们称之为图饱和。它决定在这些\tr{}上的蕴涵，灵感来自图重写。我们证明了程序的正确性。此外，我们证明了相应的决策问题是不可判定的。这证实了作者先前提出的一个猜想。
2018-06-25 cs.DM cs.LO cs.PL
There and Back Again: A Netlist's Tale with Much Egraphin'
本文提出用等式饱和项重写框架统一处理EDA编译与反编译任务，并通过案例研究验证其特性与EDA需求高度契合。
2024-03-31 cs.AR cs.PL
Colored E-Graph: Equality Reasoning with Conditions
本文提出着色E-Graph，通过在单一结构中用颜色编码表示多个粗化同余关系，解决E-graph难以处理多假设情形分裂的问题，实验表明其空间开销降低一个数量级且时间开销相近。
2023-05-30 cs.PL
Augmenting Rewrite Rule Sets via Knuth-Bendix Completion
Saarland University（萨尔兰州立大学）
本文评估了 Knuth-Bendix 完备化方法，用于自动生成和扩充等式饱和中的重写规则，实验表明其能加快优化并发现先前遗漏的优化机会。
2026-10-02 cs.PL
Automated Code Optimization with E-Graphs
本文提出了一个先进的，通用的和高层次的代码重写和分析系统的Julia程序设计语言，提供应用的平等饱和存在的多重分派和元编程。我们展示了我们的系统如何实际解决一些具有挑战性的问题：程序员可以实现自己的高层次的编译器优化其特定领域的科学计划，而不要求他们在所有的编译器专家？这些优化器是否可以由用户在相同的语言和他们想要优化的相同程序中实现，从而解决两种语言的问题？这些编译器优化器是否可以以高级方式编写，如方程式，而无需担心重写顺序？因此，符号数学可以进行高级编译器优化，反之亦然吗？
2021-12-30 cs.PL cs.SC
Reflective Metagraph Rewriting as a Foundation for an AGI "Language of Thought"
MeTTa（Meta Type Talk）是一种新的程序设计语言，用于OpenCog Hyperon AGI系统。它被设计为一种元语言，具有非常基本和通用的设施，用于处理符号、接地、变量、类型、替换和模式匹配。原语的存在是为了创建新的类型系统和相关的DSL。非正式地说，MeTTa是Hyperon最低级的“思想语言”--学习更具体知识表示的算法将在其中操作的元语言，并且这些算法本身可以在其中表示。在这里，我们解释了如何将MeTTa语言形式化为元数据重写规则系统，这种方法自然适合Hyperon框架，因为后者的核心组件是分布式元数据知识存储（Atomspace）。构成MeTTa程序的元图重写规则也可以表示为元图，为MeTTa反射和自修改代码提供了自然模型。考虑到MeTTa程序计算其他MeTTa程序的执行轨迹之间的等价性，允许我们使用同伦类型论来建模MeTTa执行轨迹的空间。考虑到在MeTTa程序的执行轨迹之间映射的MeTTa程序的限制，我们发现，给定的MeTTa码基被有效地建模为无穷广群，并且所有MeTTa码基的空间被建模为（无穷，1）-topis。在离散物理学上下文中，该拓扑基本上与先前从关于超图的重写规则导出的所谓的“Ruliad”相同。作为元数据重写规则的MeTTA的形式化还可以提供有用的框架，用于在MeTTa解释器内构造用于模式匹配和等式推断的有效方法的实现。
2021-12-12 cs.PL
babble: Learning Better Abstractions with E-Graphs and Anti-Unification
库学习通过从语料库中提取公共结构来压缩给定的程序语料库，从而将其转换为可重用的库函数。之前关于库学习的工作受到两个限制，这阻止了它扩展到更大，更复杂的输入。首先，它探索了太多对压缩无用的候选库函数。其次，它对输入中的句法变化不鲁棒。我们提出了图书馆学习模理论（LLMT），一个新的图书馆学习算法，另外作为输入的方程理论为一个给定的问题域。LLMT使用e-graph和等式饱和来表示等价模理论的程序空间，并使用一种新的e-graph反统一技术来更直接有效地发现语料库中的公共模式。我们在一个名为BABBLE的工具中实现了LLMT。我们的评估表明，BABBLE实现了更好的压缩数量级比最先进的。我们还提供了一个定性的评估表明，BABBLE学习可重用的功能，以前无法达到的输入库学习。
2022-12-08 cs.PL
KestRel: Relational Verification Using E-Graphs for Program Alignment
本文提出KestRel关系验证方法，利用e-graph、等式饱和及数据驱动提取技术构建语义对齐的中间程序，以简化多程序关系性质验证。
2025-03-12 cs.PL
