Recursive Program Synthesis from Sketches and Mixed-Quantifier Properties

TL;DR

This paper introduces a new method for automatically synthesizing recursive programs from complex logical specifications using Skolemization and counterexample-guided techniques, improving efficiency on benchmark problems.

Contribution

It presents a novel synthesis approach that reduces mixed-quantifier logic problems to simpler forms and employs pruning strategies to enhance performance.

Findings

Significant performance improvements with counterexample generalization.

Prophylactic pruning reduces invalid candidate enumeration.

Effective on 42 benchmark problems.

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.