验证线性规划：通过容差感知的精度提升
Verified Linear Programming through Tolerance-Aware Precision Boosting
另 1 家 · 查看机构详情
- Newcastle University（纽卡斯尔大学）
- University of Birmingham（伯明翰大学）
- MPI-SWS（马克斯·普朗克软件系统研究所）
- Università di Roma “La Sapienza”（罗马大学）
机构由 AI 辅助整理，请以论文原文为准。
浏览论文内容
中文总结 AI 辅助
本文提出容差感知的精度提升单纯形算法，在浮点实现与精确有理数实现间建立可证明的等价条件，并引入delta-完备终止准则，实现带形式保证的线性规划求解。
中文摘要 AI 辅助
线性规划在计算机科学中扮演基础性角色，其应用涵盖优化、形式验证、SMT求解以及众多其他领域。当需要精确性保证时，浮点运算引起的数值不精确可能损害可靠性，而精确有理数运算往往带来显著的计算开销。本文研究了单纯形算法的数值稳定性，并建立了在何种条件下，一种精度提升的浮点实现能够可证明地产生与精确有理数实现相同的枢轴决策和最终基，从而可以精确地重构并验证最终结果。我们的分析表明，正确性既依赖于算术精度，也依赖于对数值容差的谨慎处理。基于这些结果，我们开发了一种具有形式正确性保证的容差感知、精度提升的单纯形算法。最后，我们引入了一个delta-完备的终止准则，允许算法在最优目标函数的认证上界和下界之差不超过用户指定的阈值delta时终止，从而提供经过认证的、用户可控的最优性间隙。
英文摘要
Linear programming plays a fundamental role in computer science, with applications in optimization, formal verification, SMT solving, and numerous other domains. When exactness guarantees are required, numerical inaccuracies arising from floating-point arithmetic can compromise soundness, whereas exact rational arithmetic often incurs significant computational overhead. In this paper, we investigate the numerical stability of the simplex algorithm and establish conditions under which a precision-boosting floating-point implementation provably produces the same pivot decisions and final basis as an exact rational implementation, from which the final result is reconstructed and certified exactly. Our analysis shows that correctness depends on both arithmetic precision and a careful handling of numerical tolerances. Based on these results, we develop a tolerance-aware, precision-boosting simplex algorithm with formal correctness guarantees. Finally, we introduce a delta-complete termination criterion that allows the algorithm to terminate once certified upper and lower bounds on the optimal objective differ by at most a user-specified threshold delta, providing a certified, user-controlled optimality gap.
