谷歌论文提出HolStep：一个用于高阶逻辑定理证明的机器学习数据集

项目地址：https://github.com/tensorflow/deepmath/tree/master/holstep_baselines 

论文：HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving

论文地址：https://arxiv.org/abs/1703.00426 

摘要：大型的计算机可以理解的证据由数百万个中间逻辑步骤构成。这些步骤中绝大多数都源自人工的选择和人工引导的、应用于中间目标的启发式方法。到目前为止，机器学习一般还没有被用于过滤或生成这些步骤。在这篇论文中，我们介绍一个基于高阶逻辑（HOL：Higher-Order Logic）的新数据集，其能用于开发新的基于机器学习的定理证明（theorem-proving）策略。我们在 BSD 证书下公开开放了这一数据集。我们提出了多种可以在这个数据集上执行的机器学习任务，并讨论了它们对定理证明的重要性。我们还在一些任务上基准测试了一些简单的基线机器学习模型（包括 logistic 回归、卷积神经网络和循环神经网络）。我们的基线模型的结果表明了将机器学习应用于 HOL 定理证明的潜力。