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

References in corpus (1)

• DeepMath - Deep Sequence Models for Premise Selection

Cited by in corpus (15)

• GamePad: A Learning Environment for Theorem Proving
• Generative Language Modeling for Automated Theorem Proving
• Premise Selection for Theorem Proving by Deep Graph Embedding
• MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
• HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
• Learning to Reason in Large Theories without Imitation
• NaturalProofs: Mathematical Theorem Proving in Natural Language
• Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning
• Learning to Prove Theorems by Learning to Generate Theorems
• Proof Artifact Co-training for Theorem Proving with Language Models
• Premise selection with neural networks and distributed representation of features
• From Shallow to Deep Interactions Between Knowledge Representation, Reasoning and Machine Learning (Kay R. Amel group)
• Guiding High-Performance SAT Solvers with Unsat-Core Predictions
• BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving
• Machine Learning Guidance and Proof Certification for Connection Tableaux