# Counterexample-Driven Synthesis for Probabilistic Program Sketches

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Apr 2019.

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

- [RefineStat: Efficient Exploration for Probabilistic Program Synthesis](https://mlsanity.com/paper/2509.01082/) (2025)
- [Inductive Synthesis for Probabilistic Programs Reaches New Horizons](https://mlsanity.com/paper/2101.12683/) (2021)
- [Probabilistic Counterexample Guidance for Safer Reinforcement Learning (Extended Version)](https://mlsanity.com/paper/2307.04927/) (2023)

## Abstract (arXiv)

Probabilistic programs are key to deal with uncertainty in e.g. controller synthesis. They are typically small but intricate. Their development is complex and error prone requiring quantitative reasoning over a myriad of alternative designs. To mitigate this complexity, we adopt counterexample-guided inductive synthesis (CEGIS) to automatically synthesise finite-state probabilistic programs. Our approach leverages efficient model checking, modern SMT solving, and counterexample generation at program level. Experiments on practically relevant case studies show that design spaces with millions of candidate designs can be fully explored using a few thousand verification queries.