UC Santa Barbara

Program synthesis has found its unique position in automated programming for both end-users and developers; it is changing the way that users code. Recent advances in deep learning and computer-aided reasoning for program synthesis have greatly pushed both techniques for an open range of domains, e.g., data analysis, high-performance computing, design and reasoning of complex systems, web3 security and science. While algorithms from these two paradigms may place different assumptions of the problem (e.g., modality of specification) and guarantees for the result (e.g., completeness), it is usually difficult for users to benefit simultaneously from both. In fact, feedback generated by statistical and logical reasoning algorithms are usually found useful for each other, but they are seldom integrated in a seamless way for program synthesis due to the aforementioned difference.

Motivated by these challenges, this dissertation presents a program synthesis framework that unifies the two paradigms of statistical and logical reasoning. Specifically, we address this problem by three aspects. We first describe a unified \emph{interface} that encodes user-provided specification from multi-modalities into machine-readable constraints by a hybrid approach of reasoning. The framework's \emph{core} infrastructure is then powered by deduction-guided reinforcement learning, a novel approach that seamlessly incorporated feedback from logical reasoning into statistical models. We further demonstrate the \emph{extent} of the framework by a derived system for reasoning and refinement of deep learning model's predictions.

We implement the proposed techniques in research prototypes, whose effectiveness is confirmed by a set of extensive evaluations. Our proposed framework also brings improvements for end-user programming via broaden expressiveness, enhanced explainability and natural interactivity.