CS Talk
Priyanka Golia
Host: Ruzica Piskac
Please contact Ruzica if you would like to meet with the speaker
Title: Functional Synthesis: Formal Methods meets Machine Learning
Abstract:
Given a specification F(X,Y) over the set of input variables X and output variables Y, we want the assistant, aka functional synthesis engine, to design a function G such that (X,Y=G(X)) satisfies F. Functional synthesis has been studied for over 150 years, dating back Boole in 1850’s and yet scalability remains a core challenge. Motivated by progress in machine learning, we design a new algorithmic framework Manthan, which views functional synthesis as a classification problem, relying on advances in constrained sampling for data generation, and advances in automated reasoning for novel proof-guided refinement and provable verification. On an extensive and rigorous evaluation of 609 benchmarks, we demonstrate that Manthan significantly improves upon the current state of the art, solving 509 benchmarks in comparison to 280, which is the most solved by a state-of-the-art technique. The significant performance improvements, along with our detailed analysis, highlight several exciting avenues of future work in machine learning, constrained sampling, and automated reasoning.
Bio:
Priyanka Golia is a Ph.D. candidate at National University of Singapore and Indian Institute of Technology Kanpur, India. Her research interests lie in the area of automated reasoning and formal methods. Specifically, her work is directed at functional synthesis, constrained sampling, and knowledge compilation.