FMitF: Track 1: Foundational Approaches for End-to-end Formal Verification of Computational Physics

FMitF：轨道 1：计算物理端到端形式验证的基础方法

• 批准号: 2219997
• 负责人: Jean-Baptiste Jeannin
• 金额: $ 75万
• 依托单位: Regents of the University of Michigan - Ann Arbor
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-10-01 至 2026-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2219997&HistoricalAwards=false
• 关键词: FMitF; Track; Foundational; Approaches; End

Numerical solutions of differential equations are widely used in analysis and design tasks in science and engineering. Examples include modeling climate change, discovering new materials, designing aircraft, and understanding the early universe. This simulation process, however, involves errors arising from a number of sources such as the finiteness of the numerical discretization, potential lack of convergence of algorithms, floating-point arithmetic, and sampling required to quantify uncertainties. The project's novelties are a new formalism to ensure a rigorous handle over errors and uncertainties in numerical methods, and computer-checked proofs of the formalization and applications. The project's impact is a better understanding and quantification of the errors involved in scientific computations, leading to a higher confidence in simulation-informed analysis and design of natural and engineered systems.The current state of the art in numerical analysis relies on paper proofs. In practical implementations, the impact of rounding error is seldom quantified, and even when quantified, not formalized. The interplay with the implementation (C code level and below) is also not clearly assessed. Practitioners use intuitive techniques such as convergence tests and the method of manufactured solutions to manually check the viability of a numerical algorithm. Since these techniques yield necessary yet not sufficient checks, scientists rely on their expertise to guide applications. This work offers the possibility of the user setting a tolerable error threshold, and being assured of achieving it via their implementation in several computational physics tasks. The idea of bounding errors asymptotically is uncommon in formal methods, and will inevitably lead to the development of tools and techniques to better handle asymptotic guarantees in interactive theorem proving. As a side effect, this will expand and consolidate formal-methods libraries handling real arithmetic and limits. This work is expected to be transformational for computational physics, and spur the development of a sub-field at the intersection of formal methods and computational science. The proofs are mechanically checked in an interactive theorem prover using a variety of mathematical results ranging from convergence of functions to floating-point arithmetic and C semantics, thereby using various theories in one proof of correctness. The project creates a new space of physical applications to formal methods researchers, and for computational physicists to derive value from formalizing their programs.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.

微分方程的数值解广泛应用于科学和工程的分析和设计任务中。例子包括模拟气候变化、发现新材料、设计飞机和了解早期宇宙。然而，该模拟过程涉及多种来源产生的误差，例如数值离散化的有限性、算法可能缺乏收敛性、浮点运算以及量化不确定性所需的采样。该项目的新颖之处在于一种新的形式主义，以确保严格处理数值方法中的错误和不确定性，以及形式化和应用的计算机检查证明。该项目的影响是更好地理解和量化科学计算中涉及的错误，从而提高对自然和工程系统的模拟分析和设计的信心。数值分析的当前技术水平依赖于纸质证明。在实际实现中，舍入误差的影响很少被量化，即使量化了，也没有形式化。与实现（C 代码级别及以下）的相互作用也没有明确评估。从业者使用直观的技术（例如收敛测试和制造解决方案的方法）来手动检查数值算法的可行性。由于这些技术产生必要但不充分的检查，科学家依靠他们的专业知识来指导应用。这项工作为用户提供了设置可容忍误差阈值的可能性，并确保通过在多个计算物理任务中实现来实现它。渐近限制误差的想法在形式方法中并不常见，并且将不可避免地导致工具和技术的发展，以更好地处理交互式定理证明中的渐近保证。作为副作用，这将扩展和巩固处理实际算术和限制的形式方法库。这项工作预计将给计算物理学带来变革，并刺激形式方法和计算科学交叉领域的发展。这些证明在交互式定理证明器中使用从函数收敛到浮点算术和 C 语义的各种数学结果进行机械检查，从而在一次正确性证明中使用各种理论。该项目为形式方法研究人员创造了物理应用的新空间，并为计算物理学家从形式化其程序中获取价值。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查进行评估，被认为值得支持标准。