# Semantics-Guided Synthesis

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 22 Aug 2020.

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

- [SEVerA: Verified Synthesis of Self-Evolving Agents](https://mlsanity.com/paper/2603.25111/) (2026)
- [Modelling Program Spaces in Program Synthesis with Constraints](https://mlsanity.com/paper/2508.00005/) (2025)
- [Herb.jl: A Unifying Program Synthesis Library](https://mlsanity.com/paper/2510.09726/) (2025)
- [Program Synthesis as Dependency Quantified Formula Modulo Theory](https://mlsanity.com/paper/2105.09221/) (2021)
- [Learning the Error Patterns of Language Models](https://mlsanity.com/paper/2605.28328/) (2026)

## Abstract (arXiv)

This paper develops a new framework for program synthesis, called semantics-guided synthesis (SemGuS), that allows a user to provide both the syntax and the semantics for the constructs in the language. SemGuS accepts a recursively defined big-step semantics, which allows it, for example, to be used to specify and solve synthesis problems over an imperative programming language that may contain loops with unbounded behavior. The customizable nature of SemGuS also allows synthesis problems to be defined over a non-standard semantics, such as an abstract semantics. In addition to the SemGuS framework, we develop an algorithm for solving SemGuS problems that is capable of both synthesizing programs and proving unrealizability, by encoding a SemGuS problem as a proof search over Constrained Horn Clauses: in particular, our approach is the first that we are aware of that can prove unrealizabilty for synthesis problems that involve imperative programs with unbounded loops, over an infinite syntactic search space. We implemented the technique in a tool called MESSY, and applied it to both SyGuS problems(i.e., over expressions) and synthesis problems over an imperative programming language.