Research Projects

Program syntheses have significantly impacted recent academic research directions, as well as, assuaged the burden of writing programs from the programmer in the real world. This has been possible through continuous progress, both in more traditional Symbolic program synthesis using ideas from program verification and programming languages, as well as recent developments in Neural program synthesis, using advancement in the Machine Learning techniques. Unfortunately, both these lines of approaches fall severely short of the goal of synthesizing general-purpose, correct programs for complex domains. The \textit{Symbolic} approaches rely fundamentally on precise, and costly formal reasoning, and thus lack scalability to handle the complexity and size of these programs. On the other hand, Neural approaches too have their ill-comings; program synthesis tasks are hard for deep networks that have \textit{no symbolic understanding} of these programs and often are \textit{data hungry}. This is particularly problematic for complex tasks where good training data is limited. Further, neural approaches lack basic functional correctness guarantees for the synthesized programs, due to the black-box nature of these models. This makes them futile programming tasks which are error-prone and where safety is a critical requirement. These observations lead to general inquiry about combining the power of precise reasoning in Symbolic program synthesis with the efficient (but imprecise) generalization of Neural synthesis approaches, leading to the development of the new domain of {\it Neurosymbolic Program Synthesis} or {\it Neurosymbolic Programming.} The idea is that these approaches can mutually aid the other and together they will be able to tackle challenges that are infeasible for either alone. The main goal of this project is to develop novel NeuroSymbolic techniques and tools to address the limitations of both Neural and Symbolic approaches. Towards this goal, the project proposes two main directions; First, it proposes a NeuroSymbolic Network configuration synthesis pipeline that integrates modern, pre-trained LLMs with Formal Verification engines. LLMs allow fast (but mostly imprecise) programs which are then repaired by slow (and correct) Formal verification engines, while each feeding information to the other. Second, it proposes a formal specification inference pipeline that uses richer embeddings for programs (compared to word embedding or control flow graph embeddings) capturing formal semantics (logic) and type systems. This allows enriching ML models (e.g. Seq2Seq models) with a deeper understanding of formal logic and types.