全息语：一种用于高阶逻辑的神经自动定理证明器

我提出了一种在高阶逻辑中使用深度学习进行自动定理证明的系统，该系统避免了手工构建特征。Holophrasm 利用了 Metamath 语言的形式化特性，并使用神经网络增强的多臂赌博机算法和序列到序列模型来探索部分证明树。该系统能够从 Metamath 的 set.mm 模块中证明 14% 的测试定理。