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

Abstract

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.

arXiv commentPOPL 2023

References in corpus (6)

• egg: Fast and Extensible Equality Saturation
• Learning to Infer and Execute 3D Shape Programs
• Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations
• Learning to Infer Graphics Programs from Hand-Drawn Images
• Top-Down Synthesis for Library Learning
• ShapeMOD: Macro Operation Discovery for 3D Shape Programs

Cited by in corpus (6)

• Top-Down Synthesis for Library Learning
• Anti-unification and Generalization: A Survey
• WASM-MUTATE: Fast and Effective Binary Diversification for WebAssembly
• Equational Anti-Unification over Absorption Theories
• Synthesizing DSLs for Few-Shot Learning
• One or Nothing: Anti-unification over the Simply-Typed Lambda Calculus