DROPS

Document

Machine Learning and Logical Reasoning: The New Frontier (Dagstuhl Seminar 22291)

Authors: Sébastien Bardin, Somesh Jha, and Vijay Ganesh

Published in: Dagstuhl Reports, Volume 12, Issue 7 (2023)

Abstract

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 mathematics? This Dagstuhl seminar seeks to answer these and related questions, 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.

Cite as

Sébastien Bardin, Somesh Jha, and Vijay Ganesh. Machine Learning and Logical Reasoning: The New Frontier (Dagstuhl Seminar 22291). In Dagstuhl Reports, Volume 12, Issue 7, pp. 80-111, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{bardin_et_al:DagRep.12.7.80,
  author =	{Bardin, S\'{e}bastien and Jha, Somesh and Ganesh, Vijay},
  title =	{{Machine Learning and Logical Reasoning: The New Frontier (Dagstuhl Seminar 22291)}},
  pages =	{80--111},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2023},
  volume =	{12},
  number =	{7},
  editor =	{Bardin, S\'{e}bastien and Jha, Somesh and Ganesh, Vijay},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.12.7.80},
  URN =		{urn:nbn:de:0030-drops-176131},
  doi =		{10.4230/DagRep.12.7.80},
  annote =	{Keywords: Logic for ML, ML-based heuristics for solvers, SAT/SMT/CP solvers and theorem provers, Security, reliability and privacy of ML-based systems}
}

Document

DOI: 10.4230/DagRep.9.2.27

Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving (Dagstuhl Seminar 19062)

Authors: Sébastien Bardin, Nikolaj Bjørner, and Cristian Cadar

Published in: Dagstuhl Reports, Volume 9, Issue 2 (2019)

Abstract

This report documents the program and the outcomes of Dagstuhl Seminar 19062 "Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving", whose main goals were to bring together leading researchers in the different subfields of automated reasoning and constraint solving, foster greater communication between these communities and exchange ideas about new research directions. Constraint solving is at the heart of several key technologies, including program analysis, testing, formal methods, compilers, security analysis, optimization, and AI. During the last two decades, constraint solving has been highly successful and transformative: on the one hand, SAT/SMT solvers have seen a significant performance improvement with a concomitant impact on software engineering, formal methods and security; on the other hand, CP solvers have also seen a dramatic performance improvement, with deep impact in AI and optimization. These successes bring new applications together with new challenges, not yet met by any current technology. The seminar brought together researchers from SAT, SMT and CP along with application researchers in order to foster cross-fertilization of ideas, deepen interactions, identify the best ways to serve the application fields and in turn help improve the solvers for specific domains.

Cite as

Sébastien Bardin, Nikolaj Bjørner, and Cristian Cadar. Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving (Dagstuhl Seminar 19062). In Dagstuhl Reports, Volume 9, Issue 2, pp. 27-47, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{bardin_et_al:DagRep.9.2.27,
  author =	{Bardin, S\'{e}bastien and Bj{\o}rner, Nikolaj and Cadar, Cristian},
  title =	{{Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving (Dagstuhl Seminar 19062)}},
  pages =	{27--47},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2019},
  volume =	{9},
  number =	{2},
  editor =	{Bardin, S\'{e}bastien and Bj{\o}rner, Nikolaj and Cadar, Cristian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.9.2.27},
  URN =		{urn:nbn:de:0030-drops-108574},
  doi =		{10.4230/DagRep.9.2.27},
  annote =	{Keywords: Automated Decision Procedures, Constraint Programming, SAT, SMT}
}

Search Results

Documents authored by Bardin, Sébastien

Machine Learning and Logical Reasoning: The New Frontier (Dagstuhl Seminar 22291)

Abstract

Cite as

Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving (Dagstuhl Seminar 19062)

Abstract

Cite as

Thanks for your feedback!

Could not send message