The Coq mailing list

[geoff AT cs.miami.edu]

What: AAAI 2025 Tutorial on Machine Learning for Solvers
When: 2-6 PM ET, Wednesday Feb 26th, 2025
Where: Philadelphia, PA, USA
Web: https://ml-for-solvers.github.io/
Registration: https://aaai.org/conference/aaai/aaai-25/registration/
Signup: To save some money, please signup by Jan 20, 2025

More details:
Machine learning (ML) and logical 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. 
Notably, ML has had a dramatic impact on SAT and SMT solvers, as demonstrated 
by the award-winning SATzilla, MapleSAT, and Z3alpha solvers. Our tutorial 
aims to inspire new interdisciplinary research by bridging the gap between ML 
and logical reasoning research communities. We will introduce the broader AI 
community to ML techniques that have been used in the context of logical 
reasoning solvers, with a sharp focus on approaches that are successful and 
promising. We will also host a panel discussion on how LLMs may shape this 
area going forward.

Rather than pure end-to-end learning, successful ML approaches tend to be 
tightly integrated with symbolic solvers. The central thesis of our tutorial, 
supported by numerous successful cases, is that ML excels best when it is 
used to sequence, select, initialize, and configure proof/rewrite rules that 
solvers implement. One prominent example that we will highlight is the use of 
ML for learning branching heuristics, both online for particular instances 
using reinforcement learning (RL) and offline training a neural network 
policy across representative instances from a particular application.

There will be theory, hands-on lab, and panel discussion on the use of ML for 
solvers.