Automated Functional Synthesis: An Ideal Meeting Ground for Symbolic Reasoning and Machine Learning

In this talk, I will focus on one of the most fundamental problems in computer science: functional synthesis, which seeks to synthesize a system from a given relational specification. The synthesis problem is as old as propositional logic, tracing its origins to Boole’s seminal work in the 1850’s. Despite decades of work, scalability remains the fundamental challenge in functional synthesis. I will discuss a new data-driven approach, Manthan, that combines the power of machine learning with symbolic reasoning to achieve dramatic improvements in scalability. In particular, Manthan views functional synthesis as a classification problem, relies on advances in constrained sampling for data generation, and advances in automated reasoning for a novel proof-guided refinement and provable verification. The significant performance improvements call for interesting future work at the intersection of machine learning and symbolic reasoning.