GPU accelerated program synthesis: Enumerate semantics, not syntax!
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.
Code (0)
등록된 구현이 없습니다.
Tasks
CPUGPUProgram SynthesisSimilar Papers 제목 키워드 기반
Write, Execute, Assess: Program Synthesis with a REPL
We present a neural program synthesis approach integrating components which write, execute, and assess code to navigate the search space of possible programs. We equip the search process with an interpreter or a read-eva…
NavigateProgram SynthesisDynamic Neural Program Embeddings for Program Repair
Neural program embeddings have shown much promise recently for a variety of program analysis tasks, including program synthesis, program repair, code completion, and fault localization. However, most existing program emb…
Code CompletionFault localizationProgram RepairProgram SynthesisSemRegex: A Semantics-Based Approach for Generating Regular Expressions from Natural Language Specifications
Recent research proposes syntax-based approaches to address the problem of generating programs from natural language specifications. These approaches typically train a sequence-to-sequence learning model using a syntax-b…
Program SynthesisLatent Execution for Neural Program Synthesis
Program synthesis from input-output (IO) examples has been a long-standing challenge. While recent works demonstrated limited success on domain-specific languages (DSL), it remains highly challenging to apply them to rea…
C++ codeProgram SynthesisLatent Execution for Neural Program Synthesis Beyond Domain-Specific Languages
Program synthesis from input-output (IO) examples has been a long-standing challenge. While recent works demonstrated limited success on domain-specific languages (DSL), it remains highly challenging to apply them to rea…
C++ codeProgram Synthesis