GPU accelerated program synthesis: Enumerate semantics, not syntax!
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866913810039701504 |
|---|---|
| author | Berger, Martin Fijalkow, Nathanaël Valizadeh, Mojtaba |
| author_facet | Berger, Martin Fijalkow, Nathanaël Valizadeh, Mojtaba |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_18943 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | GPU accelerated program synthesis: Enumerate semantics, not syntax! Berger, Martin Fijalkow, Nathanaël Valizadeh, Mojtaba Programming Languages Artificial Intelligence Logic in Computer Science 68 D.3 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. |
| title | GPU accelerated program synthesis: Enumerate semantics, not syntax! |
| topic | Programming Languages Artificial Intelligence Logic in Computer Science 68 D.3 |
| url | https://arxiv.org/abs/2504.18943 |