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

Daniel Whalen
8/8/2016
cs.AIcs.LO

Official code: dwhalen/holophrasm (56 stars, MIT, last commit 2020-03-26).

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.

View on arXivView PDF

Code Implementations(1)

dwhalen/holophrasmOfficial100%
MIT

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

5612Roff, PythonAug 8, 20166 years agoMIT

Similar Papers

On the Limits of Hierarchically Embedded Logic in Classical Neural Networks

85% match2025

Multi-Step Deductive Reasoning Over Natural Language: An Empirical Study on Out-of-Distribution Generalisation

83% match1 repo102022

The Logical Expressiveness of Topological Neural Networks

81% match2026

Categorical Construction of Logically Verifiable Neural Architectures

81% match2025

Learning higher-order logic programs

81% match2 repos2122019

Cellular automata, many-valued logic, and deep neural networks

81% match2024

Cite this paper

@article{whalen2016holophrasm,
  title  = {Holophrasm: a neural Automated Theorem Prover for higher-order logic},
  author = {Daniel Whalen},
  year   = {2016},
  eprint = {1608.02644},
  archivePrefix = {arXiv},
  url    = {https://arxiv.org/abs/1608.02644}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/1608.02644.svg)](https://codeofpaper.com/paper/1608.02644)

Discussion