FMiTF: Track II: Rigorous and Versatile Float-Point Precision Analysis and Tuning

浮点数是计算机中最常用的实数值表示形式，例如地球上的全球平均温度。 由于计算机存储单元的精度有限，因此必须遵循电气和电子工程师协会 (IEEE) 颁布的标准舍入规则，对浮点量进行适当舍入。不幸的是，这些舍入规则有时在现有的重要软件中被错误地实现。 在其他情况下，软件转换管道中的关键环节偏离数学规定。 该项目提供了一个名为 FPFormal 的集成工具集，有助于建立数学上严格的舍入误差估计。它可以帮助设计人员准确地确定必须增强转换管道中的哪些环节才能获得可验证的计算结果。这项研究消除或极大地减少了为关键科学决策提供信息的计算结果的偏差。该项目开发的工具将向整个科学界开放，并在促进各级计算教育的教学法方面发挥关键作用。 FPFormal 项目提供了点工具的集成集合，可帮助科学和工程研究人员为其数值计算建立严格的舍入误差界限。其中一些工具采用了由名为“泰勒形式”的新颖想法支持的符号微分，将结果提供给名为 Gelpia 的全局优化器。 FPFormal 中的其他工具将通过不同的分支计算来帮助查明结果偏差的来源。他们还将计算导致最多舍入误差的输入。 FPFormal 将向研究界发布，并在专门针对三个群体的会议和研讨会上进行推广：国家实验室的计算科学家；投资开发数学软件的公司；以及物理学等领域的个人研究人员，在这些领域，计算是探索未知的唯一手段。 研究人员的主要重点是遵守社区开发的 FPBench 等标准，以提供经过严格审查的基准。该项目更广泛的影响是为领域科学和工程研究人员和从业人员提供工具，帮助他们在基础规范允许的情况下选择较低的精度，从而帮助他们使计算软件变得值得信赖并提高能源效率。潜在影响涵盖高性能计算和机器学习。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Floating-point numbers serve as the mostly commonly used representation within computers of real-valued quantities such as the average global temperature on Earth. Since computer storage cells have finite precision, floating-point quantities must be suitably rounded, following standard rounding rules such as promulgated by the Institute of Electrical and Electronics Engineers (IEEE). Unfortunately, these rounding rules are sometimes incorrectly implemented in existing pieces of important software. In other cases, key links in the software transformation pipeline deviate from mathematical stipulations. This project provides an integrated collection of tools called FPFormal that helps establish mathematically rigorous estimates of round-off error. It assists designers pinpoint exactly which links in the transformation pipeline must be enhanced to attain certifiable calculation results. This research eliminates or vastly minimize deviations in calculation results that inform critical scientific decisions. The tools developed in this project will be open to the entire scientific community, and also play a key role in promoting pedagogy at all levels of computing education.The FPFormal project provides an integrated collection of point tools that help researchers in science and engineering establish tight round-off error bounds for their numerical calculations. Some of these tools employ symbolic differentiation supported by a novel idea called Taylor Forms, feeding the results to a global optimizer called Gelpia. Other tools in FPFormal will help pinpoint the sources of result deviations through differently branching computations. They will also compute inputs that cause the most roundoff errors. FPFormal will be released to the research community and promoted at conferences and workshops specifically targeting three groups: computational scientists at national laboratories; companies invested in developing mathematical software; and individual researchers in areas such as Physics where calculations are the only means of exploring the unknown. A major emphasis of the investigators will be to adhere to standards such as FPBench being developed by the community to supply well-vetted benchmarks. Broader impacts of the project are to equip domain science and engineering researchers and practitioners with tools that help them make their computational software trustworthy as well as more energy efficient, by enabling them to choose lower precision whenever the underlying specifications allow. Potential impacts span both high-performance computing and machine learning.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.