From: geoff@cs.miami.edu
To: <caml-list@inria.fr>
Subject: [Caml-list] 2nd Workshop on Machine Learning for Solvers and Provers
Date: Wed, 25 Feb 2026 11:44:24 -0500 [thread overview]
Message-ID: <20260225164424.EFEAAA018CC@armistead.ccs.miami.edu> (raw)
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 2601 bytes --]
CfP: 2nd Workshop on Machine Learning for Solvers and Provers - Lisbon - July 18
=========================================
We warmly invite you to submit your work to the 2nd Workshop on Machine Learning for Solvers and Provers (ML4SP), organised as part of the 2026 Federated Logic Conference (FLoC 2026) at Lisbon, Portugal. The workshop will run during the first block of the conference, on July 18, 2026.
Workshop website: https://ml4sp.github.io/
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
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).
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/
Key dates:
+ Submission deadline: 15 May 2026 AoE
+ Result notification: 25 May 2026
+ Camera ready: 2 July 2026
+ Workshop day: 18 July 2026
Registration: please see FLoC’26 registration page
reply other threads:[~2026-02-25 16:47 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20260225164424.EFEAAA018CC@armistead.ccs.miami.edu \
--to=geoff@cs.miami.edu \
--cc=caml-list@inria.fr \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox