ENIGMA-NG：面向 E 的高效神经与梯度提升推理引导
人工智能
2019-03-11 v1 机器学习
计算机科学中的逻辑
摘要
我们描述了基于饱和的自动定理证明器中子句引导的高效实现，扩展了 ENIGMA 方法。与在第一个 ENIGMA 实现中训练和使用快速线性分类器并配合手动设计特征不同，我们已经开始尝试更复杂的、最先进的机器学习方法，如梯度提升树和递归神经网络。特别是后一种方法在子句评估效率方面提出了挑战，然而，我们表明，将神经评估与 ATP 数据结构的深度集成可以在很大程度上摊销这一成本，并产生具有竞争力的实时结果。这两种方法都在一个包含大量定理证明问题的数据集上进行了评估，并与以前的方法进行了比较。由此产生的方法改进了手动设计的子句引导，提供了在饱和式自动定理证明器中梯度提升和神经子句引导的第一个令人信服的实际应用。
引用
@article{arxiv.1903.03182,
title = {ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E},
author = {Karel Chvalovský and Jan Jakubův and Martin Suda and Josef Urban},
journal= {arXiv preprint arXiv:1903.03182},
year = {2019}
}