From Provable Correctness to Probabilistic Generation: A Comparative Review of Program Synthesis Paradigms

TL;DR

This paper reviews the evolution of program synthesis from logic-based methods to neural and hybrid approaches, analyzing their principles, systems, and trade-offs to guide future research.

Contribution

It provides a comprehensive comparison of five main paradigms in program synthesis, highlighting their foundations, advancements, and challenges, especially the shift towards neuro-symbolic hybrid models.

Findings

Logic-based synthesis offers formal correctness guarantees.

Neural models enable natural language code generation.

Hybrid approaches aim to combine reliability with scalability.

Abstract

Program synthesis--the automated generation of executable code from high-level specifications--has been a central goal of computer science for over fifty years. This thesis provides a comparative literature review of the main paradigms that have shaped the field, tracing its evolution from formal logic based methods to recent advances using large scale neural models. We examine five key approaches: logic based (deductive) synthesis, inductive (example based) synthesis, sketch/schema based synthesis, large language model based synthesis, and neuro-symbolic hybrids. For each, we analyze foundational principles, notable systems, and practical applications, highlighting trade offs between correctness guarantees, specification requirements, search complexity, and expressive power. By reviewing developments from formally verified synthesis tools such as KIDS and Coq to data driven models generating probabilistic code from natural language like Codex, we present a comprehensive narrative of progress and ongoing challenges. This work emphasizes the transition from symbolic to hybrid neuro-symbolic methods and outlines future directions for reliable and scalable program synthesis.