SHF: Medium: Generating Correctness Proofs with Neural Networks

SHF：中：使用神经网络生成正确性证明

• 批准号: 1955457
• 负责人: Sorin Lerner
• 金额: $ 120万
• 依托单位: University of California-San Diego
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-07-01 至 2025-06-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1955457&HistoricalAwards=false
• 关键词: SHF; Medium; Generating; Correctness; Proofs

Errors in software can lead to disastrous consequences, from power outages to stock market crashes, and from massive leaks of private consumer data to wide-scale software vulnerabilities. A promising approach to making software more reliable is foundational verification. In this approach programmers use a theorem prover to state and prove properties about their programs. Because the proofs are done with the assistance of a theorem prover, in full complete detail, foundational verification provides the strongest possible levels of assurance, virtually guaranteeing that the software works correctly. However, while foundational verification shows great promise, the cost of producing foundationally verified software remains prohibitively high for most programs, as it requires enormous manual effort by highly trained experts. The manual effort required in foundational verification is one of the main impediments to the broader adoption of this promising technique.The goal of this project is to use machine learning to significantly alleviate the manual effort required to complete proofs in foundational verification, thereby fundamentally reshaping the cost/benefit analysis of using the methodology. The intellectual merit involves training machine-learning algorithms on current proofs to automatically predict the steps that need to be taken in future proofs. By laying the foundation for a significant shift in the cost/benefit analysis of using foundational verification, this project has the potential of ushering in an new era of increased adoption of the technique, and of safer and more secure software as a result.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 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Just-in-time learning for bottom-up enumerative synthesis

自下而上的枚举综合的即时学习

• DOI: 10.1145/3428295
• 发表时间: 2020
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Barke, Shraddha;Peleg, Hila;Polikarpova, Nadia
• 通讯作者: Polikarpova, Nadia

Regex+: Synthesizing Regular Expressions from Positive Examples

Regex：从正例合成正则表达式

• 发表时间: 2022
• 期刊: 11TH Workshop on Synthesis
• 作者: Pertseva, Elizaveta;Barbone, Mark;Rudek, Joey;Polikarpova, Nadia
• 通讯作者: Polikarpova, Nadia

Generating correctness proofs with neural networks

使用神经网络生成正确性证明

• DOI: 10.1145/3394450.3397466
• 发表时间: 2020
• 期刊: 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languagesu
• 作者: Sanchez-Stern, Alex;Alhessi, Yousef;Saul, Lawrence;Lerner, Sorin
• 通讯作者: Lerner, Sorin

Data-driven lemma synthesis for interactive proofs

用于交互式证明的数据驱动引理合成

• DOI: 10.1145/3563306
• 发表时间: 2022
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Sivaraman, Aishwarya;Sanchez-Stern, Alex;Chen, Bretton;Lerner, Sorin;Millstein, Todd
• 通讯作者: Millstein, Todd