Research
I am interested in engineering systems that combine deductive reasoning tools with inductive and abductive ones: solvers that learn, and learners that can be checked.
- Automated reasoning: propositional satisfiability, satisfiability modulo theories, mixed-integer linear programming, and the solvers behind them.
- Machine learning: meta-learning, algorithm selection, active learning, machine teaching, symbolic regression.
- AI safety: verification of neural networks.
- Applications: reinforcement-learning driven fuzzing and testing, physics and automated scientific discovery, finance.
Software
- MachSMT: a machine-learning algorithm selector for SMT solvers covering the whole SMT-LIB language. Builds empirical hardness models and pairwise ranking comparators over state-of-the-art solvers and ranks them by predicted runtime on a given formula.
- BanditFuzz: a multi-agent reinforcement-learning performance fuzzer. Constructs inputs that expose performance gaps between target and reference SMT solvers. The first performance fuzzer supporting every theory in SMT-LIB.
- Goose: a meta-solver for deep neural network verification. Combines algorithm selection, probabilistic satisfiability inference, and time iterative deepening across complete and incomplete solvers, for a 47.3% PAR-2 improvement over 800+ VNN-COMP ‘21 benchmarks and 13 solvers.
- Pierce: a testing infrastructure for neural network verification, built on a fuzzing engine over ONNX and VNN-LIB. Produced a benchmark suite and a relative performance fuzzer that exposed slowdowns in four state-of-the-art solvers.
- Logic Guided Machine Learning: symbolic regression with a neural network proposer and a mathematical reasoning solver in a corrective feedback loop, applied to learning physics equations, symmetries, and conserved quantities.
Publications
- Algorithm Selection for SMT International Journal on Software Tools for Technology Transfer 25(2), 2023
- Meta-Solving for Deep Neural Network Verification Preprint, 2023
- Perspectives on Learning and Reasoning within AI Systems (PhD Thesis) University of Waterloo, 2023
- Pierce: A Testing Infrastructure for Neural Network Verification Tools Preprint, 2023
- Goose: A Meta-Solver for Deep Neural Network Verification SMT Workshop at IJCAR/FLoC 2022, 2022
- Machine Learning for Algorithm Selection + Neuro Symbolic AI Dagstuhl Seminar 22291: Machine Learning and Logical Reasoning, 2022
- Algorithm Selection for SMT Solvers with Network Analysis NetVerify 2021 (with IEEE ICNP), 2021
- BanditFuzz: Fuzzing SMT Solvers with Multi-agent Reinforcement Learning FM 2021, 2021
- Logic Guided Genetic Algorithms (Student Abstract) AAAI 2021, 2021
- MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers TACAS 2021, 2021
- xAI-GAN: Enhancing Generative Adversarial Networks via Explainable AI Systems AAAI 2021 Workshop on Explainable Agency in AI, 2021
- Abstract: BanditFuzz: A Reinforcement-Learning based Performance Fuzzer for SMT Solvers SMT Workshop at IJCAR 2020, 2020
- Abstract: MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers SMT Workshop at IJCAR 2020, 2020
- BanditFuzz: A Reinforcement-Learning Based Performance Fuzzer for SMT Solvers VSTTE 2020, 2020
- Discovering Symmetry Invariants and Conserved Quantities by Interpreting Siamese Neural Networks arXiv 2003.04299, 2020
- LGML: Logic Guided Machine Learning (Student Abstract) AAAI 2020, 2020
- An Algorithm Selection Approach for QF_FP Solvers SMT Workshop at SAT 2019, 2019
- A Propagation Rate Based Splitting Heuristic for Divide-and-Conquer Solvers SAT 2017, 2017