PaperlayerView exact revision on arXiv

Source-linked AI summary

babble: Learning Better Abstractions with E-Graphs and Anti-Unification

David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, Nadia Polikarpova

arXiv:2212.04596v1cs.PL

TL;DR

Prior library-learning methods generate many unhelpful candidates and are not robust to syntactic variation, limiting their scaling to larger inputs. LLMT uses domain-specific equational theories, e-graphs, and e-graph anti-unification to find reusable abstractions. BABBLE achieves better compression orders of magnitude faster than the state of the art and learns functions for larger CAD corpora previously beyond reach.

  • Problem

    Prior library learning generates many candidate abstractions that cannot help compression and is purely syntactic, making it brittle to superficial variation.

    Source: §1 · p. 2

  • Method

    LLMT incorporates a domain-specific equational theory and uses e-graphs with anti-unification to generate abstractions across equivalent programs.

    Source: §1 · p. 3, §4.1 · p. 16

  • Results

    BABBLE achieves better compression orders of magnitude faster than the state of the art and learns sensible functions for larger 2D CAD corpora previously too large for library-learning techniques.

    Source: §8 · p. 26

  • Takeaways & Limitations

    BABBLE learns reusable functions that compress larger 2D CAD datasets and match human intuition.

    Source: §1 · p. 3, §8 · p. 26

    LLMT relies on domain-specific equational theories that must be provided by domain experts.

    Source: §8 · p. 26

Abstract

from arXiv · show

Library learning compresses a given corpus of programs by extracting common structure from the corpus into reusable library functions. Prior work on library learning suffers from two limitations that prevent it from scaling to larger, more complex inputs. First, it explores too many candidate library functions that are not useful for compression. Second, it is not robust to syntactic variation in the input. We propose library learning modulo theory (LLMT), a new library learning algorithm that additionally takes as input an equational theory for a given problem domain. LLMT uses e-graphs and equality saturation to compactly represent the space of programs equivalent modulo the theory, and uses a novel e-graph anti-unification technique to find common patterns in the corpus more directly and efficiently. We implemented LLMT in a tool named BABBLE. Our evaluation shows that BABBLE achieves better compression orders of magnitude faster than the state of the art. We also provide a qualitative evaluation showing that BABBLE learns reusable functions on inputs previously out of reach for library learning.

1 INTRODUCTION

Library learning seeks reusable abstractions by compressing program corpora, but prior methods generate unhelpful candidates and are brittle to syntactic variation. LLMT addresses these limits with equational theories and e-graph anti-unification; BABBLE reports stronger compression faster and scales to larger CAD corpora.

1 INTRODUCTION

  • BABBLE’s compression objective counts both corpus and library AST nodes, discouraging overly specific functions and favoring reusable abstractions.In the Figure 1 example, total size drops from 208 to 72 AST nodes after introducing a scaled-polygon function.Source: §1 · pp. 1–2, Figure 1 · p. 2
  • Prior library learning generates many unusable candidate abstractions and relies on syntax, limiting robustness to superficial variation.For example, commutativity can make different expressions share an abstraction that a purely syntactic approach misses.Source: §1 · p. 2
  • LLMT uses anti-unification to generate candidate abstractions from least-general patterns shared by pairs of corpus subterms.Useful abstractions should occur at least twice, and should be as concrete as possible for the corpus.Source: §1 · p. 2
  • Selecting the optimal library requires extracting the smallest term from an e-graph with common sub-expressions, a computationally intensive problem.The proposed targeted subexpression-elimination algorithm uses domain knowledge to reduce the search space and supports beam-search approximation to trade accuracy for efficiency.Source: §1 · p. 3
  • BABBLE implements LLMT on the egg e-graph library, and its workflow distinguishes existing techniques from the paper’s contributions.The architecture overview uses gray boxes for existing techniques and black boxes for contributions.Source: §1 · p. 3, Figure 2 · p. 3
  • BABBLE achieves better compression than DreamCoder on its benchmarks in orders of magnitude less time, and handles larger 2D CAD corpora beyond DreamCoder’s reach.Adding domain-specific rewrites improves compression further, and BABBLE learns functions that match human intuition.Source: §1 · p. 3
  • LLMT incorporates a domain-specific equational theory, making library learning robust to syntactic variation by considering semantically equivalent programs.E-graphs and equality saturation compactly represent equivalent programs, while e-graph anti-unification computes common patterns across them using dynamic programming.Source: §1 · p. 3

2 OVERVIEW

BABBLE uses LLMT to learn abstractions despite semantics-preserving syntactic variation, representing equivalent programs and generating candidates directly from their shared structure. It then selects a compressed corpus by extracting a small term while accounting for shared abstractions.

2 OVERVIEW

  • From a 196-node simplified corpus, syntactic learning yields an 81-node compressed corpus, while BABBLE still finds the 72-node abstraction in a fraction of a second.The original 208-node corpus also compresses to 72 nodes with that abstraction.Source: §2 · p. 4

2.1 Representing Equivalent Terms with E-Graphs

  • Equality saturation with a domain-specific equational theory uses e-graphs to compactly represent programs equivalent to corpus terms, including forms that align syntactically.In the example, the rewrite rule allows a term from the simplified corpus to be represented in the form needed for the abstraction.Source: §2.1 · p. 5

2.2 Candidate Generation via E-Graph Anti-Unification

  • E-graph anti-unification finds dominant patterns across equivalent subterms, using bottom-up dynamic programming to reuse overlapping computations.BABBLE restricts candidates to the most concrete patterns matching pairs of corpus subterms; this can theoretically eliminate optimal patterns, though the authors report it works well in practice.Source: §2.2 · pp. 6–8

2.3 Candidate Selection via Targeted Common Subexpression Elimination

  • Candidate selection accounts for corpus-wide compression, including the trade-off between abstraction reuse and argument costs and the possibility that abstractions can be defined using others.The chosen library minimizes the combined size of library definitions and refactored programs.Source: §2.3 · pp. 8–9
  • BABBLE reduces selection to extracting the smallest term with common subexpressions, counting shared abstraction definitions only once.Its custom extraction algorithm uses domain-specific knowledge and approximation; beam search trades scalability for precision.Source: §2.3 · p. 9

3 LIBRARY LEARNING OVER TERMS

The section formalizes library learning as finding a smallest compressed corpus, then develops pattern-based compression and candidate-pruning methods. Its candidate-generation approximation is practical but theoretically incomplete.

3.1 Preliminaries

  • The formal problem seeks the smallest compressed term that evaluates to the input, with reusable abstractions counted once and restricted to closed terms.The exposition formalizes first-order terms, while the implementation is not limited to that setting.Source: §3 · p. 9, §3.1 · pp. 10–11

3.2 Pattern-Based Library Learning

  • Candidate abstractions use patterns as function bodies, replacing matching terms with applications that share each abstraction.The section reduces library learning to minimizing the size of a compressed term under these pattern-based rewrite rules.Source: §3.2 · pp. 11–12
  • Any optimal global solution can be obtained by compressing with patterns that match subterms of the original term.Pattern-based compression is sound and complete for the global library-learning problem.Source: §3.2 · p. 12

3.3 Pruning Candidate Patterns

  • Non-negative-cost patterns can be discarded safely; trivial patterns and patterns with a single match are also pruned.A trivial linear pattern has a skeleton too small to pay for introducing an application.Source: §3.3 · p. 13
  • BABBLE uses pairwise joins P2(t) instead of exploring the full parametrization lattice because generalizing candidates is expensive.This approximation is theoretically incomplete: a pattern needed for optimal compression may be absent from P2(t), though the authors report that it works well in practice.Source: §3.3 · p. 14

Syntax

The e-graph syntax distinguishes identifiers, constructor applications, and sets of those applications.

Syntax

4 LIBRARY LEARNING MODULO EQUATIONAL THEORY

LLMT combines equality saturation with library learning, representing equivalent programs in e-graphs before finding and selecting reusable patterns. Its e-graph anti-unification generates compression candidates from co-occurring e-classes while pruning dominated patterns and avoiding redundant cycle-derived candidates.

4.1 Top-Level Algorithm

  • LLMT applies equality saturation to represent terms equivalent under the supplied equations, then generates candidate patterns and selects compression rules to extract a smallest compressed term.Candidate generation uses e-graph anti-unification; selection constructs an e-graph of possible compressions before extracting the smallest result.Source: §4.1 · p. 16

4.2 Candidate Generation via E-Graph Anti-Unification

  • E-graph anti-unification computes candidate patterns directly over e-classes instead of enumerating represented terms, which may be infinite, without discarding optimal patterns.The algorithm memoizes pairwise anti-unification results using dynamic programming.Source: §4.2 · pp. 16, 18
  • For matching constructors, e-class anti-unification recursively combines child patterns; differing constructors yield a pattern variable, while visited pairs break cycles.Variables are named from the paired e-class ids, avoiding the need to track anti-substitutions.Source: §4.2 · p. 17
  • Dominant patterns can replace dominated candidates when they use a subset of the variables and are no larger, preserving no-worse compression while pruning redundancy.This dominance criterion also justifies discarding cycle-derived patterns because they are dominated by another solution.Source: §4.2 · pp. 17–18
  • Only pairs of co-occurring e-classes need anti-unification, where co-occurrence means one is a proper ancestor of the other or their ancestors are siblings.This restricts candidate generation to classes that can occur together in a represented term.Source: §4.2 · p. 18

5 CANDIDATE SELECTION VIA E-GRAPH EXTRACTION

BABBLE selects a library by minimizing the combined size of its definitions and the compressed corpus. It uses bottom-up cost-set propagation with pruning and an optional beam approximation to control the search.

Library Selection as E-Graph Extraction

  • The library objective minimizes the root term's size plus the sizes of library definitions, counting each definition once and allowing library abstractions to compress one another.For a fixed library, the smallest term can be found by traversing the e-graph.Source: §5 · p. 18

Exploiting Partial Shared Structure

  • Enumerating every subset of candidate patterns for library selection becomes intractable as the candidate set grows.BABBLE instead selects a library with bottom-up dynamic programming over cost sets.Source: §5 · p. 19
  • Cost sets pair a library with the smallest represented term's use cost, excluding library-definition size, and propagate upward through e-nodes and e-classes.Application nodes account for the called abstraction in the library, while their use cost includes the argument's use cost rather than the abstraction body.Source: §5 · p. 19, Figure 11 · p. 19
  • Partial-order reduction removes a cost pair when a smaller library has no greater use cost, pruning provably suboptimal alternatives.This often removes libraries containing redundant abstractions that compress the same subterms.Source: §5 · p. 19

Beam Approximation

  • An optional beam approximation caps library size and cost-set size, then retains the top K libraries ranked by total cost.The cost-set propagation figure marks the partial-order reduction and beam-approximation operations separately.Source: §5 · p. 19, Figure 11 · p. 19

6 EVALUATION

On DreamCoder benchmarks, BABBLE achieves better compression ratios than DreamCoder in 1–2 orders of magnitude less time. Evaluation on larger 2d CAD corpora finds that equational theories improve compression across all four benchmarks, while learned abstractions include recurring structures across domains.

6.1 Comparison with DreamCoder

  • BABBLE consistently achieves better compression ratios than DreamCoder on DreamCoder-domain benchmarks, and does so 1–2 orders of magnitude faster.The comparison plots benchmark compression ratio against run time; lower and farther right is better.Source: Figure 12 · p. 21, §6.1 · p. 22
  • DreamCoder’s benchmark inputs are grouped by synthesis task, and BABBLE treats programs within each group as equivalent in an e-class.The evaluation also includes a 1,000-program 2d CAD suite divided into four subdomains.Source: §6.1 · pp. 20, 22, §6 · p. 20

6.2 Large-Scale 2d cad Benchmarks

  • Adding equational theories improves compression on all four 2d CAD benchmarks and can also improve run time in two cases.Equational theories sometimes reduce e-graph work by combining relevant e-classes, despite typically making an e-graph larger.Source: §6.2 · pp. 22–23, Figure 13 · p. 23
  • On modified Nuts-and-bolts data with redundant transformations removed, BABBLE retains identical compression with equations but compresses worse without them.The authors identify redundant transformations as potentially useful without equations, but not required when LLMT can introduce them.Source: §6.2 · p. 23
  • BABBLE learns recurring abstractions across 2d CAD domains, including scaled polygons, rings of shapes, and both whole-model and component abstractions for Gadgets.The authors note that rigorous user studies are still needed to assess usability and readability of learned libraries.Source: §6.2 · p. 23

7 RELATED WORK

BABBLE builds on library learning, equality saturation, and anti-unification, while adding e-graph anti-unification and targeted extraction for library selection. Its approach supports equational theories and multiple abstractions, with a beam-search approximation for the larger joint search.

DreamCoder

  • Unlike DreamCoder, BABBLE uses equality saturation to make library learning robust to syntactic variation, and the evaluation reports more optimal abstractions faster.DreamCoder uses e-graph ideas for exploring refactorings with candidate libraries, not for this robustness in library learning.Source: §7 · p. 25

Stitch

  • Stitch interleaves candidate generation and selection in branch-and-bound search; BABBLE separates them and uses e-graph extraction to search over pattern subsets and their application.Stitch's rewrite strategy is precise, whereas BABBLE's larger search uses a beam approximation.Source: §7 · p. 25
  • BABBLE supports learning modulo equational theories and can learn multiple abstractions at once, while Stitch learns one best abstraction at a time with optimality guarantees.BABBLE sacrifices theoretical optimality and uses beam search because its joint search space is larger.Source: §7 · p. 25

Other Library Learning Techniques

  • Other library-learning systems restrict which subterms can be abstracted, reducing tractability costs but limiting the expressiveness of learned abstractions.The paper cites shape macros and top-level graphical-program abstractions as examples of such restrictions.Source: §7 · p. 25

Synthesis and Optimization using E-graphs

  • BABBLE applies anti-unification over e-graphs with domain-specific rewrites, a combination prior work had not shown.The paper also presents targeted common subexpression elimination for extraction, which it argues may apply to other equality-saturation uses.Source: §7 · p. 26

8 CONCLUSION AND FUTURE WORK

LLMT learns program abstractions modulo a user-provided equational theory, and BABBLE achieves better compression orders of magnitude faster than the state of the art. The conclusion also identifies user-supplied theories and incomplete anti-unification as limitations and directions for future work.

8 CONCLUSION AND FUTURE WORK

  • BABBLE achieves better compression orders of magnitude faster than the state of the art and learns sensible functions for 2D CAD data previously too large for library-learning techniques.The evaluation also found that domain-specific rewrites improve compression further.Source: §8 · p. 26
  • Equational theories matter for high compression, but domain experts must provide them; automated theory synthesis could help with this task.The authors identify Ruler and TheSy as possible aids.Source: §8 · p. 26
  • E-graph anti-unification is incomplete and misses patterns that could yield better compression, while extending Stitch’s top-down search is challenging because e-graph matches can come from different syntactic variants.The compression bound used by Stitch does not straightforwardly extend to e-graphs because abstraction gains must be balanced against syntactic-variant size differences.Source: §8 · p. 27

A PROOFS

The appendix proves properties of pattern-based library learning, including soundness and completeness under the global learning problem. It also gives supporting arguments about normalization, pattern matches, and compression proofs.

A PROOFS

  • The language of compressed terms is strongly normalizing, with the proof showing that each applicative-order β-step strictly decreases the number of λ-abstractions.The argument relies on the reduced redex having no inner β-redexes.Source: A PROOFS · p. 30
  • A pattern’s match count does not decrease across the described compression step; the proof considers matches outside, inside, and overlapping the β-redex.For a subterm in the β-redex body, the earlier term has a more specific subterm that still matches the pattern.Source: A PROOFS · p. 30
  • The theorem establishes soundness—compressed terms evaluate to the original—and completeness: a globally minimal solution can be obtained using patterns that match the original term.The completeness proof uses applicative evaluation to ensure the relevant abstraction corresponds to a valid pattern.Source: A PROOFS · p. 30
  • In the completeness argument, unused λ-bindings cannot occur in a minimal compressed term because removing them makes the term smaller without removing sharing.The proof also rules out free variables in a global library abstraction, since they would require outer λ-abstractions.Source: A PROOFS · p. 30

B ADDITIONAL EXPERIMENTS

BABBLE’s default configuration runs for 20 rounds; fewer rounds make it faster but worsen compression.

B ADDITIONAL EXPERIMENTS

  • Fewer than the default 20 rounds make BABBLE faster but yield worse compression.The plot compares configurations with fewer rounds against the default.Source: Figure 15 · p. 32

Related papers

Loading 2212.04596v1…