CORE Lab, Clausthal University of Technology, Clausthal-Zellerfeld, Germany
When Dividing Requires Knowing how to Conquer - aligning decomposition structure with a bounded synthesizer's tractable distribution, rather than imitating the annotator's factorization choices.
Decomposition-based PBE scales synthesis by splitting tasks into subtasks - a decomposer predicts intermediate subgoals, and a synthesizer generates programs conditioned on them. Execution-decomposition approaches such as ExeDec train the decomposer to imitate ground-truth (GT) subgoals, implicitly treating decomposition quality as intrinsic to the task.
We challenge this assumption. For bounded solvers with fixed inductive biases, GT decompositions reflect the annotator's factorization choices - not the solver's search dynamics. A decomposer trained to match GT decompositions may therefore propose subgoals that are logically valid yet intractable for the solver, and imitation-only training has no mechanism to correct this.
Decomposition quality is solver-relative, not intrinsic to the task. The same intermediate representation that is tractable for one solver may be search-intractable for another. Training must account for the specific synthesizer that will act on the subgoals.
We propose Solver-Aware Decomposition (SAD), a training framework that retains supervised training on GT subgoals as a structural scaffold, while additionally optimizing the decomposer online with policy gradients against a frozen learned synthesizer. Each sampled subgoal is rewarded by the synthesizer's cross-entropy loss on the target program - a continuous signal of subtask difficulty that encourages decompositions the solver can act on.
Our experiments reveal an accuracy paradox: higher agreement with GT decompositions does not improve synthesis success - even though the synthesizer was trained on the very same GT data the decomposer is optimized to mimic. SAD instead learns decompositions that trade GT alignment for solver tractability, yielding consistent gains in synthesis and end-to-end task accuracy across two PBE domains and under zero-shot transfer to an external list-processing benchmark. Moreover, SAD solves tasks that a GT decomposition oracle fails - empirical evidence, under an identical synthesizer and search procedure, that GT decompositions are not universally optimal for bounded solvers.
SAD treats decomposition as a solver-dependent decision problem: intermediate representations should be optimized for downstream usability under a fixed solver, rather than for similarity to GT structure.
The synthesizer is trained once with teacher forcing on the full current task specification to predict the next GT subprogram, then frozen. Unlike ExeDec's synthesizer, which is trained on GT subtasks, it must infer which subtask comes next as well as how to implement it - this is what lets it give meaningful feedback on decompositions that deviate from the GT trajectory. At inference, it receives the subtask induced by the predicted subgoal, exactly as in ExeDec. Freezing the synthesizer is a deliberate isolation choice: any improvement in task success is attributable solely to the decomposer.
The training objective combines a supervised scaffold with the RL signal and an entropy bonus to prevent collapse:
Supervised imitation of GT subgoals keeps the decomposer within a meaningful decomposition space. Without it, the policy collapses to degenerate outputs and task accuracy falls below 20%.
SCST feedback from the frozen synthesizer steers the decomposer toward subgoals in the solver's tractable distribution - including subgoals the annotator never explicitly specified.
Prevents premature convergence to deterministic decomposition patterns, preserving the diversity needed to discover solver-tractable alternative paths.
SAD consistently outperforms the solver-blind baseline across both domains and evaluation settings. All SAD vs. solver-blind differences are statistically significant (paired t-test, p < 0.05). SAD also improves over ExeDec in both domains. The relative advantage over solver-blind is larger under length generalization than in-distribution: 22.2% vs. 10.7% on Deepcoder, and 14.0% vs. 10.9% on Lambdabeam.
Three methods are compared. ExeDec: GT-subtask-trained synthesizer, GT-supervised decomposer. Solver-blind: full-task-trained synthesizer, GT-supervised decomposer (ExeDec with SAD's synthesizer). SAD: full-task-trained synthesizer, GT supervision plus solver-aware SCST. All causal claims rest on the SAD vs. solver-blind comparison, which shares architecture, synthesizer weights, search configuration and training data.
A key finding is that higher GT decomposition alignment does not translate into synthesis success. Measured single-step under teacher forcing, SAD achieves consistently higher synthesis accuracy despite matching GT subgoals 2–3× less often than the solver-blind baseline - confirming that GT alignment is a poor proxy for solver utility.
| Domain | Method | Decomp. Acc. (in-dist.) | Decomp. Acc. (len. gen.) | Synth. Acc. (in-dist.) | Synth. Acc. (len. gen.) |
|---|---|---|---|---|---|
| Deepcoder | SAD | 31.7 ± 0.7 | 21.5 ± 0.5 | 87.2 ± 1.3 | 79.8 ± 1.1 |
| Solver-blind | 79.2 ± 0.4 | 63.3 ± 0.6 | 73.0 ± 1.2 | 64.3 ± 0.8 | |
| Lambdabeam | SAD | 33.7 ± 0.3 | 21.4 ± 0.3 | 61.9 ± 1.0 | 49.0 ± 1.2 |
| Solver-blind | 69.9 ± 0.7 | 48.5 ± 0.7 | 54.2 ± 0.5 | 41.3 ± 0.5 |
The performance gap grows with program length despite SAD being trained on single-step tasks only. Solver alignment compounds across decomposition steps.
Beam oracle gains are below 2% in all settings, and the solver-blind beam oracle stays below SAD's raw performance - the gap is generative, not a ranking problem.
Where decomposition order is structurally fixed and ambiguity is absent, SAD matches the solver-blind baseline (94.1% / 90.8% for both, in-dist. / length gen.) - a designed falsifiability check that confirms the mechanism.
The GT decomposition oracle (GT subgoals at inference, same synthesizer and beam size) remains an approximate ceiling overall - 94.7% / 79.8% on Deepcoder and 89.6% / 51.3% on Lambdabeam (in-dist. / length gen.). Yet SAD solves a consistent subset of tasks the oracle cannot: 63.2 ± 6.7 on Deepcoder and 109.8 ± 18.3 on Lambdabeam (out of 2 × 1000 tasks per seed). These are genuinely alternative programs - fewer than 2% match the GT program, and they differ systematically in length and DSL primitive usage. GT decompositions are not universally optimal for a bounded synthesizer.
Without retraining, the Lambdabeam-trained SAD model solves 42.3% ± 7.1% of 129 tasks from the external list-processing benchmark of Rule et al., against 33.0% ± 3.5% for solver-blind.
With a LoRA-fine-tuned Llama-3.1-8B as decomposer and frozen synthesizer on 200 Deepcoder tasks, SAD reaches 34.5% vs. 30.5% for an equal-budget solver-blind control (start: 28.0%). Single run.
Removing supervision collapses decomposition accuracy to 2–9% and test task accuracy below 20%. Lsup keeps the policy in a meaningful decomposition space; LRL navigates within it.
Three standard PBE domains, chosen to vary the key structural property: the degree of valid decomposition ambiguity available for solver-aware training to exploit.
Integer list transformations via a DSL of first- and higher-order functions. Intermediate outputs accumulate as named variables - multiple valid programs and decompositions exist per task, making solver preferences over this ambiguity non-trivial.
Extends Deepcoder with dynamically constructed lambda functions and a conditional If-operation. A larger, less constrained search space amplifies the cost of solver misalignment at every step.
String transformations with a residual state update that structurally fixes decomposition order. Any deviation from the correct sequential prefix propagates failure irrecoverably - designed to produce a null result that validates the causal claim.
All models share the same Transformer architecture (3 layers, embedding dim. 512, hidden dim. 1024), beam size 10, 5 random seeds, 1 000 test tasks per seed, paired t-tests at the 5% level. Each domain is evaluated in-distribution and under length generalization (list domains: train on lengths 1–4, test on length 5; Robustfill: train on 1–6, test on 7–10). A leave-one-out protocol holds out one I/O example for evaluation; step limits are T = 10 for list domains and T = 20 for Robustfill. Lambdabeam-trained models are additionally evaluated zero-shot on 129 tasks from the Rule et al. list-processing benchmark. Training on an NVIDIA RTX A6000; SAD adds ~30% wall-clock time over solver-blind training due to two additional frozen synthesizer forward passes per update step.
A training framework combining supervised GT subgoal imitation as a structural scaffold with SCST using direct feedback from a frozen synthesizer. The reward - synthesizer cross-entropy against the GT program - provides a dense signal that steers decompositions toward the solver's tractable distribution.
Empirical demonstration that higher GT decomposition alignment does not translate into synthesis success. SAD achieves higher synthesis and task accuracy in every setting despite matching GT subgoals 2–3× less often - and solves tasks that a GT decomposition oracle cannot.
A conceptual reframing with implications beyond PBE: any system that learns intermediate representations independently of the bounded component that executes them faces the same structural misalignment. Closing the feedback loop is a general strategy for this class of problem.
Published at the 40th Conference on Neural Information Processing Systems (NeurIPS 2026), Sydney. If you find this work useful, please cite: