用循环神经网络引导连接表aux证明中的推理
人工智能
2020-04-10 v2 机器学习
计算机科学中的逻辑
神经与进化计算
机器学习
摘要
我们提出一个数据集并开展实验，将循环神经网络（RNNs）应用于连接表aux证明演算中的子句选择引导。该 RNN 将来自部分证明树当前分支的字面量序列编码为隐藏向量状态；系统利用它选择用于扩展证明树的子句。我们描述了训练数据与学习设置，并讨论结果且与使用梯度提升树的最先进方法进行比较。此外，我们进行了一项猜想实验，其中 RNN 不仅选择已有子句，还完整构造下一个表aux目标。
引用
@article{arxiv.1905.07961,
title = {Guiding Inferences in Connection Tableau by Recurrent Neural Networks},
author = {Bartosz Piotrowski and Josef Urban},
journal= {arXiv preprint arXiv:1905.07961},
year = {2020}
}