27. August – 01. September 2017, Dagstuhl-Seminar 17351

Machine Learning and Formal Methods


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)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl Report, Volume 7, Issue 8 Dagstuhl Report


This seminar seeks to bring together members of two communities:

  • The community that works on machine learning, both on theoretical topics and on applications to areas such as robotics and cyber-physical systems, and
  • The community that works on formal methods, 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 proving correctness of systems via automated deduction, e.g., using theorem proving or model checking as a core reasoning method.

However, recently, certain trends are starting to bring the two areas together:

  • Trusted Machine Learning: Machine learning is increasingly being used in applications where safety/correctness concerns are paramount;
  • Synthesis from Examples: It is increasingly effective to synthesize formal artifacts (programs, controllers, etc.) from examples, blending inductive learning with deduction;
  • Teaching vs. Learning: In both synthesis from examples and machine learning, the role of oracles (humans or otherwise) in guiding the learning process is receiving renewed attention from both a theoretical and practical perspective, and
  • Learning and Proof: There is increasing interest in leveraging machine learning to improve computational proof engines and make them work more effectively with humans.

These trends suggest that the time is ripe for a meeting to promote cross-fertilization between the areas at a deep technical level. This Dagstuhl Seminar is envisioned to have several benefits. First, formal methods can benefit from a more effective use of machine learning techniques particularly in the context of automated synthesis and guidance in proof search. Similarly, the use of machine learning in high-assurance applications can benefit greatly from an integration with formal methods; e.g., going beyond the i.i.d. assumption and into causality, optimal teaching, trading off exploration and exploitation, etc. Moreover, the organizers believe that the potential synergies between the two areas go beyond a straightforward application of the techniques in one area to the other area. The seminar will be a unique opportunity to explore new fundamental science in the intersection of machine learning and formal methods, and to discuss a range of industrially-relevant and impactful applications as well.

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


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


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


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.