DeepMath - 用于前提选择的深度序列模型
人工智能
2017-01-30 v2 机器学习
计算机科学中的逻辑
摘要
我们研究了神经序列模型在自动定理证明中前提选择的有效性，前提选择是数学形式化的主要瓶颈之一。我们针对该任务提出了一种两阶段方法，在Mizar语料库的前提选择任务上取得了良好的结果，同时避免了现有SOTA模型中的人工设计特征。据我们所知，这是深度学习首次大规模应用于定理证明。
引用
@article{arxiv.1606.04442,
title = {DeepMath - Deep Sequence Models for Premise Selection},
author = {Alex A. Alemi and Francois Chollet and Niklas Een and Geoffrey Irving and Christian Szegedy and Josef Urban},
journal= {arXiv preprint arXiv:1606.04442},
year = {2017}
}