Generating Correctness Proofs with Neural Networks

Understand

Foundational verification allows programmers to build software which has been empirically shown to have high levels of assurance in a variety of important domains.

• However, the cost of producing foundationally verified software remains prohibitively high for most projects,as it requires significant manual effort by highly trained experts.
• In this paper we present Proverbot9001,a proof search system using machine learning techniques to produce proofs of software correctness in interactive theorem provers.
• We demonstrate Proverbot9001 on the proof obligations from a large practical proof project,the CompCert verified C compiler,and show that it can effectively automate what were previously manual proofs,automatically producing proofs for 27.5% of theorem statements in our test dataset, when combined with solver-based tooling.