快与慢的ENIGMA及亲代引导
人工智能
2021-07-16 v1
摘要
我们描述了ENIGMA系统的若干补充，该系统用于引导E自动定理证明器中的子句选择。首先，我们通过添加基于服务器的GPU评估显著加快了它的神经引导。第二个补充的动机来自当前在E和Prover9等系统中使用的基于权重的快速拒绝过滤器。这类系统可以通过训练实现更智能预过滤的ENIGMA快速版本而变得更智能。这产生了可训练的快与慢思维的组合，优于仅快和仅慢的方法。第三个补充基于“由亲代评判子代”，即在产生子句之前可能拒绝一次推理。其动机来自标准进化机制，即在当前种群中产生所有可能后代总是有代价的。这通过不以更昂贵的方法评估所有子句来节省时间，并提供了对生成子句的补充视角。这些方法在一个来自Mizar数学图书馆的大型基准上进行了评估，显示出相对于最先进技术的良好改进。
引用
@article{arxiv.2107.06750,
title = {Fast and Slow Enigmas and Parental Guidance},
author = {Zarathustra Goertzel and Karel Chvalovský and Jan Jakubův and Miroslav Olšák and Josef Urban},
journal= {arXiv preprint arXiv:2107.06750},
year = {2021}
}
备注
23 pages, 11 tables, 1 figure, submitted to FroCoS 2021