ML4SP — PROGRAM
Days: Saturday, 18 July 2026
Saturday, 18 July 2026
09:30-10:30
Invited talk 1
ML4SP
Location:
C4.08
10:00-11:00
Coffee Break
ML4SP
Location:
C4.08
11:00-12:40
Paper talks 1
ML4SP
Location:
C4.08
| 11:00-11:20 |
An LLM-based Recommendation System for PVS (abstract) 20 min
1 Universidade de Brasília
2 Analytical Mechanics Associates Inc.
|
| 11:20-11:40 |
Neural Local Search Enhanced with Knowledge Compilation (abstract) 20 min
1 KU Leuven
2 UCLouvain
3 UC Louvain and Polytechnique Montréal
|
| 11:40-12:00 |
Algorithm Selection with Zero Domain Knowledge via Text Embeddings (abstract) 20 min
1 TU Wien
|
| 12:00-12:20 |
Do LLMs Scale on Inductive Proofs? A Controlled Study of Elementary Arithmetical Proofs (abstract) 20 min
1 Keio University
|
| 12:20-12:40 |
Learning Better Representations From Less Data For Propositional Satisfiability (abstract) 20 min
1 CISPA Helmholtz Center for Information Security
|
12:40-14:00
Lunch
ML4SP
Location:
C4.08
14:00-15:00
Invited talk 2
ML4SP
Location:
C4.08
15:00-15:40
Paper talks 2
ML4SP
Location:
C4.08
| 15:00-15:20 |
Predicting Assignments of MaxSAT Variables with Graph Neural Networks (abstract) 20 min
1 University of York
|
| 15:20-15:40 |
Caching and Batching for Neural Clause Selection in Saturation-Based Theorem Proving (abstract) 20 min
1 TU Wien
|
15:40-16:10
Coffee Break
ML4SP
Location:
C4.08
16:10-17:10
Paper talks 3
ML4SP
Location:
C4.08
| 16:10-16:30 |
A priori knowledge for learning combinations of heuristics for CSPs (abstract) 20 min
1 CNRS, University of Montpellier
|
| 16:30-16:50 |
KissatEvolve: Controllable and Scalable Synthesis of SAT Heuristics with Densely Annotated Memory Bank (abstract) 20 min
1 Georgia Institute of Technology
2 Simon Fraser University
|
| 16:50-17:10 |
Revealing the limits of Machine Learning for Satisfiability Testing: a dataset for learning minimal moves (abstract) 20 min
1 LaBRI
2 Bordeaux INP
3 Univ Bordeaux
4 CNRS
|
17:10-18:00
Panel discussion
ML4SP
Location:
C4.08