Holophrasm: a neural Automated Theorem Prover for higher-order logic
Daniel P.Z. Whalen Stanford University
Abstract
I propose a system for Automated Theorem Proving in higher order logic using deep learning and eschewing hand-constructed features. Holophrasm exploits the formalism of the Metamath language and explores partial proof trees using a neural-network-augmented bandit algorithm and a sequence-to-sequence model for action enumeration. The system proves 14% of its test theorems from Metamath’s set.mm module.
中文速览
让机器自动证明数学定理一直是难题，尤其是面对高阶逻辑的形式化证明体系。Holophrasm 系统利用 Metamath 形式语言的树状证明结构，将深度学习与树搜索算法相结合：用一个"回报网络"评估证明节点的价值，用"相关性网络"预选有用定理，再用序列到序列的"生成网络"补全证明步骤中未约束的变量替换，整体搜索策略借鉴了围棋 AI 中的 UCT（Upper Confidence Tree）算法。在 Metamath 的 set.mm 数据集上测试，系统成功证明了约 14% 的测试定理，全程无需人工干预，也无需手工设计特征。这项工作首次将序列到序列生成模型引入自动定理证明的动作枚举环节，为纯数据驱动的形式数学自动化提供了可行路径。
原文 arXiv:1608.02644;中英对照 + 大白话阅读 https://aha.fim.ai/paper/1608.02644v2