Holophrasm: a neural Automated Theorem Prover for higher-order logic

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.

9 pages, 1 figure

Cited by in corpus (5)

• Generative Language Modeling for Automated Theorem Proving
• Premise Selection for Theorem Proving by Deep Graph Embedding
• Guiding High-Performance SAT Solvers with Unsat-Core Predictions
• From Shallow to Deep Interactions Between Knowledge Representation, Reasoning and Machine Learning (Kay R. Amel group)
• BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving