Delta-Complete SMT Solvers for Learning and Optimization Algorithms

用于学习和优化算法的 Delta-Complete SMT 求解器

• 批准号: 2869702
• 金额: --
• 依托单位: Newcastle University
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2023
• 资助国家: 英国
• 起止时间: 2023 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2869702
• 关键词: Delta; Complete; SMT; Solvers; Learning

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.

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