GPU accelerated program synthesis: Enumerate semantics, not syntax!
This work addresses the performance bottleneck in program synthesis for formal methods, offering a GPU-accelerated approach that is incremental but enables broader scalability.
The authors tackled the problem of accelerating program synthesis by implementing a GPU-based search synthesizer that uses semantics to minimize data movement and branching, achieving significantly faster performance and scaling to larger problems than the previous CPU-based state-of-the-art.
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.