论文标题
COQ证明助手的战术学习和证明
Tactic Learning and Proving for the Coq Proof Assistant
论文作者
论文摘要
我们提出了一个系统，该系统利用机器学习在COQ证明助手中进行战术证明搜索。与Hol4的Tactictoe项目相似，我们的系统可以预测适当的战术，并以战术脚本的形式找到证据。为此，它可以从以前的战术脚本以及如何将其应用于证明状态中学习。系统的性能在COQ标准库中评估。当前，我们的预测指标可以确定适用于证明状态的正确策略，有23.4％的时间。我们的证明搜索者可以完全自动证明39.3％的引理。当与Coqhammer系统结合使用时，两个系统共同证明了图书馆的引理的56.7％。
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.
