Modelling Program Spaces in Program Synthesis with Constraints
This work addresses the combinatorial search problem in program synthesis for researchers and practitioners, offering an incremental improvement over existing constraint-based methods.
The paper tackles the challenge of taming large program spaces in program synthesis by using syntactic constraints to model program spaces, defining both feasible and likely useful solutions. They introduce BART, a solver that efficiently propagates and solves these constraints, eliminating up to 99% of the program space and significantly reducing enumeration time.
A core challenge in program synthesis is taming the large space of possible programs. Since program synthesis is essentially a combinatorial search, the community has sought to leverage powerful combinatorial constraint solvers. Here, constraints are used to express the program semantics, but not as a potentially potent tool to remove unwanted programs. Recent inductive logic programming approaches introduce constraints on the program's syntax to be synthesized. These syntactic constraints allow for checking and propagating a constraint without executing the program, and thus for arbitrary operators. In this work, we leverage syntactic constraints to model program spaces, defining not just solutions that are feasible, but also ones that are likely useful. To demonstrate this idea, we introduce BART, a solver that efficiently propagates and solves these constraints. We evaluate BART on program space enumeration tasks, finding that the constraints eliminate up to 99 percent of the program space, and that modeling program spaces significantly reduces enumeration time.