Title:
Functional Synthesis: An Ideal Meeting Ground for Formal
Methods and Machine Learning
Abstract:
Don't
we all dream of the perfect assistant whom we can just
tell what to do and the assistant can figure out how to
accomplish the tasks?
Formally, 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 F(X,G(X)) is true. 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 356
benchmarks in comparison to 280, which is the most
solved by a state of the art technique; thereby, we
demonstrate an increase of 76 benchmarks over the
current state of the art. The significant performance
improvements call for interesting future work at the
intersection of machine learning, constrained sampling,
and automated reasoning.
Bio:
Kuldeep Meel is the Sung Kah Kay Assistant Professor in
the Computer Science Department of School of Computing
at the National University of Singapore. His research
interests lie at the intersection of Formal Methods and
Artificial Intelligence. He is a recipient of 2019 NRF
Fellowship for AI (accompanied with 2.5 million SGD
funding), and was named AI's 10 to Watch by IEEE
Intelligent Systems in 2020. His work received the 2018
Ralph Budd Award for Best PhD Thesis in Engineering,
2014 Outstanding Masters Thesis Award from Vienna Center
of Logic and Algorithms and Best Student Paper Award at
CP 2015. He received his Ph.D. (2017) and M.S. (2014)
degree from Rice University, and B. Tech. (with Honors)
degree (2012) in Computer Science and Engineering from
Indian Institute of Technology, Bombay.
JOHN
CYPHERT is inviting you to a scheduled Zoom meeting.
Topic: Kuldeep Meel MadPL Seminar
Time: Mar 24, 2021 09:00 AM Central Time (US and
Canada)
Join Zoom Meeting
Meeting ID: 943 4908 2113
Passcode: 396030
One tap mobile
+13126266799,,94349082113#,,,,*396030# US (Chicago)
+19292056099,,94349082113#,,,,*396030# US (New York)
Dial by your location
+1 312 626 6799 US (Chicago)
+1 929 205 6099 US (New York)
+1 301 715 8592 US (Washington DC)
+1 346 248 7799 US (Houston)
+1 669 900 6833 US (San Jose)
+1 253 215 8782 US (Tacoma)
Meeting ID: 943 4908 2113
Passcode: 396030
Join by SIP
Join by H.323
162.255.37.11 (US West)
162.255.36.11 (US East)
115.114.131.7 (India Mumbai)
115.114.115.7 (India Hyderabad)
213.19.144.110 (Amsterdam Netherlands)
213.244.140.110 (Germany)
103.122.166.55 (Australia Sydney)
103.122.167.55 (Australia Melbourne)
149.137.40.110 (Singapore)
64.211.144.160 (Brazil)
69.174.57.160 (Canada Toronto)
65.39.152.160 (Canada Vancouver)
207.226.132.110 (Japan Tokyo)
149.137.24.110 (Japan Osaka)
Meeting ID: 943 4908 2113
Passcode: 396030
![[Computer Systems Lab]](http://www.cs.wisc.edu/pics/csl_logo.gif){kind=logo}