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

FMiTF：轨道 II：严格且多功能的浮点精度分析和调整

• 批准号: 1918497
• 负责人: Ganesh Gopalakrishnan
• 金额: $ 10万
• 依托单位: University of Utah
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-10-01 至 2021-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1918497&HistoricalAwards=false
• 关键词: FMiTF; Track; II; Rigorous; Versatile

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.

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

项目成果

FLoAT : Framework for Workflow Analysis and Transformation

FLoAT：工作流程分析和转换框架

• 发表时间: 2021
• 期刊: Correctness 2021: Fifth International Workshop on Software Correctness for HPC Applications
• 作者: Jacobson, John;Bentley, Michael;Gopalakrishnan, Ganesh;Ahn, Dong;Lee, Gregory
• 通讯作者: Lee, Gregory

Robustness Analysis of Loop-Free Floating-Point Programs via Symbolic Automatic Differentiation

通过符号自动微分进行无循环浮点程序的鲁棒性分析

• 发表时间: 2021
• 期刊: IEEE Cluster 2021
• 作者: Das, Arnab;Tirpankar, Tanmay;Gopalakrishnan, Ganesh;Krishnamoorthy, Sriram
• 通讯作者: Krishnamoorthy, Sriram