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

合作研究：FMitF：第一轨：形式验证的数值方法

• 批准号: 2219758
• 负责人: David Bindel
• 金额: $ 19.05万
• 依托单位: Cornell University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-10-01 至 2025-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2219758&HistoricalAwards=false
• 关键词: Collaborative; Research; FMitF; Track; Formally

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.

当计算机算法计算物理系统（行星、自动驾驶汽车、火箭、Wi-Fi 天线、药物）的行为时，一些数学方程无法精确求解，因此，算法会根据需要精确地近似答案。数值分析是一门计算这些算法的精确度的科学，当人们绝对需要提前知道答案的精确度时，需要的精度越高，计算答案所需的时间就越多。传统数值方法难以结合该项目的新颖之处在于（1）将有关数值软件的所有推理集成到一个系统中，（2）连接从数学到软件代码的所有推理级别，产生端到端的解决方案。 -最终保证正确性和准确性，以及（3）以数学定理的形式产生这种保证，其证明可以完全自动检查该项目的更广泛的意义和重要性既是科学的又是经济的：开发的新颖方法和工具可以。 (1) 防止软件错误通过传统方法进行诊断的成本极其高昂；(2) 允许使用更快的算法（现在可以证明它们是准确的）；(3) 确保飞机和车辆等安全关键应用中控制软件的安全性；该项目采用分层方法对数值软件的正确性和准确性进行基础验证，即对程序（不仅仅是算法）进行正式的机器检查证明，除了指令集架构的规范之外没有任何假设。在每一层构建、改进和使用适当的工具：证明关于离散算法的实数；证明浮点算法如何逼近实数算法；以及在 Coq 证明助手中端到端连接所有证明。使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。