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.
