From Provable Correctness to Probabilistic Generation

📄 Abstract

Program synthesis, the automated generation of executable code from high-level specifications, has long stood as a central goal in computer science. This thesis presents a comprehensive comparative literature review of the five major paradigms that have shaped the field:

• Logic-Based (Deductive) Synthesis — Formal proofs and theorem proving
• Inductive (Example-Based) Synthesis — Learning from input-output examples
• Sketch & Schema-Based Synthesis — Human-guided program completion
• LLM-Based Synthesis — Large language model approaches
• Neuro-Symbolic (Hybrid) Synthesis — Combining neural and symbolic methods

The review outlines each paradigm's motivations, mechanisms, seminal systems, and fundamental trade-offs— ultimately showcasing the transition from formal methods to statistical models and the ongoing quest to balance correctness guarantees with accessibility.