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.

线性程序（LPS）广泛用于许多域，例如计算机算术，机器人技术，机器学习，计算机视觉和数据库。经过数十年的研究，现有的LP求解器已稳步改善，可以解决数万个约束。这些求解器专注于线性程序，其中约束数量与变量数量（即高维线性程序）相同。但是，在许多域中，具有数十亿个约束但少数变量的线性程序很常见。这样的线性程序称为“低维线性程序”（LDLP）。不幸的是，现有的LP求解器无法解决它们。 该项目旨在开发有效和确定性的方法来解决低维线性程序，可以正式验证，以产生具有浮点精度的正确解决方案。与现有的求解器相比，使用合理算术产生真实系数的LP问题，该项目的新颖性在于使用计算几何形状的思想生成具有浮点（FP）精度的解决方案。 该项目的影响在于设计可扩展的LDLP求解器，这些求解器可以处理两个完整级别的线性程序（即，存在一个满足所有约束的单个解决方案）和那些不完全级别的解决方案，并具有数十亿个约束。在后一种情况下，该项目将生成满足最大约束数量的解决方案。该项目将严格评估LDLP求解器在各个领域的功效，并有可能将正式方法的使用扩展到更广泛的应用程序类别。它还将教育从业者，研究生和本科生在计算机中的基础摘要。该项目在设计LDLP求解器方面的基础进展：（a）它将开发出一种算法来求解完整排名的LDLP，同时识别关键约束。满足这些关键约束的解决方案也满足了所有其他约束。 （b）它将开发一种新的方法，用于通过使用超平面和点之间的几何双重性在高维度中构造凸壳来识别关键约束。 （c）它将使用关键约束来开发新的LP公式，其解决方案满足原始非满足级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的法定使命，并使用基金会的知识分子优点和更广泛的影响审查标准来评估值得支持。