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

SHF：小型：用于以浮点精度求解低维线性程序的高效、确定性且经过正式认证的方法

• 批准号: 2312220
• 负责人: Mridul Aanjaneya
• 金额: $ 54万
• 依托单位: Rutgers University New Brunswick
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-07-01 至 2026-06-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2312220&HistoricalAwards=false
• 关键词: SHF; Small; Efficient; Deterministic; Formally

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.

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