Vijay Ganesh Seminar

From its inception, AI has had two broad sub-fields, namely, reasoning and learning, with little interaction between them. In recent years, there is a growing recognition that if our goal is to solve problems at the cutting-edge of AI (trustworthy AI, AI for Science, AI for Math), then we need to bring these sub-fields together. In this talk, I will present techniques and results showing how machine learning (ML) can be used in the service of automated reasoning (a la, SAT/SMT solvers), and in the reverse direction, how symbolic reasoning engines can be used to improve LLMs. The key idea in both directions is the same: the ML model is viewed as a synthesizer that generates assignments/code/proofs/molecules/equations, while the reasoning engine acts as a verifier that provides corrective feedback to the model at various points (training, fine-tuning, or inference) in its life cycle.

 

Vijay Ganesh is a professor of computer science at Georgia Tech. Prior to joining Georgia Tech in 2023, Ganesh was a professor at the University of Waterloo in Canada from 2012 to 2023, co-director of the Waterloo AI Institute from 2021 to 2023, and a research scientist at the Massachusetts Institute of Technology from 2007 to 2012. Ganesh completed his PhD in computer science from Stanford University in 2007. His primary area of research is the theory and practice of SAT/SMT solvers, and their application in AI, software engineering, security, mathematics, and physics. In this context he has led the development of many SAT/SMT solvers, most notably, STP, Z3str family of string solvers, AlphaZ3, MapleSAT, AlphaMapleSAT, and MathCheck. On the theoretical side, he works on topics in mathematical logic and proof complexity. More recently he has started working on problems in AI that can be solved via combinations of automated reasoning and machine learning, notably the use of machine learning for efficient solvers and the use of solvers aimed at making AI more trustworthy, secure, and robust. For his research, Ganesh has won over 35 awards, honors, and medals, including an ACM Impact Paper Award at ISSTA 2019, ACM Test of Time Award at CCS 2016, and a Ten-Year Most Influential Paper citation at DATE 2008.