SHF: Small: Efficient, Deterministic and Formally Certified Methods for Solving Low-dimensional Linear Programs with Floating-point Precision

线性规划被广泛应用于计算机算术、机器人学、机器学习、计算机视觉和数据库等众多领域。经过几十年的研究，现有的线性规划解算器已经得到了稳步的改进，可以解决数万个约束。这些解算器专注于约束数量与变量数量相同数量级的线性规划(即，高维线性规划)。然而，在许多领域中，具有数十亿个约束但变量数量较少的线性规划是常见的。这种线性规划被称为“低维线性规划”(LDLP)。不幸的是，现有的LP解算器无法解决这些问题。这个项目的目的是开发高效和确定性的方法来求解低维线性规划，这些方法可以得到形式上的验证，以产生浮点精度的正确解。与使用有理算术生成实数系数的现有LP问题的求解器不同，该项目的新颖性在于使用计算几何的思想生成浮点(FP)精度的解。该项目的影响在于设计可伸缩的LDLP解算器，该解算器既可以处理满秩线性规划(即，存在满足所有约束的单一解)，也可以处理非满秩线性规划，具有潜在的数十亿个约束。在后一种情况下，此项目将生成满足最大约束数量的解决方案。该项目将严格评估LDLP解算器在各个领域的效力，并有可能将形式方法的使用扩大到更广泛的应用类别。它还将教育从业者、研究生和本科生关于计算的基本抽象。这个项目在设计LDLP解算器方面取得了以下基础性进展：(A)它将开发一种算法来求解满级的LDLP，同时识别关键约束。满足这些关键约束的解决方案也满足所有其他约束。(B)通过利用超平面和点之间的几何对偶构造高维凸壳，将开发一种识别关键约束的新方法。(C)它将使用其解满足原始非满秩线性规划中的最大约束数的关键约束来开发新的线性规划公式。(D)它将开发一种方法来正式验证高维凸壳的构造，特别是处理存在数值和舍入误差时可能出现的退化情况，以及(E)它将在两个实际应用中对LDLP求解器进行评估：(1)为初等函数生成正确的舍入数学库，(2)为机器学习快速训练支持向量机。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Linear programs (LPs) are widely used in numerous domains, such as computer arithmetic, robotics, machine learning, computer vision and databases. Existing LP solvers, which have been steadily improved after decades of research, can solve several tens of thousands of constraints. These solvers focus on linear programs where the number of constraints is of the same order of magnitude as the number of variables (i.e., high-dimensional linear programs). However, in many domains, linear programs with billions of constraints but a small number of variables are common. Such linear programs are called "low-dimensional linear programs" (LDLPs). Unfortunately, existing LP solvers cannot solve them. This project aims to develop efficient and deterministic methods to solve low-dimensional linear programs that can be formally verified to produce the correct solution with floating-point precision. In contrast to existing solvers for LP problems that generate real coefficients using rational arithmetic, this project's novelty lies in generating solutions with floating-point (FP) precision using ideas from computational geometry. The project's impacts are in designing scalable LDLP solvers that can handle both linear programs that are full-rank (i.e., there exists a single solution that satisfies all constraints) and those that are not full-rank, with potentially billions of constraints. In the latter case, this project will generate a solution that satisfies the maximum number of constraints. This project will rigorously evaluate the efficacy of the LDLP solver in various domains and has the potential of expanding the use of formal methods to a wider class of applications. It will also educate practitioners, graduate and undergraduate students on foundational abstractions in computing.This project makes the following foundational advances in designing LDLP solvers: (a) It will develop an algorithm to solve LDLPs that are full rank while also identifying the key constraints. A solution that satisfies these key constraints also satisfies all the other constraints. (b) It will develop a novel method for identifying the key constraints by constructing the convex hull in high dimensions using the geometric duality between hyperplanes and points. (c) It will develop a new LP formulation using the key constraints whose solution satisfies the maximum number of constraints in the original non-full-rank LDLP. (d) It will develop an approach to formally verify the construction of the convex hull in high dimensions, especially to handle the degenerate cases that may arise in the presence of numerical and rounding errors, and (e) it will evaluate the LDLP solver in two practical applications: (1) generating correctly rounded math libraries for elementary functions, and (2) fast training of support vector machines for machine learning.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.