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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
