Generating correctness proofs with neural networks
Generating correctness proofs with neural networks
复制标题
使用神经网络生成正确性证明
DOI：
10.1145/3394450.3397466
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Lerner, Sorin
中科院分区：
文献类型：
--
作者：
Sanchez-Stern, Alex;Alhessi, Yousef;Saul, Lawrence;Lerner, Sorin
基础验证允许程序员构建软件，这些软件已被经验证明在各种重要领域具有高水平的保证。然而，对大多数项目来说，生产经过基础验证的软件的成本仍然高得令人望而却步，因为它需要训练有素的专家进行大量的手工工作。在本文中，我们提出了Proverbot9001，证明搜索系统，使用机器学习技术，以产生软件的正确性证明，在交互式定理证明。我们展示了Proverbot9001的证明义务，从一个大型的实际证明项目，CompCert验证的C编译器，并表明它可以有效地自动化什么是以前的手动证明，自动生成证明28%的定理语句在我们的测试数据集，结合基于求解器的工具。在没有任何额外的求解器的情况下，我们展示了一个证明完成率，这是一个比现有的最先进的机器学习模型在Coq中生成证明提高了4倍。
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 28% 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.
登录
查看更多内容
ACL2(ml)：ACL2 的机器学习
影响因子：
--
作者：
Heras J
通讯作者：
Heras J
通过与证明助手交互学习证明定理
DOI：
--
发表时间：
2019
期刊：
International Conference on Machine Learning
影响因子：
--
作者：
Yang, Kaiyu;Deng, Jia
通讯作者：
Deng, Jia
CompCert：集成和鉴定经过形式验证的优化编译器的实践经验
DOI：
--
发表时间：
2018
期刊：
影响因子：
--
作者：
Daniel Kästner;J. Barrho;Ulrich Wünsche;Marc Schlickling;Bernhard Schommer;Michael Schmidt;C. Ferdinand;X. Leroy;Sandrine Blazy
通讯作者：
Sandrine Blazy
DOI：
10.1007/s10817-018-9458-4
发表时间：
2018
期刊：
Journal of automated reasoning
影响因子：
--
作者：
Czajka Ł;Kaliszyk C
通讯作者：
Kaliszyk C
影响因子：
3.4
作者：
Ekaterina Komendantskaya;Jónathan Heras;G. Grov
通讯作者：
Ekaterina Komendantskaya;Jónathan Heras;G. Grov