Program Synthesis

Program synthesis is the task of automatically constructing a program that satisfies a specification expressed at a higher level than the code itself: a logical formula, a set of input-output examples, a partial program with holes, or a natural language description. Where a compiler translates one complete program into another, a synthesizer must search a space of candidate programs for one that meets the specification, and in the classical formulations it must also demonstrate that the result actually meets it. The problem is one of the oldest in computer science and artificial intelligence, dating back to work on extracting programs from theorem-prover proofs in 1969 ^[1].

The field spans several distinct traditions that differ mainly in what counts as a specification and what counts as evidence of correctness. Deductive synthesis derives programs from formal specifications by logical inference, so the output is correct by construction ^[2]. Inductive synthesis, including programming by example (PBE), generalizes from examples of desired behavior; its best-known product is the Flash Fill feature that has shipped in Microsoft Excel since 2013 ^[5][6]. Syntax-guided synthesis (SyGuS) standardized the problem of searching a grammar-restricted space of expressions against a logical constraint, and ran annual solver competitions from 2014 to 2019 ^[8][9]. Neural program synthesis brought learned models into the search, and since 2021 large language models trained on code have absorbed most of the practical demand under the looser banner of code generation ^[15].

Program synthesis is not the same thing as code completion. Completion systems predict likely continuations of existing code (or fill gaps in it, as in fill-in-the-middle training) with no requirement beyond plausibility. A synthesizer is accountable to a specification: the produced program must pass the examples, satisfy the formula, or clear the tests. Modern LLM coding systems sit between the two poles, and the most capable ones, from AlphaCode onward, recover classic synthesis structure by generating many candidates and filtering them against executable checks ^[17].

Specifications and problem variants

What the user supplies determines both the search problem and the guarantee the synthesizer can offer.

Scroll sideways for more →

Example-based and natural language specifications are inherently ambiguous: many programs fit a handful of examples, and most of them are wrong on unseen inputs. Practical PBE systems therefore rank candidates, preferring smaller and more general programs, and interactive systems let the user add examples until the intended behavior is pinned down ^[10].

Deductive synthesis

The earliest line of work treated synthesis as theorem proving. Cordell Green's 1969 paper showed that a resolution theorem prover could return a program as a side effect of answering a query, by tracking the terms used to establish that an output exists ^[1]. Zohar Manna and Richard Waldinger's 1980 paper "A Deductive Approach to Program Synthesis" made this systematic: to synthesize a function, one proves a theorem stating that for every input there exists an output satisfying the specification, in a proof system designed so that a program can be extracted from the proof, with mathematical induction in the proof giving rise to recursion in the program ^[2]. Because the program falls out of a proof, it is correct by construction, which remains the gold standard of the field.

A separate deductive tradition, reactive synthesis, targets systems that run forever and interact with an environment, such as controllers and protocols. Amir Pnueli and Roni Rosner's 1989 work formulated synthesis of a reactive module from a temporal logic specification and established its complexity ^[3]. The shared limitation of the deductive tradition is its input: writing a complete formal specification is often as hard as writing the program, which restricted these methods to domains where the specification is genuinely simpler than the implementation.

Inductive synthesis and programming by example

Inductive synthesis flips the burden: instead of a full specification, the user gives examples, and the synthesizer generalizes. Armando Solar-Lezama and colleagues' Sketch system (2006) developed an influential middle path called sketching, where the programmer writes a partial program with holes and a solver fills the holes so that the whole satisfies a correctness condition ^[4]. The accompanying algorithm, counterexample-guided inductive synthesis (CEGIS), alternates between an inductive synthesizer that proposes a candidate consistent with the examples seen so far and a verifier that either accepts the candidate or returns a counterexample to add to the example set ^[4]. CEGIS became the workhorse loop of the entire field, and it is the clearest illustration of how synthesis and verification are coupled: every CEGIS synthesizer contains a verifier.

The commercial breakthrough for PBE came from Sumit Gulwani's POPL 2011 paper "Automating String Processing in Spreadsheets Using Input-Output Examples," which defined a small language of string transformations (restricted regular expressions, conditionals, and loops) and an algorithm that synthesizes programs in it from one or two examples ^[5]. The technique shipped as Flash Fill in Excel 2013, released in January 2013: a user types the desired output for a row or two, and Excel synthesizes a transformation and applies it down the column ^[6]. The paper later received the Most Influential POPL Paper Award ^[5]. Microsoft generalized the approach into the PROSE SDK, whose synthesis engines also back features in Power Query, Azure data tools, and PowerShell's ConvertFrom-String cmdlet ^[7]. Flash Fill remains the most widely deployed program synthesizer ever shipped, and it reaches users who never see the synthesized program at all.

Syntax-guided synthesis

By 2013 many synthesis tools shared the same underlying shape, and a group of ten researchers including Rajeev Alur, Rastislav Bodik, Sanjit Seshia, Solar-Lezama, and Emina Torlak proposed syntax-guided synthesis as a common formulation: find an expression that satisfies a semantic constraint given as a formula in an SMT theory, drawn from a syntactic space of candidate expressions described by a grammar ^[8]. The grammar does double duty, shrinking the search space and forcing the output into a shape the user finds acceptable. The paper compared three solver families that still organize the field: enumerative search, constraint-based (symbolic) solving, and stochastic search ^[8].

The standardized format enabled competition. The first SyGuS-Comp ran in July 2014 at the FLoC Olympic Games in Vienna with five solvers on a single track; the competition ran annually through 2019, by then with five tracks covering settings such as programming by example and invariant synthesis ^[9]. Sketching, SyGuS, and solver-aided languages such as Torlak and Bodik's Rosette, which extends Racket so that verification and synthesis queries against an interpreter compile down to SMT solving, made synthesis a reusable component inside larger programming tools rather than a bespoke research artifact ^[24]. Gulwani, Oleksandr Polozov, and Rishabh Singh's 2017 survey "Program Synthesis" summarizes this pre-neural state of the art ^[10].

Neural program synthesis

Around 2016 researchers began using neural networks to guide or replace symbolic search. DeepCoder (Balog et al., ICLR 2017) trained a network to predict, from input-output examples, which operations the target program likely contains, and used the predictions to prioritize enumerative and SMT-based search, reporting order-of-magnitude speedups over unaugmented baselines on problems comparable to the easiest competitive programming exercises ^[11]. RobustFill (Devlin et al., ICML 2017) went further and generated programs directly with an attention-based sequence model in the Flash Fill string-processing domain, reaching 92 percent accuracy on a real-world test set where the best prior neural approach scored 34 percent, and, unlike hand-engineered rule systems, it kept working when the examples contained typos ^[12]. Execution-guided neural synthesis (Chen, Liu, and Song, ICLR 2019) improved direct generation by executing partial programs and conditioning the decoder on the resulting intermediate states rather than on program text alone ^[13], an idea that recurs in later systems.

DreamCoder (Ellis et al., published at PLDI 2021) closed the loop between learning and library building: a wake-sleep algorithm alternates between solving synthesis tasks, compressing recurring solution fragments into new reusable library components, and retraining a neural recognition model that guides search, allowing the system to bootstrap concepts across domains including list processing and graphics programs ^[14]. This neurosymbolic line kept the guarantees of search over a discrete program space while using learning to make the search tractable.

AlphaCode and competitive programming

Google DeepMind's AlphaCode was the first system to reach a competitive level on open-ended programming contest problems, which require reading a natural language problem statement and inventing an algorithm, not just implementing a described function. The system, described in a February 2022 preprint and published in Science on December 8, 2022, combined a transformer model trained on competitive programming data with search at scale: it sampled an enormous number of candidate programs per problem, filtered them against the example tests in the problem statement, clustered the survivors by runtime behavior, and submitted up to ten candidates ^[17][18]. Evaluated on ten recent Codeforces contests, AlphaCode achieved an average ranking in the top 54.3 percent of contestants in competitions with more than 5,000 participants, roughly the level of the median competitor; across the dataset it was evaluated on, it solved about 34 percent of problems ^[17][18]. Codeforces founder Mike Mirzayanov said that "AlphaCode managed to perform at the level of a promising new competitor" ^[18]. DeepMind also released the CodeContests training and evaluation dataset ^[18].

AlphaCode 2, announced in a December 6, 2023 technical report, rebuilt the system on fine-tuned Gemini Pro models. Generating up to a million samples per problem and submitting at most ten, it solved 43 percent of 77 problems drawn from 12 recent Codeforces contests, versus 25 percent for the original AlphaCode on the same setup, which DeepMind estimated as performing better than 85 percent of contest participants ^[19]. The AlphaCode recipe (massive sampling, execution-based filtering, clustering, reranking) is generate-and-test synthesis at industrial scale, with the problem's tests standing in for a specification.

The LLM era: code generation as pragmatic synthesis

OpenAI's Codex, described in the July 2021 paper "Evaluating Large Language Models Trained on Code," was a GPT model fine-tuned on public GitHub code that generated Python functions from docstrings ^[15]. The paper introduced HumanEval, a benchmark of 164 hand-written programming problems with unit tests ^[15][16]. Codex solved 28.8 percent of the problems with a single sample per problem, while GPT-3 solved none; when the model generated 100 samples per problem, at least one sample solved 70.2 percent of the problems, an early sign that sampling plus test-based selection was the practical path ^[15]. A production version of Codex powered GitHub Copilot ^[15]. See OpenAI Codex for the model family's later history.

The center of gravity then moved from function-level puzzles to real software work. SWE-bench (Jimenez et al., ICLR 2024) collected 2,294 real GitHub issues from 12 popular Python repositories and asked models to produce repository-level patches; at release in October 2023, the best model evaluated, Claude 2, resolved just 1.96 percent of issues ^[20]. SWE-bench Verified, a 500-instance subset confirmed solvable by human software engineers, followed in August 2024 in collaboration with OpenAI ^[21], and SWE-bench Multimodal, 617 tasks from JavaScript libraries in which each issue includes at least one image, followed in October 2024 ^[25]. Scores on these benchmarks became the standard progress measure for coding agents such as SWE-agent and the generation of tools it inspired.

Whether LLM code generation counts as program synthesis is partly a definitional argument. The specification (a natural language issue or docstring plus some tests) is informal and incomplete, and the model offers no guarantee beyond passing the checks it was given. But the systems that perform best lean on exactly the machinery the synthesis community developed: candidate generation over a search space, execution against tests as a weak verifier, and iterative refinement from counterexamples, which is CEGIS with the roles played by a language model and a test harness. In practice, LLMs became the pragmatic successor to classical synthesis for general-purpose programming because they accept the specifications people actually write, while classical methods survive where their strengths matter: tiny ambiguous specs (Flash Fill's two examples) or hard correctness requirements.

Verification-coupled synthesis

The deductive tradition's promise, programs correct by construction, did not disappear; it moved into the loop. CEGIS-style architectures embed a verifier directly in synthesis ^[4], SyGuS solvers certify their output against the semantic constraint ^[8], and solver-aided languages like Rosette make verification and synthesis two queries against the same SMT encoding ^[24]. On the neural side, the AlphaCode line substitutes executable tests for a verifier ^[17][19], which is sound only as far as the tests reach. Bridging LLM generation and formal guarantees, for instance by generating code together with proofs checkable in systems such as Lean or by pairing generation with automated theorem proving, is an active research direction, and the tradeoff it targets is the field's oldest one: specifications strong enough to guarantee correctness are expensive, and specifications cheap enough to write leave the synthesizer room to be wrong.

Recent developments

In September 2025, an advanced version of Gemini 2.5 Deep Think achieved gold-medal-level performance at the ICPC World Finals in Baku, Azerbaijan (held September 4, 2025), solving 10 of 12 problems under the five-hour contest constraints, a total that would have ranked second among the 139 university teams; it also solved one problem that no university team at the contest solved ^[22]. The human champion, a St. Petersburg State University team, solved 11 of 12 ^[23]. Contest performance that AlphaCode approximated at the median-competitor level in 2022 ^[18] had moved to the top of the field within three years, and evaluation attention shifted further toward contamination-resistant and realistic settings such as LiveCodeBench and the SWE-bench family ^[21].

Scroll sideways for more →

See also

• AlphaCode
• OpenAI Codex
• SWE-bench
• HumanEval
• Automated theorem proving
• AlphaEvolve

References

1. ^C. Cordell Green. "Application of Theorem Proving to Problem Solving." IJCAI 1969, pp. 219-240. dblp.org/...Green69
2. ^Zohar Manna and Richard Waldinger. "A Deductive Approach to Program Synthesis." ACM Transactions on Programming Languages and Systems 2(1), 1980, pp. 90-121. doi.org/...357084.357090
3. ^Amir Pnueli and Roni Rosner. "On the Synthesis of a Reactive Module." POPL 1989, pp. 179-190. doi.org/...75277.75293
4. ^Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit A. Seshia, and Vijay Saraswat. "Combinatorial Sketching for Finite Programs." ASPLOS 2006, pp. 404-415. doi.org/...1168857.1168907
5. ^Sumit Gulwani. "Automating String Processing in Spreadsheets Using Input-Output Examples." POPL 2011. Microsoft Research publication page. microsoft.com/...heets-using-input-output-examples
6. ^Microsoft Research Blog. "Flash Fill Gives Excel a Smart Charge." 2013. microsoft.com/...h-fill-gives-excel-a-smart-charge
7. ^Microsoft Research. "PROSE" group page. microsoft.com/...prose
8. ^Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. "Syntax-Guided Synthesis." FMCAD 2013, pp. 1-8. cis.upenn.edu/...SyGuS13.pdf
9. ^SyGuS Organization. "Competitions" (SyGuS-Comp 2014-2019). sygus-org.github.io/comp
10. ^Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. "Program Synthesis." Foundations and Trends in Programming Languages 4(1-2), 2017, pp. 1-119. doi.org/...2500000010
11. ^Matej Balog, Alexander L. Gaunt, Marc Brockschmidt, Sebastian Nowozin, and Daniel Tarlow. "DeepCoder: Learning to Write Programs." ICLR 2017. arxiv.org/...1611.01989
12. ^Jacob Devlin, Jonathan Uesato, Surya Bhupatiraju, Rishabh Singh, Abdel-rahman Mohamed, and Pushmeet Kohli. "RobustFill: Neural Program Learning under Noisy I/O." ICML 2017, PMLR 70, pp. 990-998. proceedings.mlr.press/...devlin17a
13. ^Xinyun Chen, Chang Liu, and Dawn Song. "Execution-Guided Neural Program Synthesis." ICLR 2019. dblp.org/...ChenLS19
14. ^Kevin Ellis, Catherine Wong, Maxwell Nye, Mathias Sable-Meyer, Luc Cary, Lucas Morales, Luke Hewitt, Armando Solar-Lezama, and Joshua B. Tenenbaum. "DreamCoder: Growing Generalizable, Interpretable Knowledge with Wake-Sleep Bayesian Program Learning." arXiv, June 2020; published at PLDI 2021. arxiv.org/...2006.08381
15. ^Mark Chen, Jerry Tworek, Heewoo Jun, et al. "Evaluating Large Language Models Trained on Code." arXiv, July 2021. arxiv.org/...2107.03374
16. ^OpenAI. "openai_humaneval" dataset card (164 problems). Hugging Face. huggingface.co/...openai_humaneval
17. ^Yujia Li, David Choi, Junyoung Chung, et al. "Competition-Level Code Generation with AlphaCode." arXiv, February 2022; Science, December 8, 2022. arxiv.org/...2203.07814
18. ^Google DeepMind. "Competitive programming with AlphaCode." Blog post, December 2022. deepmind.google/...tive-programming-with-alphacode
19. ^AlphaCode Team, Google DeepMind. "AlphaCode 2 Technical Report." December 6, 2023. storage.googleapis.com/...AlphaCode2_Tech_Report.pdf
20. ^Carlos E. Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik Narasimhan. "SWE-bench: Can Language Models Resolve Real-World GitHub Issues?" ICLR 2024. arxiv.org/...2310.06770
21. ^SWE-bench GitHub repository (SWE-bench Verified and Multimodal announcements). github.com/...SWE-bench
22. ^Google DeepMind. "Gemini achieves gold-level performance at the International Collegiate Programming Contest World Finals." September 17, 2025. deepmind.google/...rogramming-contest-world-finals
23. ^Wikipedia. "International Collegiate Programming Contest" (2025 World Finals results). en.wikipedia.org/...Collegiate_Programming_Contest
24. ^Emina Torlak and Rastislav Bodik. "Growing Solver-Aided Languages with Rosette." Onward! 2013. Project site: emina.github.io/rosette
25. ^John Yang, Carlos E. Jimenez, Alex L. Zhang, et al. "SWE-bench Multimodal: Do AI Systems Generalize to Visual Software Domains?" arXiv, October 2024. arxiv.org/...2410.03859