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.