Programming-By-Example by Programming-By-Example: Synthesis of Looping Programs

TL;DR

This paper presents a multi-phase algorithm for synthesizing recursive looping programs within the SyGuS framework, enabling the generation of recursive functions from examples.

Contribution

It introduces a modular, solver-agnostic approach for synthesizing recursive programs in SyGuS, addressing a gap in existing solvers.

Findings

Supports recursive program synthesis in SyGuS

Modular approach compatible with any SyGuS solver

Enables synthesis of looplike recursive functions from examples

Abstract

Program synthesis has seen many new applications in recent years, in large part thanks to the introduction of SyGuS. However, no existing SyGuS solvers have support for synthesizing recursive functions. We introduce an multi-phase algorithm for the synthesis of recursive ``looplike'' programs in SyGuS for programming-by-example. We solve constraints individually and treat them as ``unrolled`` examples of how a recursive program would behave, and solve for the generalized recursive solution. Our approach is modular and supports any SyGuS Solver.