Solver-aware decomposition trades ground-truth subgoals for tractable program search

On DeepCoder, the solver-blind decomposer is much better at copying annotated intermediate states: 79.2% versus 31.7% decomposition accuracy on the test distribution. Yet it is worse at getting the program synthesized from those states: 73.0% versus 87.2% synthesis accuracy. Under length generalization, the same inversion widens to 63.3% versus 21.5% for decomposition and 64.3% versus 79.8% for synthesis. 1

That is the central result of Solver-Aware Decomposition (SAD), a preprint submitted to arXiv on 4 August 2026. The paper's claim is narrower than "ground-truth decompositions are bad." It shows that, for a bounded synthesizer, matching the annotator's factorization can be a poor proxy for proposing an intermediate task the synthesizer can actually solve.

Programming-by-example (PBE) gives a system input-output examples and asks it to find a program in a domain-specific language (DSL) that satisfies them. Decomposition-based PBE inserts a learned model between the examples and the synthesizer: the decomposer proposes an intermediate output, and the synthesizer searches for a DSL program that produces that output. The resulting subprogram is executed, its output is added to the program state, and the process repeats until the original task is solved. 2

This interface creates a failure mode that ordinary supervised training cannot see. A subgoal may be close to the annotated one while being impossible for any single DSL operation, or it may be expressible but route the synthesizer through operations that fall outside its effective beam. The paper gives both kinds of example. In one DeepCoder task, the solver-blind model predicts an intermediate list that no one-step DSL function can produce; SAD proposes a realizable subgoal and solves the task. In another, the ground-truth path uses Scanl1 followed by a chain of ZipWith operations that the synthesizer cannot find within its search budget, while SAD reaches the same output through a shorter Map-based program. 2

The distinction is between structural fidelity and solver utility. Ground-truth subgoals measure whether the decomposer resembles the annotation. They do not measure whether the downstream model can turn those subgoals into executable steps.

The authors hold the synthesizer fixed and train only the decomposer. The synthesizer first learns to predict target program tokens with teacher forcing. SAD then samples a candidate subgoal and compares it with the decomposer's greedy subgoal by running both through the frozen synthesizer. The reward is the negative cross-entropy of the synthesizer on the target program. A sampled subgoal receives positive advantage when it puts the target program in a higher-probability region of the synthesizer's distribution than the greedy choice. 2

This is self-critical sequence training applied to problem formulation, not to final program generation. The decomposer still receives supervised cross-entropy on ground-truth subgoals, which keeps it in a meaningful decomposition space. The reinforcement-learning term searches within that space for subgoals the frozen solver finds tractable, and an entropy term prevents early collapse. Without the supervised scaffold, the paper reports near-zero decomposition accuracy and task accuracy below 20%. 2

At inference, SAD runs beam search over complete decomposition-synthesis trajectories. Each beam contains a partial program, its predicted intermediate states, and the synthesized subprograms. Candidates are scored with the combined log-probabilities of the decomposer and synthesizer, then pruned when they fail to parse or execute, duplicate a higher-scoring candidate, or exceed domain limits. Training, however, uses only single-step rewards; the gains on longer programs are an emergent consequence rather than a directly optimized trajectory objective. 2

The evaluation uses DeepCoder, LambdaBeam, and RobustFill. DeepCoder has multiple valid intermediate decompositions over list operations. LambdaBeam adds dynamically constructed lambdas and conditional operations, making the solver's search space less forgiving. RobustFill is the control: its residual-output construction largely fixes the order of decomposition, leaving little ambiguity for solver-aware feedback to exploit. The experiments use the same three-layer Transformer family, beam size 10, five random seeds, and 1,000 test tasks per seed; the comparisons use paired t-tests at the 5% level. 2

The reported diagnostic numbers make the paper's point more clearly than the headline task-accuracy gains:

The end-to-end relative improvement over the solver-blind baseline is 10.7% on DeepCoder's ordinary test split and 22.2% under length generalization. LambdaBeam shows 10.9% and 14.0% relative improvement in the same settings. All SAD-versus-baseline differences are statistically significant in the paper's reported tests. The larger gains on unseen program lengths fit the proposed mechanism: as a trajectory gets longer, one intractable intermediate can poison every later step. 2

The beam-oracle check asks whether the solver-blind model already generates a good decomposition but ranks it badly. Its oracle gains are below 2%, and giving the solver-blind model access to the ground-truth decomposition wherever it appears in its beam still leaves it below SAD's raw performance. That points to a coverage problem: SAD is generating intermediate targets that the imitation model rarely proposes, rather than merely reordering the same candidates. 2

The ground-truth oracle supplies the necessary qualification. It is stronger overall, reaching 94.7% ± 0.3% on DeepCoder's ordinary test setting and 79.8% ± 1.9% under length generalization; on LambdaBeam it reaches 89.6% ± 2.1% and 51.3% ± 5.5%. So SAD has not shown that its alternatives are generally better than the annotated decomposition. It has shown that the annotation is not universally optimal for this synthesizer: across the two settings and five seeds, SAD solves an average of 63.2 ± 6.7 DeepCoder tasks and 109.8 ± 18.3 LambdaBeam tasks that the ground-truth decomposition oracle misses. Fewer than 2% of those SAD-only solutions match the ground-truth program. 2

RobustFill behaves as the proposed falsifiability check predicts. SAD and the solver-blind baseline are effectively tied at 94.1% ± 0.3% versus 94.1% ± 0.4% on the test distribution, and 90.8% ± 0.5% versus 90.8% ± 0.3% under length generalization. When the task structure leaves little decomposition ambiguity, downstream solver feedback has little useful preference to learn. 2

DreamCoder makes the library itself a learned object. Its wake-sleep loop alternates between solving tasks, adding symbolic abstractions to a domain language, and training neural recognition models on imagined and replayed problems. The recognizer then guides symbolic search inside the expanding language. 3

LAPS changes the information available to that loop: natural-language annotations guide joint learning of program libraries and neurally guided search heuristics, with gains that remain when language hints disappear at test time. 4 Stitch takes a more symbolic route, using corpus-guided top-down synthesis and syntactic pattern matching to compress DSL programs into abstractions. Its comparison with DreamCoder reports 3–4 orders of magnitude lower runtime and 2 orders of magnitude lower memory while retaining comparable or better compressivity. 5 LILO combines LLM-guided synthesis, Stitch compression, and AutoDoc so that learned abstractions receive names and docstrings that can feed back into later synthesis; it evaluates the resulting loop on string editing, scene reasoning, and graphics composition. 6

SAD is adjacent to this lineage rather than a new member of its full loop. It has a learned DSL-facing guidance model, but its learned object is a decomposer for one fixed synthesizer. It does not grow a persistent library across a task corpus, optimize a Bayesian library prior, compress programs with Stitch, train on imagined tasks, or document abstractions. The paper changes the guidance interface: instead of asking only whether an intermediate state matches an annotation, it asks whether the downstream solver can act on it.

That distinction matters for DreamCoder-style systems. A recognition model is useful only through the search behavior it induces. SAD supplies a concrete test for that interface: if the recognizer's target is an explicit intermediate representation, measure the executor's actual tractability rather than treating the representation as self-validating. But the paper leaves open whether this feedback can coexist with a library that remains reusable and interpretable instead of becoming tuned to one solver's quirks.

The clean causal setup creates the paper's main limitations. SAD trains the decomposer for a specific frozen synthesizer, so changing the synthesizer requires retraining. The reward is single-step, so the decomposer and synthesizer do not negotiate how deep a subtask should be. Training also requires ground-truth programs; a specification-only version would need execution-based rewards. The authors say code will be released upon acceptance, so the preprint does not yet provide a released artifact to test. 1

The paper's contribution to the DreamCoder line is therefore specific. It identifies a measurable failure in neural program synthesis—higher fidelity to annotated subgoals can coexist with lower end-to-end success—and closes one missing feedback path from solver to recognizer. It does not advance wake-sleep library learning or demonstrate persistent DSL growth. The next hard test is to combine both requirements: let an explicit library grow across tasks while the neural guide learns which decompositions the current symbolic search can actually execute, then change the searcher and see whether the abstractions survive.