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. Without any additional solvers,we exhibit a proof completion rate that
is a 4X improvement over prior state-of-the-art machine learning models for
generating proofs in Coq.

本文提出了一个使用机器学习技术的证明搜索系统 Proverbot9001，它能够自动化之前需要手动完成的证明，有效地产生了 27.5% 的证明陈述，在 Coq 中产生了 4 倍的提高。