Ingest: DreamCoder: growing interpretable knowledge with wake-sleep Bayesian program learning

Type: kb/sources/types/ingest-report.md

Source: dreamcoder-wake-sleep-bayesian-program-learning.md Captured: 2026-07-26 From: https://arxiv.org/abs/2006.08381

Classification

Genre: scientific-paper -- peer-reviewed-track research system paper with eight evaluated domains, ablations, and stated limitations; the snapshot carries the arXiv landing page for the June 2020 preprint. Domains: self-improving-systems, program-synthesis, abstraction, compression Author: Kevin Ellis, Catherine Wong, Maxwell Nye, Mathias Sable-Meyer, Luc Cary, Lucas Morales, Luke Hewitt, Armando Solar-Lezama, Joshua B. Tenenbaum (MIT CSAIL / BCS). High credibility for the mechanism; the rediscovery framing is the authors' own and carries the usual self-assessment discount.

Summary

DreamCoder learns to solve inductive programming tasks by growing its own domain-specific language. A wake phase searches for programs solving training tasks, guided by a neural recognition model; an abstraction sleep phase refactors the discovered programs into semantically equivalent forms and adds new library primitives that minimize a Bayesian description-length objective over the corpus; a dreaming sleep phase retrains the recognition model on a mix of replayed real solutions and fantasies sampled from the current library. The refactoring search is the hard engineering: the space runs to roughly 10^14 rewrites under a three-step lambda-evaluation bound, made tractable by a version-space-algebra plus equivalence-graph structure with dynamic programming. Across eight domains -- list processing, text editing, LOGO graphics, tower building, probabilistic regexes, symbolic regression, physics identities, and recursive functional programming -- the system goes from near-zero to strong performance (SyGuS text editing 3.7% to 79.6% at 40s per task, matching CVC4 at an hour), and library depth correlates with performance at r=0.79. The headline claim is that the resulting knowledge is compositional and interpretable: from generic sequence and arithmetic primitives the system builds vector operations, then an inverse-square schema, then Newton's law of gravitation and Coulomb's law, solving 93% of 60 physics identities after eight cycles.

Connections Found

This source lands as the missing middle case in the KB's self-improving-systems casebook. A proposal-selection improvement loop requires search, evaluation, and operative retention currently sits between two poles -- Ashby's Homeostat, which retains without a reject-capable gate, and Gödel machines, which retain only on proof. DreamCoder is a third, working point: a real reject-capable gate that is statistical rather than proof-mediated, running computationally autonomously and cumulatively, which is also the mixed placement real self-improving systems occupy combinations no single rung captures predicts no single rung will capture. Its split between an inspectable library and an opaque recognition network is an external worked case for reflective coverage is graded across representational forms, which so far rests mainly on Commonplace's own case.

Its most productive role is as a counterpoint. Abstract an experience into a lesson only when you can state where the lesson stops makes boundary-statability the abstraction criterion; DreamCoder abstracts on a computed description-length reduction with no statable boundary and reports transfer anyway. The same substitution appears in self-revising discovery systems, whose MDL-gated regime transitions are structurally what DreamCoder's library growth does a decade earlier, and from the measurement side in SuperARC. Read together, these suggest the criterion is domain-scoped rather than wrong -- the tension is flagged, not settled here.

As a system, it is the pre-LLM ancestor of the skill-library reviews already in the KB (VOYAGER, SkillX, SkillRL), differing from all of them in what may reject a candidate. It is already cited indirectly: the EsoLangBench snapshot's bibliography names Ellis et al. as the learned-library program-synthesis precedent, and that reference now resolves in-KB.

Extractable Value

  1. A mechanical abstraction gate is available only where the retained artifact carries formal semantics. DreamCoder replaces the judgment "state where this lesson stops" with a computed description-length reduction -- which is possible because programs have evaluation semantics that make refactoring-equivalence decidable. This is the sharpest thing the source offers a prose knowledge base: it explains why Commonplace cannot mechanize its own abstraction gate, extending representational form from "form sets the review method" to "form sets the retention gate". [deep-dive]
  2. Gate strength, not autonomy, discriminates the library-growth family. Homeostat (none), Gödel machine (proof), DreamCoder (description length), VOYAGER (task success), SkillX/SkillRL (LLM or RL signal), KCSI (benchmark) are all computationally autonomous cumulative retainers differing almost only in what may reject a candidate. The KB treats these one at a time; DreamCoder is the datapoint that makes the ordering variable visible. [deep-dive]
  3. Compression is applied to semantic, not syntactic, reuse. The authors are explicit: "rather than compress out reused syntactic structures, we refactor the programs to expose reused semantic patterns," with a three-step evaluation bound and a version-space/e-graph structure to make it tractable. The transferable warning is that surface-similarity deduplication finds the wrong units -- the reusable abstraction is usually not literally present in any solution. [experiment]
  4. Library depth correlates with performance at r=0.79. Empirical support from a formal domain for the artifact-shape argument in short composable notes maximize combinatorial discovery: what improved was hierarchical depth of small reusable units, not a flat set of larger ones. [quick-win]
  5. The rediscovery result is a known-target benchmark with authored inputs. The 60 physics identities come from AP/MCAT cheat sheets, and the supplied primitives (map, fold, recursion, arithmetic) were chosen after the target was known. This is a clean pre-benchmark-literature instance for known-target discovery benchmarks show reachability, not discovery closure, and its contrast is DiscoverPhysics, which authors counterfactual worlds precisely to defeat recall. [quick-win]
  6. Retention split across a readable and an unreadable channel in one system. The library is explicit, inspectable, and transferable; the recognition network retains search competence nothing can read, trained 50/50 on replays and self-generated fantasies. A concrete external case for only explicit retention is durable, writable, and addressable. [just-a-reference]
  7. The formal-domain oracle exists, and this is what a loop looks like once it does. Automated synthesis is missing good oracles carves out formal domains where verification is cheap but cites no example; DreamCoder fills that parenthetical, and so bounds the note from outside rather than contradicting it. [quick-win]

Limitations (our opinion)

Our reading, not the authors'.

What was not tested is the part that matters for this KB. Every domain has crisp symbolic form and a hand-authored primitive set plus a curated suite of 100-200 tasks; the authors concede that "much real-world data is far messier" and that noise, natural language, and causal inference were not attempted. The description-length gate is therefore evaluated only where refactoring-equivalence is decidable, which is exactly the condition a prose KB does not meet -- so the result should not be read as evidence that compression is a general abstraction criterion.

The gate is also a proxy the paper does not separate from what it stands in for. Description length is measured over already-solved training programs; nothing in the criterion sees held-out generalization. Held-out performance is reported and is good, but the causal link from "shortens the training corpus" to "transfers" is asserted by correlation (the r=0.79 depth-performance figure) rather than isolated by an ablation that varies the gate while holding search fixed. The baselines compare against weaker search (enumeration, exploration-compression, RobustFill on the initial library) and against memorization, but not against a strong human-authored DSL for the same domain -- the comparison that would tell us whether learned libraries beat expert-designed ones, which is the question codification and relaxing navigate the bitter lesson boundary actually cares about.

The rediscovery claim is the weakest part and should be handled independently of the architecture claim. Targets were drawn from published formula sheets and primitives supplied afterwards; the simpler account of "rediscovers Newton's and Coulomb's laws" is that an inverse-square schema is the shortest program expressing several of the 60 supplied datasets, which is a reachability result. Cost is also under-advertised: convergence is typically a day on 20-100 CPUs, and the origami experiment ran roughly a CPU-year. A gate that is cheap to evaluate sits on top of a search that is not.

Finally, a capture caveat: the in-KB snapshot is a web-fetch of the arXiv /abs/ landing page and contains only title, authors, and abstract. Every mechanism-level and quantitative statement in this report was verified against the full paper text, not against the snapshot. A reader rechecking any number here must open the PDF; and the snapshot's own description frontmatter asserts mechanism the capture cannot support, which is worth checking across other web-fetch arXiv snapshots.

Write a note in kb/notes/ claiming that a mechanical abstraction gate is available only where the retained artifact carries formal semantics -- description-length reduction substitutes for boundary-statability in programs and cannot in prose -- citing this source and self-revising discovery systems as its two gated instances, and reconciling it with abstract an experience into a lesson only when you can state where the lesson stops, whose criterion it would scope rather than overturn.