Title: Learning Logical Expressions

Speaker: Madhusudan Parthasarathy    (bio) (bio)

Madhusudan Parthasarathy is a Professor of Computer Science at the University of Illinois at Urbana-Champaign. He has worked on several projects that turn the theory lens to problems in software verification including visibly pushdown languages, ICE-learning for learning inductive invariants, and natural proofs for proving programs that manipulate data structures. His current interests are in software verification, program synthesis, and trustworthy AI.

When: Tuesday, 28 November 2023 at 1900 hrs (IST)       

Abstract:
We consider the problem of learning logical formulas/expressions that work as classifiers of structures. Logic learning has many applications ranging from program synthesis from input-output examples, learning specifications from code (contracts and inductive invariants), interpretable concept learning in AI, synthesizing lemmas to help prove theorems, finding axiomatizations, and, more generally, replacing certain creative tasks that currently require human help in many applications.

We will first motivate logic learning using the applications above. We then will turn a theory lens to this problem by considering when the logic learning problem is decidable. We show a general technique using tree automata that realize learning algorithms for a variety of logics/languages ranging from fragments of FOL, regular expressions, temporal logics, grammars, to string transformation for Excel (as in Flashfill). We in fact will show a meta-theorem that can be used to show a logic is decidable simply by programming a particular kind of evaluator for its semantics. This theory suggests that many logics can be learned by using Version Space Algebras (VSAs) based on tree automata.

If time permits, we will also consider the problem of learning logics themselves to aid few-shot learning.