Delta-Complete SMT Solvers for Learning and Optimization Algorithms

点击翻译按钮获取中文摘要

Satisfiability Modulo Theories SMT, for short, is a set of decision problems defined within a theory, meaning a specific set of axioms and inference rules. An SMT solver is a tool that determines whether a given formula is satisfiable and, if that is the case, finds a valid assignment for its variables. Otherwise, a subset of the input formula known to be unsatisfiable is returned, leading to the creation of a counterexample.By exploiting the relationship between validity and satisfiability, it is possible to verify if a set of premises p1, p2, ..., pn entails a conclusion c by checking the unsatisfiability of the formula built as a conjunction of all the premises plus the negation of the conclusion. If the result is unsat the implication is verified.SMT problems find their use in many different fields, from formal verification of programs and protocols to graph theory and combinatorial mathematics. Hence, many SMT solvers have been developed over the years. Z3 and CVC5 are among the most renowned and utilized. An exciting and relatively novel application of SMT solvers is verifying machine learning models. The interest arises from the fact that recently, the use of machine learning tools has become more and more widespread. As a result, the safety of such systems is receiving increasing attention, especially in safety-critical situations, with a trend towards approaches that verify some properties of the model formally.A NN (neural network) is a set of layers of nodes, called neurons, connected with all the ones in the previous and next layer through a set of weights that changes during the training phase. A DNN (Deep Neural Network) is a neural network with many layers, typically more than 3.Research on the application of SMT solvers for verification of DNNs has given rise to tools such as Reluplex and, more recently, NeuralSAT. Both solvers present a case study on the ACAS collision avoidance system for aircraft.Unfortunately, the problem is NP-complete, and the worst-case scenario is exponential. Hence, the goal is to improve the solver's efficiency with as little compromise as possible. One approach is to allow for a configurable degree of perturbation, delta. The speedup arises from using faster but error-inducing floating point arithmetic instead of the exact rational operations that most solvers carry out. The delta-weakening is defined as a numerical relaxation of the original formula. For instance, the delta-weakening of x = 0 is |x| <= delta. Note that if a formula is satisfiable, its delta-weakening is always satisfiable.Another way to make the most out of the resources we are given is through the parallelization of the algorithms used to determine the satisfiability of the formula. When dealing with linear programming, the simplex is the first to come to mind. The usage of interior-point methods could represent a valid alternative. The questions I aim to find an answer to are:Can algorithmic parallelization be introduced for verified computation of linear programming problems? While naive parallelization of the simplex algorithm is deemed inferior to sequential approaches specialized for sparse matrices, it may be worth investigating alternative approaches, such as interior-point methods, and evaluating the cost of changing the algorithm at runtime based on the input. My work will use the groundwork laid by the brilliant Martin Sidaway, who developed the current version of the delta complete linear SMT solver dLinear4.What advantages does it bring to employ delta-complete SMT solvers for verifying properties of machine learning and optimization algorithms?Computing the benchmarks on the ACAS case study will be a good starting point to evaluate the approach's effectiveness. However, the impact of the delta-weakening on the precision of the results will have to be considered.