babble: Learning Better Abstractions with E-Graphs and Anti-unification
summary
Presents Library Learning Modulo Theory (LLMT) implemented as the tool babble, which uses e-graphs plus a new e-graph anti-unification algorithm and targeted CSE to propose and select abstractions across semantically equivalent program variants. Evaluated on 250-program benchmarks and DreamCoder corpora, it learns compact, reusable functions (five abstractions on the nut-and-bolt set), compresses some datasets >4× and reaches compression ratios up to ~2.6 versus ~1.2 for prior work, and runs orders of magnitude faster, demonstrating practical scalability and improved abstraction precision.
AI-written summary · about
chapters (7)
- 0:00Start
- 3:05who cares about library learning?
- 3:59what's the challenge?
- 6:40how does babble work?
- 8:12how do e-graphs work?
- 10:06how does e-graph anti-unification work?
- 13:36how well does it work?
related talks
23mUnified Compositional Formal Methods: Exact Separation Logic and the Gi...
45mAbstraction Considered Harmful (and other opinions about writing maintainable code)
16mThe Modular Imperative: Rethinking LLMs for Maintainable Software
39mA Lever for the Mind
48mBenefits of Abstract Modelling using Conjure
24mTowards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by(…)
07h 18mFull Workshop
14mExample-Based Live Programming for Everyone: Building Language-Agnostic Tools for Live Programming w