Tactic Learning and Proving for the Coq Proof Assistant
This work addresses the problem of automating theorem proving for users of interactive proof assistants like Coq, though it is incremental as it builds on prior systems like TacticToe.
The paper tackles automated proof search in the Coq Proof Assistant by using machine learning to predict tactics and generate proofs, achieving a 23.4% accuracy in tactic prediction and proving 39.3% of lemmas automatically, with a combined 56.7% success rate when integrated with CoqHammer.
We present a system that utilizes machine learning for tactic proof search in the Coq Proof Assistant. In a similar vein as the TacticToe project for HOL4, our system predicts appropriate tactics and finds proofs in the form of tactic scripts. To do this, it learns from previous tactic scripts and how they are applied to proof states. The performance of the system is evaluated on the Coq Standard Library. Currently, our predictor can identify the correct tactic to be applied to a proof state 23.4% of the time. Our proof searcher can fully automatically prove 39.3% of the lemmas. When combined with the CoqHammer system, the two systems together prove 56.7% of the library's lemmas.