用Transformer模型为HOL4推理论证推荐下一步操作
Proof Recommendation System for the HOL4 Theorem Prover
- 基于Transformer模型分析HOL4大量证明案例，学习推理模式
- 根据已用三步以上策略，准确预测下一步最优证明步骤
- 适合形式化验证与自动化证明研究者使用
我们提出一个针对HOL4定理证明器的证明推荐系统。该工具基于专门设计的Transformer模型[2]，从包含大量定理证明的HOL4库中学习证明模式。模型能够根据已执行的证明策略历史，准确预测下一步应使用的策略（证明步骤）。系统通过读取当前至少包含三个策略的证明过程（即当前证明状态），推荐接下来最优化的证明步骤。
原文摘要 · Abstract (English)
We introduce a proof recommender system for the HOL4 theorem prover. Our tool is built upon a transformer-based model [2] designed specifically to provide proof assistance in HOL4. The model is trained to discern theorem proving patterns from extensive libraries of HOL4 containing proofs of theorems. Consequently, it can accurately predict the next tactic(s) (proof step(s)) based on the history of previously employed tactics. The tool operates by reading a given sequence of tactics already used in a proof process (in our case, it contains at least three tactics), referred to as the current proof state, and provides recommendations for the next optimal proof step(s).
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。