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

Kuldeep Meel, PhD

Associate Professor of Computer Science

University of Toronto

9/8/2023

11AM – 12PM CST

Location: San Pedro 1, Room 530

506 Dolorosa St, San Antonio, TX 78204

Zoom: https://utsa.zoom.us/j/91049981814

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.