August 27 – September 1 , 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)

For support, please contact

Dagstuhl Service Team


Dagstuhl Report, Volume 7, Issue 8 Dagstuhl Report
List of Participants


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 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).


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.