https://www.dagstuhl.de/17351

August 27 – September 1 , 2017, Dagstuhl Seminar 17351

Machine Learning and Formal Methods

Organizers

Susmit Jha (SRI – Menlo Park, US)
Andreas Krause (ETH Zürich, CH)
Sanjit A. Seshia (University of California – Berkeley, US)
Xiaojin Zhu (University of Wisconsin – Madison, US)

For support, please contact

Dagstuhl Service Team

Documents

Dagstuhl Report, Volume 7, Issue 8 Dagstuhl Report
Aims & Scope
List of Participants

Summary

The seminar was successful in bringing the following two communities together:

  • The community that works on machine learning (ML), both on theoretical topics and on applications to areas such as robotics and cyber-physical systems, and
  • The community that works on formal methods (FM), both on computational proof techniques and on applications to formal verification and program/controller synthesis.

Both communities have long and vibrant histories, with associated conferences and journals. However, they have rarely intersected. The machine learning community has traditionally focused on inductive learning from data, with the data set considered as partial (potentially noisy) observations of some phenomenon. The formal methods community has traditionally emphasized automated deduction, e.g., using theorem proving or model checking, as a core reasoning method, with a heavy emphasis placed on formal models and proofs of correctness using those models. However, recent ideas and methods have appeared that demonstrate new connections between the two disciplines, which suggested that the time is ripe for a meeting to promote cross-fertilization between the areas at a deep technical level. This seminar has been a significant step forward to bring the two communities together.

More concretely, the Seminar and the interaction it facilitated has brought three kinds of benefits. First, formal methods can benefit from a more effective use of machine learning techniques particularly in the context of automated synthesis. Similarly, the increasing use of machine learning in applications that require a high level of assurance points to the need for integration with formal methods. However, the potential synergies between the two areas go beyond a simple application of the techniques in one area to the other area. Importantly, there is new fundamental science to be explored in the intersection of machine learning and formal methods, related to the the confluence of inductive and deductive reasoning, and which can inform a range of new industrially-relevant applications as well.

The seminar had about 40 participants from both the FM and ML communities. The organizers took several steps to foster discussion and cross-pollination of ideas between the two communities, including the following:

  • Formal Methods participants, and a half-day tutorial on Formal Methods for a Machine Learning audience. These tutorials helped to establish a common vocabulary to discuss ideas, problems and solutions.
  • Sessions were organized based on themes that emerged in discussions before the seminar and during the first day. The list of session topics is as follows:
  1. Probabilistic Programming
  2. Teaching and Oracle-Guided Synthesis
  3. Safe Learning-Based Control
  4. Probabilistic Program Analysis
  5. Adversarial Analysis and Repair for Machine Learning
  6. Inductive Synthesis and Learning
  7. Machine Learning for Theorem Proving and Optimization
  8. Explainable and Interpretable Machine Learning
  9. Deep Learning and Verification/Synthesis

In organizing these sessions, the organizers tried to combine speakers from both ML and FM areas to foster discussion and comparison of approaches.

  • Seating arrangements at meals were organized so that (a) each table had an approximately qual number of participants from both communities, and (b) the seating was randomly hanged from meal to meal.
  • A joint session was organized with the concurrent seminar on analysis and synthesis of floating-point programs. This session had a panel discussion on floating-point issues in machine learning programs.

After the seminar, we have heard positive feedback from multiple participants. One told us that he started a new research project as a direct result of the seminar. A group of participants are planning to continue the interaction via joint workshops at major venues of both communities such as CAV, PLDI, ICML, NIPS, etc.

Summary text license
  Creative Commons BY 3.0 Unported license
  Susmit Jha, Andreas Krause, Sanjit A. Seshia, and Xiaojin Zhu

Classification

  • Artificial Intelligence / Robotics
  • Semantics / Formal Methods
  • Verification / Logic

Keywords

  • Machine Learning
  • Formal Methods
  • Program Synthesis
  • Robotics
  • Cyber-Physical Systems

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.