Meta-Solving via Machine Learning for Automated Reasoning
Loading...
Date
2024-05-30
Authors
SCOTT, JOSEPH
Journal Title
Journal ISSN
Volume Title
Publisher
University of Waterloo
Abstract
Automated reasoning (AR) and machine learning (ML) are two of the foundational pillars of artificial intelligence (AI) and yet have developed largely independently. The integration of these two sub-fields holds the tremendous potential to address problems that are otherwise difficult to solve, especially in the context of logic solvers, which are blackbox deductive reasoning engines designed to tackle NP-Hard problems. The early 2000s witnessed a `silent revolution' leading to the emergence of highly efficient boolean satisfiability (SAT), satisfiability modulo theories (SMT), and mixed-integer linear programming (MILP) solvers, capable of scaling to hundreds of millions of variables and being deployed billions of times daily in various industries. These advancements were primarily due to novel symbolic reasoning techniques as well as the use of ML in solvers. Building on previous successes, this thesis presents several advances in the use of ML in solvers.
A particular way of characterizing the value of using ML in the context of automated reasoning tools is the following: under widely believed complexity-theoretic assumptions, we do not expect any one solver or even a fixed sequence of solvers to perform well on all classes of instances. In fact, there is considerable empirical support for the aforementioned observation. Hence, it is reasonable for us to research methods that enable solver users to adaptively select a (sequence of) solver(s) for any given instance. ML provides a promising means to realize such (adaptive) algorithm selection methods.
We make the following contributions in this thesis: First, inspired by the success of the algorithm selection tool SATZilla for SAT solvers, we present the design and implementation of MachSMT, an algorithm selection tool for SMT solvers. MachSMT supports the entirety of the SMT-LIB and leverages ML over state-of-the-art SMT solvers. We provide empirical evidence for the value of algorithm selection and efficacy of MachSMT over three broad SMT usage scenarios, namely, solver selection for instances obtained from SMT-COMP (an annual competition for SMT solvers), configuration selection for a given solver (cvc5) over a large industrial benchmark suite, and finally for solver selection for a specific domain (network verification).
Second, we present the design and implementation of a novel adaptive algorithm selection tool (aka, a {\it meta-solver}), called \goose, for neural network verification solvers, a class of tools aimed at improving the trustworthiness of ML systems. Traditional algorithm selection tools (e.g., MachSMT) typically tend to be non-adaptive, i.e., once a solver is selected for a given instance this selection is not changed at runtime. By contrast, a key novelty here is that \goose implements an {\it adaptive} sequential portfolio, i.e., it calls a set of subsolvers in a sequence, wherein the order in which subsolvers are called is determined adaptively based on information from their online and offline performance histories. We have implemented a variety of complete and incomplete subsolvers in \goose (in addition to using a set of off-the-shelf ones), and the following synergizing techniques to implement its adaptive sequential portfolio: algorithm selection, probabilistic satisfiability inference, and time-iterative deepening.
Additionally, in the spirit of improving solver performance via ML techniques, we present \banditfuzz, an RL algorithm for relative performance fuzzing of solvers. While \machsmt and \goose leverage supervised learning to make solvers faster, \banditfuzz leverages RL to search for performance issues in solvers. \banditfuzz searches for short problem instances for which a set of target solvers is under-performant, while a set of reference solvers is performant. Such instances expose performance issues in solvers, and are often caused by solver developer errors (e.g., missing rewrite rules, errors in heuristics, etc.). We additionally introduce \pierce, a versatile and extensible testing tool aimed at solvers for the neural network verification (NNV) problem. At its core, \pierce implements a fuzzing engine over the Open Neural Network Exchange (ONNX) -- a standardized model format for deep learning and classical ML, and VNN-LIB -- a specification standard over the input-output behavior of ML systems. \pierce supports the entirety of the VNN-LIB and most of ONNX v18.
Description
Keywords
Constraint Solving, AI, Verification, Machine Learning, Formal Methods, Neural Networks