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

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

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.