用语义枚举替代语法枚举，让程序合成在GPU上快得多。
GPU accelerated program synthesis: Enumerate semantics, not syntax!
- 改用公式语义而非语法进行枚举，减少数据移动和分支依赖。
- 在正负例迹上合成逻辑公式，速度远超之前的CPU方法。
- 适合做形式化方法优化的工程师和研究者参考。
程序合成是根据规范生成程序或逻辑公式的统称。随着GPU在深度学习中表现出显著性能提升，一个自然的问题浮现：能否将基于搜索的程序合成器部署在GPU上，实现类似加速？本文基于近期工作探讨此问题，目标是构建一个运行于GPU上的合成器，输入正负例迹，输出接受正例、拒绝负例的逻辑公式。通过采用对GPU友好的编程技术——利用公式的语义来最小化数据移动并减少数据依赖分支，该合成器可扩展至更大规模的合成问题，且运行速度远超此前基于CPU的最先进方法。我们认为，使该方法适应GPU的洞察，有望广泛提升其他形式化方法工作负载的性能。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。