Program Synthesis with LLMs

9 min read

Learn

Quick Reading

Estimated 9 mins

Prereq

Intermediate

Basic ML concepts helpful

Interactive

Static Playbook

Static guide & reference tables

From completing code to synthesizing programs that satisfy a spec

Program synthesis is the older, more formal problem that code generation models now tackle informally: automatically constructing a program that satisfies a given specification, whether that spec is a natural-language description, a set of input-output examples, formal pre/post-conditions, or unit tests. Classical program synthesis (pre-LLM) used techniques like constraint solving (SAT/SMT solvers), genetic programming, and combinatorial search over a domain-specific language's grammar — powerful for narrow, well-defined domains (spreadsheet formula synthesis, as in Microsoft's FlashFill) but struggling to scale to general-purpose programming languages with huge search spaces.

LLMs reframed synthesis as conditional generation plus search

Large language models sidestep the combinatorial search problem by treating synthesis as conditional sequence generation: given a specification embedded in the prompt (a docstring, example input-output pairs, failing test cases), generate candidate programs directly, token by token, using patterns learned from billions of lines of training code rather than exhaustive search. Where this falls short on its own, modern systems add a generate-and-test loop on top: sample multiple candidate programs, execute them against available test cases or examples, and either select the first passing candidate or use failures as feedback to iteratively refine the next generation attempt — closing the loop between the LLM's generative prior and the formal correctness guarantee that execution against tests provides.

generate_and_test_synthesis.py

python

def synthesize_with_feedback(llm, spec: str, test_cases: list, max_attempts: int = 5):
    """Iterative program synthesis: generate, execute against tests, and feed
    failures back into the prompt until a passing candidate is found."""
    history = []
    for attempt in range(max_attempts):
        feedback = "\n".join(history[-3:])  # most recent failures only
        prompt = f"{spec}\n\nPrevious attempts and failures:\n{feedback}\n\nWrite a correct Python function:"
        candidate_code = llm.generate(prompt)

        passed, failure_detail = run_against_tests(candidate_code, test_cases)
        if passed:
            return candidate_code, attempt + 1

        history.append(f"Attempt {attempt}: failed on {failure_detail}")

    return None, max_attempts   # synthesis failed within budget

def run_against_tests(code: str, test_cases: list) -> tuple[bool, str]:
    namespace = {}
    exec(code, namespace)           # NOTE: real systems must sandbox this execution
    fn = namespace[list(namespace.keys())[-1]]
    for inp, expected in test_cases:
        if fn(*inp) != expected:
            return False, f"input={inp} expected={expected} got={fn(*inp)}"
    return True, ""

Paradigm	Specification type	Correctness guarantee	Scalability
Classical search/constraint-based	Formal spec, DSL grammar	Provable (within DSL)	Poor for large/general languages
LLM single-shot generation	Natural language / examples	None — just statistically likely	Scales to any language, but unreliable
LLM + generate-and-test loop	Natural language + test cases	Guaranteed against given tests only	Good, but test coverage limits guarantee
Formal verification + LLM-generated proof hints	Formal pre/post-conditions	Provable, strongest guarantee	Narrow domains, heavy tooling

The specification gap: tests are a proxy, not the real goal

A critical, often overlooked issue: passing a given set of tests doesn't mean the synthesized program is actually correct for the intended specification — it means the program satisfies those specific tests, which is a strictly weaker guarantee. A synthesized function can pass every provided example while implementing a subtly wrong general rule (classic overfitting to the visible test cases, structurally the same failure mode as overfitting in supervised learning). This is why benchmarks like HumanEval and MBPP deliberately include held-out hidden tests beyond the ones shown in the prompt — to measure whether the synthesized solution generalizes to the actual intended specification, not just the examples the model saw.

Program synthesis is where neural generation and formal methods are converging

Active research increasingly combines LLM-generated code with formal verification tools — using an LLM to generate both a candidate program and a candidate formal proof of its correctness (or invariants for a verifier like Dafny or Lean to check), getting the best of both worlds: the LLM's broad generative flexibility and the verifier's actual correctness guarantee, rather than relying on test-case coverage as an imperfect proxy for correctness.

Sandboxing isn't optional when executing synthesized code

Any generate-and-test loop that executes LLM-generated code against test cases must run that code in a properly isolated sandbox (no filesystem/network access, resource limits, timeouts) — a synthesized program, whether through model error or in principle adversarial prompt content, can contain arbitrary code, including code that deletes files, makes network calls, or runs indefinitely. Never exec() untrusted generated code directly in a production process, as shown schematically (and flagged) in the example above.

What's Next?

Synthesizing correct programs raises an immediate follow-up question that production systems can't avoid: how do you rigorously measure whether a code-generating model is actually good, beyond a handful of toy benchmark problems?

I build these systems professionally.

Whether it's a RAG pipeline, analytics migration, or AI workflow — let's talk.

Work With Me →