Topics
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.
The ML4SP 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.
Topics of interest include, but are not limited to, ML-driven approaches for:
- Heuristics (branching, restarts, …) in CP, SAT, SMT, and MIP solvers
- Tactic selection and proof guidance in automated and interactive theorem provers
- Algorithm selection, parameter tuning and 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
- Leveraging large language models (LLMs) for solver heuristics and proof guidance
This is a 2nd year of the workshop. The 1st ML4SP workshop (invited talks only) was organized at SoCS/SAT/CP 2025 in Glasgow.
Submission
We welcome submissions describing previously published work, ongoing research, and position papers and early-stage ideas intended to stimulate discussion. Submission should be in PDF form, following the LIPIcs guidelines. They can be:
- Extended abstracts (up to two pages, excluding references); or
- Full papers (up to 15 pages, excluding references).
Submissions do not need to be anonymized. All submissions will be reviewed by the PC members. A presentation time slot will be given to each accepted submission.
Submission link: https://submissions.floc26.org/ml4sp/
Dates
- Submission deadline: 15 May 2026 (AoE)
- Result notification: 25 May 2026
- Camera ready: 2 July 2026
- Workshop day: 18 July 2026
Registration
Please register via FLoC’26 registration page
Invited Talks
Federico Mora
Title and abstract: TBA
Short bio: Federico Mora is an incoming Assistant Professor at the University of Waterloo and Faculty Affiliate at the Vector Institute. His core research mission is to make verification of real-world systems practical at an industrial scale. In pursuit of this goal, Federico builds automated reasoning stacks — everything from SMT solvers to programming language interfaces — that combine the power and flexibility of artificial intelligence with the rigorous guarantees of formal methods.
Tias Guns
Title: Human-Aware Technology for Combinatorial Optimisation
Abstract: Combinatorial optimisation is widely used to solve scheduling, sequencing, rostering, routing and other assignment problems. The traditional paradigm is that of model+solve, where an expert user expresses their problem in constraints and a highly efficient solver searches for the optimal solution. Can we make this less static, and more centered around the decision maker? Adaptive, explainable, conversational? We’ll highlight recent work in decision-focussed ML training over combinatorial problems, preference learning for combinatorial optimisation and explainable constraint solving, developed as part of Prof. Guns’ ERC grant CHAT-Opt.
Short bio: Tias Guns is Professor in Computer Science at the DTAI lab of KU Leuven, Belgium. Tias’ expertise is in the hybridisation of machine learning systems with constraint solving systems, more specifically building constraint solving systems that reason both on explicit knowledge as well as knowledge learned from data. He aims to make constraint solving technology more accessible, as well as to make the technology more human-aware by learning from the daily operational environment and its users. He was awarded a prestigious ERC Consolidator grant in 2021 to work on conversational human-aware technology for optimisation, and currently leads a lab of 8 researchers.
Schedule
| Time | Title |
|---|---|
| 09:30-10:30 | Invited talk: Federico Mora |
| 10:30-11:00 | Coffee break |
| 11:00-11:20 | An LLM-based Recommendation System for PVS Nikson Bernardes Fernandes Ferreira, Mariano Miguel Moscato, Mauricio Ayala-Rincon |
| 11:20-11:40 | Neural Local Search Enhanced with Knowledge Compilation Alexandre Dubray, Hélène Verhaeghe, Quentin Cappart, Siegfried Nijssen |
| 11:40-12:00 | Algorithm Selection with Zero Domain Knowledge via Text Embeddings Stefan Szeider |
| 12:00-12:20 | Do LLMs Scale on Inductive Proofs? A Controlled Study of Elementary Arithmetical Proofs Risako Ando, Koji Mineshima, Mitsuhiro Okada |
| 12:20-12:40 | Learning Better Representations From Less Data For Propositional Satisfiability Mohamed Ghanem, Frederik Schmitt, Julian Siber, Bernd Finkbeiner |
| 12:40-14:00 | Lunch |
| 14:00-15:00 | Invited talk: Tias Guns Human-Aware Technology for Combinatorial Optimisation |
| 15:00-15:20 | Predicting Assignments of MaxSAT Variables with Graph Neural Networks Jonathan Oliva, Peter Nightingale, Felix Ulrich-Oltean |
| 15:20-15:40 | Caching and Batching for Neural Clause Selection in Saturation-Based Theorem Proving Alexander Pluska, Florian Zuleger |
| 15:40-16:10 | Coffee break |
| 16:10-16:30 | A priori knowledge for learning combinations of heuristics for CSPs Anastasia Paparrizou, Michael Sioutis, Yoan Thomas, Christian Bessiere |
| 16:30-16:50 | KissatEvolve: Controllable and Scalable Synthesis of SAT Heuristics with Densely Annotated Memory Bank Meru Gopalan, Jialin Lu, Jialin Song, Shimin Zhang, Hieu Nguyen, Wuyang Chen, Vijay Ganesh |
| 16:50-17:10 | Revealing the limits of Machine Learning for Satisfiability Testing: a dataset for learning minimal moves Laurent Simon |
| 17:10-18:00 | Panel discussion |
Program Committee
| Vijay Ganesh (chair) | Georgia Institute of Technology |
| Nguyen Dang (chair) | University of St Andrews |
| Shaowei Cai | Chinese Academy of Sciences |
| Quentin Cappart | UCLouvain and Polytechnique Montréal |
| Wuyang Chen | Simon Fraser University |
| Pascal Fontaine | LORIA, INRIA, Université de Lorraine |
| Guy Katz | The Hebrew University of Jerusalem |
| Sean Holden | Cambridge University |
| Mikoláš Janota | Czech Technical University |
| Lars Kotthoff | University of St Andrews |
| Peter Nightingale | University of York |
| Martin Suda | Czech Technical University |
| Dimos Tsouros | University of Western Macedonia |
| Felix Ulrich-Oltean | University of York |
