3rd Workshop on Formal Verification and Machine Learning (WFVML 2024)

[Proposal] About This Workshop

As data and computing infrastructures become increasingly abundant, machine learning (ML) systems are applied to ever more problems. However, for safety-critical domains, their high performance alone is not enough: applications like autonomous driving, robotics control, and medical imaging require rigorous safety guarantees. Unfortunately, many modern ML approaches lack such guarantees, precluding their adaptation. As a result, a growing body of work on formally verifying the behavior of ML systems and leveraging ML for the formal verification of classical software has emerged. While both of these communities consider the intersection of  ML and formal methods, their different target audiences and, thus, conferences of choice have limited their interaction so far. 

Our proposed Workshop on Formal Verification and Machine Learning (WFVML) aims to bridge this gap between the formal verification and ML communities. On one hand, ML techniques offer high performance but struggle to provide strong guarantees for safety-critical applications. On the other hand, formal verification methods come with rigorous guarantees but suffer from scalability issues. Encouraging dialogue between these two research communities is, therefore, crucial to their mutual advancement and success. The integration of ML and formal verification is a young and interdisciplinary field that sits at the intersection of machine learning, robotics, programming languages, and security, among others. This workshop aims to (1) bring together researchers from diverse backgrounds interested in the intersection of ML and formal verification, (2) raise awareness for the mutual benefit between ML and formal verification, and (3) discuss promising future research directions for tackling open problems in both fields.

This workshop covers a holistic perspective on formal verification and machine learning and does not significantly overlap with other workshops at NeurIPS. Topics include but are not limited to:

• Formal verification and certified training methods for a broad range of ML models.

• Applied ML techniques for formal verification.

• New applications of formal methods, such as formal verification for generative AI, autonomous systems, programming languages, cybersecurity, etc.

• Datasets and benchmarks for formal verification of machine learning and ML for formal verification.

Our workshop features a diverse panel of invited speakers spanning research backgrounds including machine learning, formal methods, programming languages, and security. Please check out our tentative workshop schedule.