arXiv:2608.03461cs.AI2026-08

让分解器学会适配求解器能力,提升编程范例的生成成功率

Solver-Aware Decompositions for Programming-by-Example: When Dividing Requires Knowing how to Conquer

  • 用求解器反馈直接优化分解器,而非盲目模仿人工标注的分解
  • 在两个任务上显著提升生成成功率,突破人工分解的瓶颈
  • 适合研究程序合成、自动推理与可解释性分解的学者

基于分解的编程范例(PBE)通过将任务拆分为子任务来提升性能:分解器预测中间子目标,合成器据此生成程序。现有方法训练分解器模仿真实(GT)子目标,隐含假设分解质量是任务固有的。我们挑战这一假设:对于具有固定归纳偏置的有限求解器,GT分解反映的是标注者的选择,而非求解器的搜索动态。盲目模仿GT可能导致逻辑正确但求解器无法处理的子目标。本文提出求解器感知分解(SAD),在保留监督训练作为结构基础的同时,引入冻结合成器的直接反馈进行优化。子目标根据合成器在目标程序上的损失获得奖励,该信号反映子任务难度,鼓励求解器可操作的分解。实验揭示准确率悖论:与GT分解的一致性越高,合成成功率反而越低——即使合成器使用相同的GT数据训练。SAD则学习在与GT对齐和求解器可处理性之间权衡,持续提升合成与端到端任务准确率。更重要的是,SAD能解决连GT分解器也无法解决的任务,实证表明GT分解并非对所有求解器最优,分解质量是求解器相关的,而非任务固有。

原文摘要 · Abstract (English)

Decomposition-based Programming-by-example (PBE) scales performance by splitting tasks into subtasks that a learned synthesizer solves: a decomposer predicts intermediate subgoals, and a synthesizer generates programs conditioned on them. Current approaches 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. 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 via direct feedback from a frozen synthesizer. Subgoals are rewarded based on the synthesizer's loss on the target program - a 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. Moreover, SAD solves tasks that a GT decomposition oracle fails - empirical evidence that GT decompositions are not universally optimal for bounded solvers, and that decomposition quality is solver-relative, not intrinsic.

程序合成分解策略求解器感知PBE

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。