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

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

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.