1
Recursive Program Synthesis from Sketches and Mixed-Quantifier Properties
arXiv:2601.04045v1 Announce Type: new
Abstract: We present a novel approach to the automatic synthesis of recursive programs from mixed-quantifier first-order logic properties. Our approach uses Skolemization to reduce the mixed-quantifier synthesis problem to a $\forall^*$-synthesis problem, synthesizing witness-generating functions for introduced Skolem symbols alongside the target program. We tackle $\forall^*$-synthesis using a sketching-based, enumerative, counterexample-guided approach. Our algorithm learns syntactic constraints from counterexamples to prune the candidate space and employs a prophylactic pruning technique to avoid enumerating invalid candidates altogether. We evaluate our technique on 42 benchmarks, demonstrating that both counterexample generalization and prophylactic pruning significantly improve performance.
Abstract: We present a novel approach to the automatic synthesis of recursive programs from mixed-quantifier first-order logic properties. Our approach uses Skolemization to reduce the mixed-quantifier synthesis problem to a $\forall^*$-synthesis problem, synthesizing witness-generating functions for introduced Skolem symbols alongside the target program. We tackle $\forall^*$-synthesis using a sketching-based, enumerative, counterexample-guided approach. Our algorithm learns syntactic constraints from counterexamples to prune the candidate space and employs a prophylactic pruning technique to avoid enumerating invalid candidates altogether. We evaluate our technique on 42 benchmarks, demonstrating that both counterexample generalization and prophylactic pruning significantly improve performance.
Anonymous
No comments yet.