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

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

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.