Towards Finding Longer Proofs
Towards Finding Longer Proofs
复制标题
寻找更长的证明
DOI：
10.1007/978-3-030-86059-2_10
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
J. Urban
中科院分区：
文献类型：
--
作者：
Zsolt Zombori;Adrián Csiszárik;H. Michalewski;C. Kaliszyk;J. Urban
我们提出了一个基于强化学习(RL)的自动定理证明指导系统，用于发现更长的证明(FLOP)。FLOP侧重于从简短的证明推广到结构相似的较长的证明。为了实现这一点，Flop使用了以前在定理证明中没有应用的最先进的RL方法。特别是，我们表明，在日益困难的算术问题的合成数据集上，课程学习显著优于之前基于学习的证明指导。
We present a reinforcement learning (RL) based guidance system for automated theorem proving geared towards Finding Longer Proofs (FLoP). FLoP focuses on generalizing from short proofs to longer ones of similar structure. To achieve that, FLoP uses state-of-the-art RL approaches that were previously not applied in theorem proving. In particular, we show that curriculum learning significantly outperforms previous learning-based proof guidance on a synthetic dataset of increasingly difficult arithmetic problems.
DOI：
10.1007/s10817-016-9362-8
发表时间：
2016-10-01
期刊：
JOURNAL OF AUTOMATED REASONING
影响因子：
--
作者：
Blanchette, Jasmin Christian;Greenaway, David;Urban, Josef
通讯作者：
Urban, Josef
DOI：
--
发表时间：
2017-09
期刊：
ArXiv
影响因子：
--
作者：
Mingzhe Wang;Yihe Tang;Jian Wang;Jia Deng
通讯作者：
Mingzhe Wang;Yihe Tang;Jian Wang;Jia Deng
DOI：
10.24963/ijcai.2019/373
发表时间：
2019-02
期刊：
ArXiv
影响因子：
--
作者：
Arthur Juliani;A. Khalifa;Vincent-Pierre Berges;Jonathan Harper;Hunter Henry;A. Crespi;J. Togelius;Danny Lange
通讯作者：
Arthur Juliani;A. Khalifa;Vincent-Pierre Berges;Jonathan Harper;Hunter Henry;A. Crespi;J. Togelius;Danny Lange