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

Code

• github.com/dwhalen/holophrasm
  Officialnone★ 0
• github.com/jinpz/refactor
  pytorch★ 8
• github.com/justin941208/SPIA-Project
  none★ 0
• github.com/giomasce/mmpp
  none★ 0

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.

Tasks

Benchmark Results

Reproductions