BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:IC Colloquium: Program Synthesis for Reliable and Interpretable Ar
 tificial Intelligence
DTSTART:20181213T101500
DTEND:20181213T113000
DTSTAMP:20260407T045610Z
UID:a6d8b5b0b67f7afa490d0fc6e2177af719d3bd357b834d27f0c1bfd4
CATEGORIES:Conferences - Seminars
DESCRIPTION:By: Swarat Chaudhuri - Rice University\n\nAbstract:\nWe are cu
 rrently in an "AI spring"\, largely fuelled by recent breakthroughs in mac
 hine learning. However\, the deep neural networks that currently rule mach
 ine learning have certain well-known flaws: they are susceptible to advers
 arial examples\, are difficult to interpret\, debug and verify\, can be ex
 ceedingly data-hungry\, and sometimes do not generalize well. These flaws 
 make the design of reliable systems with neural components an especially c
 hallenging task.\n\nIn this talk\, I will argue that the field of Formal M
 ethods can offer powerful tools for overcoming these difficulties\, and th
 at in particular\, there is value in seeing machine learning as a form of 
 *program synthesis*. Program synthesis is the problem of automatically dis
 covering high-level programs that satisfy a specification. The problem was
  first posed in the 1960s and has had a resurgence in the Formal Methods c
 ommunity in the recent past.  Framed as program\nsynthesis\, machine lear
 ning becomes the problem of automatically discovering a model (represented
  as a program in a high-level "neurosymbolic" language) that optimally fit
 s a dataset and satisfies additional correctness invariants such as robust
 ness and fairness. Such a formulation has a number of advantages. First\, 
 it is easier to enforce formal safety guarantees at the time of learning a
 s opposed to after the fact\, and at the level of high-level programs as o
 pposed to low-level neural networks. Second\, high-level models are easier
  to interpret\, and are more easily constrained by domain-specific insight
 s\, than neural nets. Third\, the compositional representation offered by 
 modern programming languages can aid transfer of knowledge across learning
  tasks and reduce the need for data. Fourth\, the syntactic constraints of
  a programming language can serve as a form of regularization\, allowing t
 he model to generalize better.\n\nThe fundamental algorithmic challenge in
  program synthesis is that it is a hard combinatorial optimization problem
 . I will describe a few recent efforts from my group that approach this ch
 allenge using a mix of ideas from formal methods and deep learning. One of
  these methods learns a neural representation of the target function using
  gradient-based techniques\, then synthesizes a high-level program that im
 itates the behavior of this neural model. A second leverages functional pr
 ogramming abstractions and type-based deduction to search a large space of
  neural architectures.  A third develops a series of\ndifferentiable appr
 oximations to a program verifier that can be used to learn model parameter
 s while ensuring a set of Boolean correctness properties. These results op
 en up a playground of new algorithmic problems\, and form the beginnings o
 f a long-term agenda of marrying Formal Methods with Machine Learning.\n\n
 Bio: \nSwarat Chaudhuri is an Associate Professor of Computer Science at R
 ice University. He studies algorithms --- based on automated deduction\, c
 ombinatorial search and optimization\, and statistical machine learning --
 - for program analysis and synthesis\, and the use of these algorithms in 
 practical systems that make programs more reliable\, faster\, and easier t
 o write.\n\nSwarat received a bachelor's degree in computer science from t
 he Indian Institute of Technology\, Kharagpur\, in 2001\, and a doctoral d
 egree in computer science from the University of Pennsylvania in 2007. Fro
 m 2008-2011\, he was an Assistant Professor at the Pennsylvania State Univ
 ersity. He is a recipient of the National Science Foundation CAREER award\
 , the ACM SIGPLAN John Reynolds Doctoral Dissertation Award\, the Morris a
 nd Dorothy Rubinoff\nDissertation Award\, and a Google Research Award. He 
 has served on program committees of many conferences in Formal Methods and
  Programming Languages\, and chaired the 2016 Conference on Computer-Aided
  Verification (CAV).\n\nMore information\n 
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR