arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2102.09756cs.LGcs.AIcs.LO
收藏

TacticZero:使用深度强化学习从头开始学习证明定理

TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning

Australian National University(澳大利亚国立大学);Data61, CSIRO(澳大利亚联邦科学与工业研究组织Data61部门)

Minchao Wu, Michael Norrish, Christian Walder, Amir Dezfouli

摘要:

我们提出了一种使用深度强化学习的交互式定理证明(ITP)的新方法。所提出的框架能够学习证明搜索策略以及端到端方式的策略和参数预测。我们制定ITP的过程作为一个马尔可夫决策过程(MDP),其中每个状态代表一组潜在的衍生路径。这种结构使我们能够引入一种新的回溯机制,使代理有效地丢弃(预测)死端推导和重新启动有前途的替代品。我们在HOL4定理证明器中实现了该框架。实验结果表明,该框架优于现有的自动定理证明器(即,锤子)在HOL4中可用。我们进一步阐述了使用消融研究的框架的关键组成部分的作用。

英文摘要:

We propose a novel approach to interactive theorem-proving (ITP) using deep reinforcement learning. The proposed framework is able to learn proof search strategies as well as tactic and arguments prediction in an end-to-end manner. We formulate the process of ITP as a Markov decision process (MDP) in which each state represents a set of potential derivation paths. This structure allows us to introduce a novel backtracking mechanism which enables the agent to efficiently discard (predicted) dead-end derivations and restart from promising alternatives. We implement the framework in the HOL4 theorem prover. Experimental results show that the framework outperforms existing automated theorem provers (i.e., hammers) available in HOL4 when evaluated on unseen problems. We further elaborate the role of key components of the framework using ablation studies.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑