Delta-Complete SMT Solvers for Learning and Optimization Algorithms

可满足性模理论SMT，简称SMT，是定义在一个理论中的一组决策问题，意味着一组特定的公理和推理规则。SMT求解器是一种工具，用于确定给定公式是否可满足，如果是，则为其变量找到有效赋值。通过利用有效性和可满足性之间的关系，可以通过检查作为所有前提的合取而构建的公式的不可满足性以及结论的否定来验证前提集p1，p2，…，pn是否包含结论c。SMT问题在许多不同的领域都有应用，从程序和协议的形式验证到图论和组合数学。因此，多年来已经开发了许多SMT解算器。Z3和CVC5是最著名和使用最多的。SMT解算器的一个令人兴奋且相对新颖的应用是验证机器学习模型。最近，机器学习工具的使用变得越来越广泛，这一事实引起了人们的兴趣。因此，这类系统的安全性正受到越来越多的关注，特别是在安全关键的情况下，越来越倾向于形式化地验证模型的某些性质。神经网络是一组节点的集合，称为神经元，通过一组在训练阶段改变的权重与上一层和下一层中的所有节点相连。深度神经网络(DNN)是一种具有多层的神经网络，通常超过3层。对SMT求解器用于DNN验证的研究已经产生了Reluplex和最近的NeuralSAT等工具。这两个解算器都给出了一个飞机ACAS防撞系统的案例研究。不幸的是，这个问题是NP完全的，最坏的情况是指数型的。因此，目标是在尽可能少的妥协下提高求解器的效率。一种方法是允许可配置的扰动程度，增量。加速是因为使用了速度更快但容易出错的浮点运算，而不是大多数求解器执行的精确有理运算。将增量弱化定义为对原公式的数值松弛。例如，x=0的增量弱化是|x|&lt；=Delta。注意，如果一个公式是可满足的，那么它的增量弱化总是可满足的。另一种充分利用我们所获得的资源的方法是通过并行化用于确定该公式的可满足性的算法。在处理线性规划时，首先想到的是单纯形。内点法的使用可以代表一种有效的替代方法。我希望找到答案的问题是：能否将算法并行化引入到线性规划问题的验证计算中？虽然单纯形算法的朴素并行化被认为不如专门用于稀疏矩阵的顺序方法，但可能值得研究替代方法，如内点法，并根据输入在运行时评估更改算法的成本。我的工作将使用杰出的Martin Sidaway奠定的基础，他开发了当前版本的Delta完全线性SMT解算器dLinear4。使用Delta完全SMT解算器来验证机器学习和优化算法的性能会带来什么优势？计算ACAS案例研究上的基准将是评估该方法有效性的一个很好的起点。然而，必须考虑三角洲减弱对结果精度的影响。

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.