When: Thursday, September 29, 2022, 11am (CEST).

Where: Zoom online, check the address in the Google Calendar Event.

Topic: Functional Synthesis: Formal Methods meets Machine Learning.

Speaker: Priyanka Golia, Ph.D. candidate at IITK, India and NUS, Singapore.

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 a novel proof-guided refinement and provable verification. On an extensive and rigorous evaluation over 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, highlights several interesting avenues of future work at the intersection of machine learning, constrained sampling, and automated reasoning.

The talk is based on following two papers:

  1. [CAV-2020] Manthan: A Data-Driven Approach for Boolean Function Synthesis
  2. [ICCAD 2021] Engineering an Efficient Boolean Functional Synthesis Engine.

Short Bio

Priyanka Golia is Ph.D. candidate at IITK, India and NUS, Singapore. Her research interest lies in the area of functional synthesis, constrained sampling, and knowledge compilation. She is the lead designer of the state-of-the-art functional synthesis engine Manthan, which takes advantage of advances in machine learning, constrained sampling, and automated reasoning to synthesize Boolean functions efficiently.

Material