August 27 – September 1 , 2017, Dagstuhl Seminar 17351
Machine Learning and Formal Methods
For support, please contact
Annette Beyer for administrative matters
Marc Herbstritt for scientific matters
Dagstuhl Seminar Schedule (Upload here)
(Use seminar number and access code to log in)
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.
Creative Commons BY 3.0 DE
Susmit Jha and Andreas Krause and Sanjit A. Seshia and Xiaojin Zhu
- Artificial Intelligence / Robotics
- Semantics / Formal Methods
- Verification / Logic
- Machine Learning
- Formal Methods
- Program Synthesis
- Cyber-Physical Systems