Seminar Homepage : Druckversion


http://www.dagstuhl.de/17351

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

Machine Learning and Formal Methods

Organisatoren

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 erteilen

Annette Beyer zu administrativen Fragen

Marc Herbstritt zu wissenschaftlichen Fragen

Dokumente

Teilnehmerliste
Gemeinsame Dokumente

Motivation

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.

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

Classification

Keywords



Buchausstellung

Bücher der Teilnehmer 

Buchausstellung im Erdgeschoss der Bibliothek

(nur in der Veranstaltungswoche).

Dokumentation

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

Publikationen

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.


Seminar Homepage : Letzte Änderung 12.12.2017, 14:49 Uhr