# GPU accelerated program synthesis: Enumerate semantics, not syntax!

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 3 of its 25 references that are in the map.
- First posted on arXiv 26 Apr 2025.

## Builds on (most cited first, 3 of 3)

- [Search-Based Regular Expression Inference on a GPU](https://mlsanity.com/paper/2305.18575/) (2023)
- [LTL learning on GPUs](https://mlsanity.com/paper/2402.12373/) (2024)
- [Parallel Weighted Model Counting with Tensor Networks](https://mlsanity.com/paper/2006.15512/) (2020)

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

- [GPU-Accelerated Synthesis of Mixed-Boolean Arithmetic: Beyond Caching](https://mlsanity.com/paper/2605.08243/) (2026)

## Abstract (arXiv)

Program synthesis is an umbrella term for generating programs and logical formulae from specifications. With the remarkable performance improvements that GPUs enable for deep learning, a natural question arose: can we also implement a search-based program synthesiser on GPUs to achieve similar performance improvements? In this article we discuss our insights on this question, based on recent works~. The goal is to build a synthesiser running on GPUs which takes as input positive and negative example traces and returns a logical formula accepting the positive and rejecting the negative traces. With GPU-friendly programming techniques -- using the semantics of formulae to minimise data movement and reduce data-dependent branching -- our synthesiser scales to significantly larger synthesis problems, and operates much faster than the previous CPU-based state-of-the-art. We believe the insights that make our approach GPU-friendly have wide potential for enhancing the performance of other formal methods (FM) workloads.