⚙️ Machine Learning for SMT
This page highlights ongoing and past research efforts applying machine learning to improve SMT and related solvers at the reasoning and learning research group @ Georgia Tech led by Professor Vijay Ganesh.
Z3alpha: Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis (2024)
Authors: John Zhengyang Lu1, Joel Day2, Piyush Jha3, Paul Sarnighausen-Cahn4, Stefan Siemer4, Florin Manea4, Vijay Ganesh3
Affiliations: 1University of Waterloo | 2Loughborough University | 3Georgia Institute of Technology | 4University of Göttingen
TL;DR: Z3alpha applies novel Monte Carlo Tree Search (MCTS) methods to automatically synthesize effective and interpretable solving strategies for SMT solvers. Built on top of Z3, it achieved state-of-the-art performance, winning multiple first prizes at SMT-COMP in both 2024 and 2025, including in challenging logics such as QF_NIA and QF_NRA.
Btor2-Select: Machine Learning Based Algorithm Selection for Hardware Model Checking (2025)
Authors: John Zhengyang Lu1, Po-Chun Chien2, Nian-Ze Lee2,3, Arie Gurfinkel1, Vijay Ganesh4
Affiliations: 1University of Waterloo | 2LMU Munich | 3National Taiwan University | 4Georgia Institute of Technology
TL;DR: Btor2-Select is a machine-learning-based algorithm-selection framework for hardware verifiers. Using a simple and effective design supported by a graph-based circuit representation, Btor2-Select significantly improves the performance of single verifiers and delivers strong generalization across diverse hardware benchmarks.
Goose: A Meta-Solver for Deep Neural Network Verification (2022)
Authors: Joseph Scott1, Guanting Pan1, Elias B. Khalil2, Vijay Ganesh1
Affiliations: 1University of Waterloo | 2University of Toronto
TL;DR: Goose is a meta-solver for deep neural network verification. Its architecture supports a wide variety of complete and incomplete solvers and leverages three key meta-solving techniques to improve efficiency: algorithm selection, probabilistic satisfiability inference, and time iterative deepening. Goose achieves a 47.3% improvement in PAR-2 score across over 800 benchmarks and 13 solvers from VNN-COMP '21.
MachSMT: Algorithm Selection for SMT (2021)
Authors: Joseph Scott1, Aina Niemetz2, Mathias Preiner2, Saeed Nejati1, Vijay Ganesh1
Affiliations: 1University of Waterloo | 2Stanford University
TL;DR: MachSMT is an algorithm selection tool for SMT solvers that supports the full SMT-LIB language. It uses machine learning to build empirical hardness models and pairwise ranking comparators, allowing it to predict solver performance and rank solvers for any given formula. Extensively evaluated on data from SMT-COMP 2019 and 2020, MachSMT frequently improves on the competition winners.
BanditFuzz: Fuzzing SMT Solvers with Multi-agent Reinforcement Learning (2021)
Authors: Joseph Scott1, Trishal Sudula1, Hammad Rehman1, Federico Mora2, Vijay Ganesh1
Affiliations: 1University of Waterloo | 2University of California, Berkeley
TL;DR: BanditFuzz is a multi-agent reinforcement learning fuzzer that automatically generates inputs exposing performance bottlenecks in SMT solvers. It supports all SMT-LIB theories, lets users control input size, and significantly outperforms random and single-agent fuzzing, achieving up to an 82.6% gain in PAR-2 margins. Tested across 52 logics in SMT-COMP 2020, BanditFuzz uncovered surprising performance issues in major solvers including CVC4, Z3, and Bitwuzla..