Dagstuhl Seminar 22291
Machine Learning and Logical Reasoning: The New Frontier
( Jul 17 – Jul 22, 2022 )
Permalink
Organizers
- Sébastien Bardin (CEA LIST, FR)
- Vijay Ganesh (University of Waterloo, CA)
- Somesh Jha (University of Wisconsin-Madison, US)
- Joao Marques-Silva (CNRS - Toulouse, FR)
Contact
- Michael Gerke (for scientific matters)
- Jutka Gasiorowski (for administrative matters)
Shared Documents
- Dagstuhl Materials Page (Use personal credentials as created in DOOR to log in)
Schedule
Machine learning (ML) and logical reasoning have been the two key pillars of AI since its inception, and yet, there has been little interaction between these two sub-fields over the years. At the same time, each of them has been very influential in their own way. ML has revolutionized many sub-fields of AI including image recognition, language translation, and game playing, to name just a few. Independently, the field of logical reasoning (e.g., SAT/SMT/CP/first-order solvers and knowledge representation) has been equally impactful in many contexts in software engineering, verification, security, AI, and mathematics. Despite this progress, there are new problems, as well as opportunities, on the horizon that seem solvable only via a combination of ML and logic.
One such problem that requires one to consider combinations of logic and ML is the question of reliability, robustness, and security of ML models. For example, in recent years, many adversarial attacks against ML models have been developed, demonstrating their extraordinary brittleness. How can we leverage logic-based methods to analyze such ML systems with the aim of ensuring their reliability and security? What kind of logical language do we use to specify properties of ML models? How can we ensure that ML models are explainable and interpretable?
In the reverse direction, ML methods have already been successfully applied to making solvers more efficient. In particular, solvers can be modeled as complex combinations of proof systems and ML optimization methods, wherein ML-based heuristics are used to optimally select and sequence proof rules. How can we further deepen this connection between solvers and ML? Can we develop tools that automatically construct proofs for higher math?
To answer these and related questions we are organizing this Dagstuhl Seminar, with the aim of bringing together the many world-leading scientists who are conducting pioneering research at the intersection of logical reasoning and ML, enabling development of novel solutions to problems deemed impossible otherwise.

- Rajeev Alur (University of Pennsylvania - Philadelphia, US) [dblp]
- Sébastien Bardin (CEA LIST, FR) [dblp]
- Chih-Hong Cheng (Fraunhofer IKS - München, DE) [dblp]
- Jonathan Chung (University of Waterloo, CA)
- Judith Clymo (University of Liverpool, GB)
- Artur d'Avila Garcez (City - University of London, GB) [dblp]
- Alhussein Fawzi (Google DeepMind - London, GB)
- Marc Fischer (ETH Zürich, CH)
- Pascal Fontaine (University of Liège, BE) [dblp]
- Matt Fredrikson (Carnegie Mellon University - Pittsburgh, US)
- Vijay Ganesh (University of Waterloo, CA) [dblp]
- Sebastian Junges (Radboud University Nijmegen, NL) [dblp]
- Chunxiao (Ian) Li (University of Waterloo, CA)
- Ravi Mangal (Carnegie Mellon University - Pittsburgh, US)
- Georg Martius (MPI für Intelligente Systeme - Tübingen, DE)
- Kuldeep S. Meel (National University of Singapore, SG) [dblp]
- Grégoire Menguy (CEA LIST - Nano-INNOV, FR)
- Matthew Mirman (ETH Zürich, CH)
- Anselm Paulus (MPI für Intelligente Systeme - Tübingen, DE)
- Markus N. Rabe (Google - Mountain View, US)
- Joseph Scott (University of Waterloo, CA)
- Xujie Si (McGill University - Montréal, CA) [dblp]
- Armando Tacchella (University of Genova, IT) [dblp]
- Hazem Torfah (University of California - Berkeley, US) [dblp]
- Caterina Urban (INRIA - Paris, FR) [dblp]
- Saranya Vijayakumar (Carnegie Mellon University - Pittsburgh, US)
- Somesh Jha (University of Wisconsin-Madison, US) [dblp]
- Luis C. Lamb (Federal University of Rio Grande do Sul, BR) [dblp]
- Vineel Nagisetty (Borealis AI - Toronto, CA)
- Sanjit A. Seshia (University of California - Berkeley, US) [dblp]
Related Seminars
Classification
- Logic in Computer Science
- Machine Learning
- Software Engineering
Keywords
- SAT/SMT/CP solvers and theorem provers
- Testing
- Analysis
- Verification
- and Security of Machine Learning
- Neuro-symbolic AI