SHF: Medium: Generating Correctness Proofs with Neural Networks

软件中的错误可能导致灾难性的后果，从停电到股市崩盘，从大量私人消费者数据泄露到大规模的软件漏洞。使软件更可靠的一个有前途的方法是基础验证。在这种方法中，程序员使用定理证明器来陈述和证明程序的属性。因为证明是在定理证明者的帮助下完成的，在完整的细节中，基础验证提供了最强的保证级别，实际上保证了软件的正确工作。然而，虽然基础验证显示出巨大的希望，但是对于大多数程序来说，生产基础验证软件的成本仍然高得令人望而却步，因为它需要由训练有素的专家进行大量的手工工作。基础验证中需要的手工工作是广泛采用这种有前途的技术的主要障碍之一。该项目的目标是使用机器学习来显著减轻在基础验证中完成证明所需的人工工作量，从而从根本上重塑使用该方法的成本/收益分析。智力上的优点包括在当前的证明上训练机器学习算法，以自动预测未来证明中需要采取的步骤。通过为使用基础验证的成本/收益分析的重大转变奠定基础，该项目有可能迎来一个增加采用该技术的新时代，并因此带来更安全、更可靠的软件。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.