Context-aware Generation of Proof Scripts for Theorem Proving

摘要

Formal verification is a trustable method to produce correct, safe, and fast code. However, the cost of formal verification remains prohibitively high for most projects, as it requires significant manual effort by highly trained experts. In this paper, we propose a novel approach to proof automation in Coq that generates proof script based on context-awareness. We develop AutoMagic, an automatic theorem proving framework, which can use the generated proof script to achieve a fully automatic proof of the theorem. Our method is simple but pushes the limits of automatic proof. The performance of AutoMagic is evaluated in the Coq standard library. We show that 37.87% of the theorems can be proved in a push-button mode, and can be used to prove new theorems not previously provable by automated methods.