프로그래밍-바이-예제를 위한 솔버 기반 분해 방법: 분할은 어떻게 정복해야 하는지를 알아야 할 때

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

분해 기반 프로그래밍-바이-예제(PBE)는 학습된 합성기(synthesizer)가 해결하는 하위 작업으로 작업을 분할하여 성능을 향상시킵니다. 분해기는 중간 하위 목표를 예측하고, 합성기는 이러한 하위 목표에 따라 프로그램을 생성합니다. 현재의 접근 방식은 분해기를 실제(ground-truth, GT) 하위 목표를 모방하도록 훈련하며, 이는 분해 품질이 작업 자체의 고유한 특성이라는 전제를 암시적으로 가지고 있습니다. 우리는 이 가정을 비판적으로 검토합니다. 특정 유도 편향을 가진 제한된 솔버의 경우, GT 분해는 주석 작성자의 인수 방식(factorization choices)이지, 솔버의 탐색 과정을 반영하는 것이 아닙니다. 따라서 GT 분해를 모방하도록 훈련된 분해기는 논리적으로 타당하지만 솔버가 해결하기 어려운 하위 목표를 제안할 수 있습니다. 우리는 솔버 인지 분해(Solver-Aware Decomposition, SAD)라는 새로운 훈련 프레임워크를 제안합니다. SAD는 GT 하위 목표에 대한 지도 학습을 구조적인 기반으로 유지하면서, 동시에 고정된 합성기로부터 직접적인 피드백을 받아 분해기를 최적화합니다. 하위 목표는 대상 프로그램에 대한 합성기의 손실 값을 기준으로 보상받습니다. 이는 하위 작업의 난이도를 나타내는 신호이며, 솔버가 실행할 수 있는 분해를 장려합니다. 우리의 실험 결과는 정확도의 역설을 보여줍니다: GT 분해와의 높은 일치성은 합성 성공률을 향상시키지 않습니다. 이는 합성기가 동일한 GT 데이터를 사용하여 훈련되었음에도 불구하고, 분해기가 모방하도록 최적화되기 때문입니다. SAD는 GT 정렬(alignment)보다 솔버의 처리 가능성을 중시하는 분해를 학습하여, 두 가지 PBE 영역에서 합성 및 전체 작업 정확도 측면에서 일관된 성능 향상을 가져옵니다. 또한, SAD는 GT 분해가 실패하는 작업을 해결합니다. 이는 GT 분해가 제한된 솔버에게 항상 최적의 방법이 아니며, 분해 품질은 솔버에 상대적이라는 경험적인 증거를 제공합니다.

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.