Machine learning (ML) and neural networks in particular have achieved superhuman performance in numerous applications. However, most existing ML techniques are domain specific and their results are often not interpretable. For domains where correctness is critical, ensuring that learned system provide worst-case guarantees is an open problem. Formal methods (FM) are rich in languages and algorithms to specify and ensure correctness, yet their application to systems involving learned components has been explored over few specific problems.

One of the major tasks in combining machine learning and formal methods—high performance and formal guarantees—is formulating correctness properties for learned system using formal languages that are amenable to verification or, in the other direction, expressing formal safety so that it can coexist with statistical ML methods. The challenge is making machine learning and formal methods speak a common language. This workshop encourages the discussion between ML and FM practitioners on open problems in achieving reliable ML-based technology. Our goal is to stimulate the investigation of various techniques and specifications in order to get closer to a general unifying approach to learning and verification. Scaling up FM with ML and certifying ML with FM have major implications on the research and practice on complex systems with learned components.

We aim to bring together researchers working on different aspects of machine learning and verification with the goal to discuss open problems and to establish collaborations for solving them. We intend to make this an exciting event for researchers worldwide, with presentations by leading scientists from both fields and discussion tables on current and future research directions.