Delta-Complete SMT Solvers for Learning and Optimization Algorithms

可满足模理论（Satisfiability Modulo Theories，简称SMT）是在一个理论中定义的一组决策问题，即一组特定的公理和推理规则。SMT求解器是一种工具，用于确定给定公式是否可满足，如果满足，则为其变量找到有效赋值。否则，将返回已知不能满足的输入公式的子集，从而导致创建反例。通过利用有效性和可满足性之间的关系，有可能验证一组前提p1， p2，…， pn通过检查作为所有前提的连接加上结论的否定而建立的公式的不满足性，得出结论c。如果结果为unsat，则含义得到验证。SMT问题在许多不同的领域都有应用，从程序和协议的形式化验证到图论和组合数学。因此，多年来开发了许多SMT求解器。Z3和CVC5是其中最著名和最常用的。SMT求解器的一个令人兴奋且相对新颖的应用是验证机器学习模型。最近，机器学习工具的使用变得越来越广泛，这一事实引起了人们的兴趣。因此，这类系统的安全性正受到越来越多的关注，特别是在安全关键的情况下，有一种趋势是采用正式验证模型某些属性的方法。一个NN（神经网络）是一组节点层，称为神经元，通过一组在训练阶段变化的权重与前一层和下一层的所有节点连接起来。深度神经网络（DNN）是一种多层的神经网络，通常超过3层。对SMT求解器在dnn验证中的应用的研究已经产生了诸如Reluplex和最近的NeuralSAT等工具。两种求解方法都给出了飞机ACAS避碰系统的实例研究。不幸的是，这个问题是np完全的，最坏的情况是指数的。因此，目标是在尽可能少的妥协的情况下提高求解器的效率。一种方法是允许一个可配置的扰动程度，即delta。这种加速来自于使用更快但容易出错的浮点运算，而不是大多数解算器执行的精确的有理数运算。三角弱化被定义为原始公式的数值松弛。例如，x = 0的δ弱化为|x| <= 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.