CAREER:Program Analyses for Improving Reliability of Probabilistic Software

职业：提高概率软件可靠性的程序分析

• 批准号: 1846354
• 负责人: Sasa Misailovic
• 金额: $ 51.17万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-04-01 至 2025-03-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1846354&HistoricalAwards=false
• 关键词: CAREER; Program; Analyses; Improving; Reliability

Many emerging applications operate on noisy data and make decisions under uncertainty. Probabilistic programming languages represent such computations as programs that operate on random variables and probability distributions. While the existing languages open the world of powerful probabilistic inference even to programmers with limited knowledge of statistics, new techniques need to be developed to improve programmer productivity and simplify debugging of probabilistic software. This project investigates the hypothesis that static program analysis, with its sound and rich symbolic reasoning, is a solid foundation for these techniques. This project will lead to new automated tools to help scientists, engineers, and software developers build reliable and robust probabilistic software. The project will integrate research and education by developing courses based on newly developed ideas, with the goal of empowering future software engineers with solid quantitative reasoning skills.The project will investigate both the foundations of automated relational analysis for probabilistic computations and the practical application of probabilistic analysis to help application programmers and developers of probabilistic programming systems. The project will investigate two impactful relational analyses for probabilistic programs: sensitivity analysis and semantic differencing. The project will develop an ecosystem of techniques that leverage these analyses to identify errors in probabilistic programming systems, improve robustness of probabilistic computations through program transformations, and optimize the performance of applications that operate on noisy data. The benefits and key components of the approach (including flexible abstractions, transformations, and solving mechanisms) will extend to various application domains with inherent randomness.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.

许多新兴应用程序都对噪声数据进行操作，并在不确定的情况下做出决策。概率编程语言将此类计算表示为对随机变量和概率分布进行操作的程序。虽然现有语言甚至为统计知识有限的程序员打开了强大的概率推理世界，但仍需要开发新技术来提高程序员的工作效率并简化概率软件的调试。该项目研究了这样一个假设：静态程序分析及其合理且丰富的符号推理是这些技术的坚实基础。该项目将带来新的自动化工具，帮助科学家、工程师和软件开发人员构建可靠且强大的概率软件。该项目将通过开发基于新发展思想的课程来整合研究和教育，目标是使未来的软件工程师具备扎实的定量推理技能。该项目将研究概率计算的自动关系分析的基础和概率计算的实际应用分析以帮助应用程序员和概率编程系统的开发人员。该项目将研究概率程序的两种有影响力的关系分析：敏感性分析和语义差异。该项目将开发一个技术生态系统，利用这些分析来识别概率编程系统中的错误，通过程序转换提高概率计算的稳健性，并优化处理噪声数据的应用程序的性能。该方法的好处和关键组成部分（包括灵活的抽象、转换和解决机制）将扩展到具有固有随机性的各种应用领域。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力优势和能力进行评估，被认为值得支持。更广泛的影响审查标准。

项目成果

ASTRA: Understanding the practical impact of robustness for probabilistic programs

• 发表时间: 2023
• 作者: Zixin Huang;Saikat Dutta;Sasa Misailovic

Proof transfer for fast certification of multiple approximate neural networks

• DOI: 10.1145/3527319
• 发表时间: 2022-04
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Shubham Ugare;Gagandeep Singh

AquaSense: Automated Sensitivity Analysis of Probabilistic Programs via Quantized Inference

• DOI: 10.1007/978-3-031-45332-8_16
• 发表时间: 2023
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Zitong Zhou;Zixin Huang;Sasa Misailovic

Aloe: verifying reliability of approximate programs in the presence of recovery mechanisms

• DOI: 10.1145/3368826.3377924
• 发表时间: 2020-02
• 期刊: Proceedings of the 18th ACM/IEEE International Symposium on Code Generation and Optimization
• 作者: Keyur Joshi;V. Fernando;Sasa Misailovic

AQUA: Automated Quantized Inference for Probabilistic Programs

AQUA：概率程序的自动量化推理

• DOI: 10.1007/978-3-030-88885-5_16
• 发表时间: 2021
• 期刊: 2021 in Automated Technology for Verification and Analysis
• 作者: Huang, Zixin;Dutta, Saikat;Misailovic, Sasa
• 通讯作者: Misailovic, Sasa