Program synthesis using deduction-guided reinforcement learning. (English) Zbl 1478.68054

Lahiri, Shuvendu Kumar (ed.) et al., Computer aided verification. 32nd international conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12225, 587-610 (2020).
Summary: In this paper, we present a new program synthesis algorithm based on reinforcement learning. Given an initial policy (i.e. statistical model) trained off-line, our method uses this policy to guide its search and gradually improves it by leveraging feedback obtained from a deductive reasoning engine. Specifically, we formulate program synthesis as a reinforcement learning problem and propose a new variant of the policy gradient algorithm that can incorporate feedback from a deduction engine into the underlying statistical model. The benefit of this approach is two-fold: first, it combines the power of deductive and statistical reasoning in a unified framework. Second, it leverages deduction not only to prune the search space but also to guide search. We have implemented the proposed approach in a tool called Concord and experimentally evaluate it on synthesis tasks studied in prior work. Our comparison against several baselines and two existing synthesis tools shows the advantages of our proposed approach. In particular, Concord solves 15% more benchmarks compared to Neo, a state-of-the-art synthesis tool, while improving synthesis time by \(8.71 \times\) on benchmarks that can be solved by both tools.
For the entire collection see [Zbl 1453.68018].


68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68T05 Learning and adaptive systems in artificial intelligence
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Full Text: DOI