一句话：提出 Diva，通过训练多样化的证明脚本模型并结合搜索，显著提升 Coq 定理的自动证明率。
交互式定理证明器（如 Coq）的证明脚本编写仍高成本且困难。已有自动证明工具单独证明率有限但互补。论文洞察：控制机器学习学习过程可产生多样化模型；因证明合成有定理证明器作为可靠 oracle，多样性可增强搜索。作者提出 Diva，复用 TacTok 与 ASTactic 的搜索机制，并探索九个多样性维度。在 122 个开源项目的 68K 定理上，Diva 自动证明 21.7%，较 TacTok、ASTactic 分别提升 68%、77%；与 CoqHammer 互补额外证明 781 个，其中 364 个此前无工具自动证明，合计证明率达 33.8%。另优化使执行提速 40 倍。
Formally verified correctness is one of the most desirable properties of software systems. But despite great progress made via interactive theorem provers, such as Coq, writing proof scripts for verification remains one of the most effort-intensive (and often prohibitively difficult) software development activities. Recent work has created tools that automatically synthesize proofs or proof scripts. For example, CoqHammer can prove 26.6% of theorems completely automatically by reasoning using precomputed facts, while TacTok and ASTactic, which use machine learning to model proof scripts and then perform biased search through the proof-script space, can prove 12.9% and 12.3% of the theorems, respectively. Further, these three tools are highly complementary; together, they can prove 30.4% of the theorems fully automatically. Our key insight is that control over the learning process can produce a diverse set of models, and that, due to the unique nature of proof synthesis (the existence of the theorem prover, an oracle that infallibly judges a proof's correctness), this diversity can significantly improve these tools' proving power. Accordingly, we develop Diva, which uses a diverse set of models with TacTok's and ASTactic's search mechanism to prove 21.7% of the theorems. That is, Diva proves 68% more theorems than TacTok and 77% more than ASTactic. Complementary to CoqHammer, Diva proves 781 theorems (27% added value) that CoqHammer does not, and 364 theorems no existing tool has proved automatically. Together with CoqHammer, Diva proves 33.8% of the theorems, the largest fraction to date. We explore nine dimensions for learning diverse models, and identify which dimensions lead to the most useful diversity. Further, we develop an optimization to speed up Diva's execution by 40X. Our study introduces a completely new idea for using diversity in machine learning to improve the power of state-of-the-art proof-script synthesis techniques, and empirically demonstrates that the improvement is significant on a dataset of 68K theorems from 122 open-source software projects.
DOI 原文 ·
@inproceedings{paperbot6915,
title = {Diversity-driven automated formal verification},
author = {Emily First and Yuriy Brun},
booktitle = {ICSE},
year = {2022},
doi = {10.1145/3510003.3510138}
}