Collaborative Research: FMitF: Track I: Formally Verified Numerical Methods

当计算机算法计算物理系统的行为时--行星、自动驾驶汽车、火箭、wi-fi天线、药物--一些数学方程无法精确求解。因此，算法可以根据需要精确地逼近答案。数值分析是计算这些算法的精确度的科学。在某种类型的计算中需要的精度越高，计算答案所需的时间就越长。当一个人绝对需要事先知道答案的准确性时，传统的数值方法很难组合成一个完整和可信的解决方案。该项目的创新之处在于(1)将关于数值软件的所有推理集成到一个单一系统中，(2)将从数学到软件代码的所有推理层次连接起来，产生端到端的正确性和精确度保证，以及(3)以数学定理的形式产生这种保证，其证明可以完全自动检查。该项目的广泛意义和重要性既有科学意义，也有经济意义：开发的新方法和工具可以(1)防止通过传统手段诊断可能极其昂贵的软件错误；(2)允许使用更快的算法(当人们现在可以证明它们是准确的)；以及(3)确保安全关键应用中的控制软件的安全性。该项目采用分层的方法来验证数字软件的正确性和准确性--即对程序(不仅仅是算法)进行正式的机器检查证明，除了指令集体系结构的规范外，没有任何假设。研究人员在每个层面上构建、改进和使用适当的工具：用实数证明离散算法；证明浮点算法如何逼近实数算法；推理浮点算法的C程序实现；以及在CoQ证明助手中端到端连接所有证明。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

When computer algorithms calculate the behavior of physical systems -- planets, self-driving cars, rockets, wi-fi antennas, medicines – some of the mathematical equations can't be solved exactly. Thus, the algorithms approximate the answers as precisely as needed. Numerical analysis is the science of calculating how accurate these algorithms are. The more precision is needed in a certain type of computation, the more time it takes to compute the answer. When one absolutely needs to know in advance how accurate the answers will be, traditional numerical methods are hard to combine into a complete and trustworthy solution. This project's novelties are (1) to integrate all the reasoning about numerical software into a single system, (2) to connect all the levels of reasoning, from mathematics down to software code, producing an end-to-end guarantee of correctness and accuracy, and (3) to produce that guarantee in the form of a mathematical theorem whose proof can be checked fully automatically. The project's broader significance and importance are both scientific and economic: the novel methods and tools developed can (1) prevent software bugs that can be extremely expensive to diagnose by conventional means; (2) allow faster algorithms to be used (when one can now prove that they are accurate); and (3) assure the safety of control software in safety-critical applications such as aircraft and vehicle control.The project takes a layered approach to foundational verification of correctness and accuracy of numerical software---that is, formal machine-checked proofs about programs (not just algorithms), with no assumptions except specifications of instruction-set architectures. The researchers build, improve, and use appropriate tools at each layer: proving in the real numbers about discrete algorithms; proving how floating-point algorithms approximate real-number algorithms; reasoning about C program implementation of floating-point algorithms; and connecting all proofs end-to-end in the Coq proof assistant.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.