摘要
基础验证使得程序员能够构建出在多个重要领域中经实证证明具有高度可信度的软件。然而，对于大多数项目而言，构建基础验证软件的成本仍然过高，因为这需要高度训练的专业人员投入大量手动工作。本文提出 Proverbot9001，这是一个基于机器学习技术的证明搜索系统，用于在交互式定理证明器中生成软件正确性的证明。我们在一个大型实际证明项目——CompCert 验证型 C 编译器——的证明需求上验证了 Proverbot9001 的有效性，结果表明，该系统能够有效自动化此前依赖人工完成的证明任务，在结合基于求解器的工具时，可自动为测试数据集中 27.5% 的定理命题生成证明。在不依赖任何额外求解器的情况下，其证明完成率相比此前最先进的 Coq 证明生成机器学习模型实现了 4 倍的提升。