# Synthesis through Unification

arXiv: https://arxiv.org/abs/1505.05868 · HTML: https://mlsanity.com/paper/1505.05868/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 21 May 2015.

## Built on by (most cited first, 4 of 4)

- [Multi-modal Program Inference: a Marriage of Pre-trainedLanguage Models and Component-based Synthesis](https://mlsanity.com/paper/2109.02445/) (2021)
- [Learning to Combine Per-Example Solutions for Neural Program Synthesis](https://mlsanity.com/paper/2106.07175/) (2021)
- [Program Skeletons for Automated Program Translation](https://mlsanity.com/paper/2504.07483/) (2025)
- [ObSynth: An Interactive Synthesis System for Generating Object Models from Natural Language Specifications](https://mlsanity.com/paper/2210.11468/) (2022)

## Abstract (arXiv)

Given a specification and a set of candidate programs (program space), the program synthesis problem is to find a candidate program that satisfies the specification. We present the synthesis through unification (STUN) approach, which is an extension of the counter-example guided inductive synthesis (CEGIS) approach. In CEGIS, the synthesizer maintains a subset S of inputs and a candidate program Prog that is correct for S. The synthesizer repeatedly checks if there exists a counter-example input c such that the execution of Prog is incorrect on c. If so, the synthesizer enlarges S to include c, and picks a program from the program space that is correct for the new set S. The STUN approach extends CEGIS with the idea that given a program Prog that is correct for a subset of inputs, the synthesizer can try to find a program Prog' that is correct for the rest of the inputs. If Prog and Prog' can be unified into a program in the program space, then a solution has been found. We present a generic synthesis procedure based on the STUN approach and specialize it for three different domains by providing the appropriate unification operators. We implemented these specializations in prototype tools, and we show that our tools often per- forms significantly better on standard benchmarks than a tool based on a pure CEGIS approach.