Co-chairs
Overview
Learning and reasoning have been the two foundational pillars of AI since its inception, yet it is only in the past decade that interactions between these fields have become increasingly prominent. In particular, machine learning (ML) has had a substantial impact on SAT/SMT and CP solvers, as well as automated theorem provers. Recent advances have demonstrated the power of ML to inform solver heuristics, guide proof search, and optimize algorithm portfolios.
Despite growing interest in this direction, work on ML for solvers and provers is often scattered across multiple research communities — SAT, SMT, CP, theorem proving, formal methods, and machine learning - with few opportunities for focused interaction. This workshop aims to bring together researchers and practitioners working at the intersection of machine learning and formal reasoning systems. It provides a forum for the presentation of recent work, the exchange of ideas, and the fostering of collaboration between these communities.
Scope
Topics of interest include, but are not limited to, the use of various machine learning (ML) techniques in:
- Heuristics (branching, restarts,…) for SAT, SMT, and CP solvers
- Tactic selection and proof guidance in automated and interactive theorem provers
- Algorithm selection, algorithm configuration, and portfolio solvers
- End-to-end learning for solvers and provers
- Benchmark generation and instance hardness prediction
- Applications of ML-enhanced reasoning in verification, synthesis, planning, and related areas
