Projects
MachSMT is an algorithm selection tool for Satisfiability Modulo Theories solvers. MachSMT supports the entirety of the SMT-LIB language. It deploys machine learning methods to construct both empirical hardness models and pairwise ranking comparators (PWCs) over state-of-the-art SMT solvers. Given an input formula in SMT-LIB format, MachSMT leverages these learnt models to output a ranking of solvers based on predicted run time on that formula.
BanditFuzz is a multi-agent reinforcement learning guided performance fuzzing algorithm. BanditFuzz has extensively been considered in the context of Satisfiability Modulo Theories (SMT) solvers. BanditFuzz constructs inputs that expose performance issues in a set of target solvers relative to a set of reference solvers. The banditfuzz tool is the first performance fuzzer that supports the entirety of the theories in the SMT-LIB initiative.
Goose is an upcoming meta-solver for deep neural network verification. Goose’s 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. Using Goose we observe a 47.3% improvement in PAR-2 score across over 800 benchmarks and 13 solvers from VNN-COMP ‘21.
Pierce is an upcoming testing infrastructure for neural network verification. At its core, Pierce implements a fuzzing engine over the Open Neural Network Exchange (ONNX) (version 13) and the VNN-LIB standard. We leverage Pierce to create a diverse benchmark suite for the community. Furthermore, to demonstrate high usability as a testing infrastructure, we build a relative performance fuzzer and use it to expose slowdowns in four state-of-the-art solvers.
Physics is fundamentally about identifying patterns in data and codifying them in mathematical language. A machine learning approach to achieve the same goal is called symbolic regression. While symbolic regression has been around for a long time, there has been some recent efforts to applying it to data to identify patterns and convert it into mathematical expressions. We propose a variation of symbolic regression, wherein, we combine a neural network-based symbolic regression tool with a mathematical reasoning solver in a corrective feedback look (a method we refer to as Logic Guided Machine Learning) and apply it to data to learn mathematical functions and physics equations. We have also done some work on pure symbolic regression (based on neural networks) to learn several symmetries and conserved quantities in physics.