Dagstuhl Seminar 17351
Machine Learning and Formal Methods
( Aug 27 – Sep 01, 2017 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/17351
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)
Contact
- Annette Beyer (for administrative matters)
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, Andreas Krause, Sanjit A. Seshia, and Xiaojin Zhu
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:
- Probabilistic Programming
- Teaching and Oracle-Guided Synthesis
- Safe Learning-Based Control
- Probabilistic Program Analysis
- Adversarial Analysis and Repair for Machine Learning
- Inductive Synthesis and Learning
- Machine Learning for Theorem Proving and Optimization
- Explainable and Interpretable Machine Learning
- 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.
Susmit Jha, Andreas Krause, Sanjit A. Seshia, and Xiaojin Zhu
- S. Akshay (Indian Institute of Technology - Mumbai, IN) [dblp]
- Dalal Alrajeh (Imperial College London, GB) [dblp]
- Rajeev Alur (University of Pennsylvania - Philadelphia, US) [dblp]
- Nikolay A. Atanasov (University of California at San Diego, US) [dblp]
- Ammar Ben Khadra (TU Kaiserslautern, DE)
- Felix Berkenkamp (ETH Zürich, CH) [dblp]
- Ben Caulfield (University of California - Berkeley, US)
- Swarat Chaudhuri (Rice University - Houston, US) [dblp]
- Luc De Raedt (KU Leuven, BE) [dblp]
- Jyotirmoy Deshmukh (USC - Los Angeles, US) [dblp]
- Dana Fisman (Ben Gurion University - Beer Sheva, IL) [dblp]
- Pranav Garg (Amazon - Bangalore, IN) [dblp]
- Matthias Hein (Universität des Saarlandes, DE) [dblp]
- Holger Hermanns (Universität des Saarlandes, DE) [dblp]
- Susmit Jha (SRI - Menlo Park, US) [dblp]
- Kristian Kersting (TU Darmstadt, DE) [dblp]
- Andreas Krause (ETH Zürich, CH) [dblp]
- Sasa Misailovic (University of Illinois - Urbana-Champaign, US) [dblp]
- Mayur Naik (University of Pennsylvania - Philadelphia, US) [dblp]
- Nagarajan Natarajan (Microsoft Research India - Bangalore, IN) [dblp]
- Anna Rafferty (Carleton College - Northfield, US)
- Dorsa Sadigh (Stanford University, US) [dblp]
- Stephan Schulz (Duale Hochschule Baden-Württemberg - Stuttgart, DE) [dblp]
- Sanjit A. Seshia (University of California - Berkeley, US) [dblp]
- Rishabh Singh (Microsoft Research - Redmond, US) [dblp]
- Armando Solar-Lezama (MIT - Cambridge, US) [dblp]
- Charles Sutton (University of Edinburgh, GB) [dblp]
- Josef Urban (Czech Technical University - Prague, CZ) [dblp]
- Martin Vechev (ETH Zürich, CH) [dblp]
- Eran Yahav (Technion - Haifa, IL) [dblp]
- Yisong Yue (California Institute of Technology - Pasadena, US) [dblp]
- Xiaojin Zhu (University of Wisconsin - Madison, US) [dblp]
- Sandra Zilles (University of Regina, CA) [dblp]
Classification
- artificial intelligence / robotics
- semantics / formal methods
- verification / logic
Keywords
- Machine Learning
- Formal Methods
- Program Synthesis
- Robotics
- Cyber-Physical Systems
