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

By Daniel Whalen. 2016

58 citations recorded by the source corpus.

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.

Subfields: Artificial Intelligence, Program Analysis & Verification

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Program Analysis & Verification

Citations in the corpus

Generative Language Modeling for Automated Theorem Proving (2020, methodology): “Holophrasm [35] and MetaGen-IL [25] propose RNN-based models to generate proofs for Metamath (the formal system we focus on).”
A Survey of Deep Learning for Mathematical Reasoning (2022, unknown): “, 2016) TP Classification CNN CNN - 7 The first deep large scale theorem prover Holophrasm (Whalen, 2016) TP Classification BiGRU BiGRU - 7 A neural prover for higher-order logic CNNTP (Loos et al.”
GamePad: A Learning Environment for Theorem Proving (2018, background): “Holphrasm (Whalen, 2016) uses string encodings of proof states and focuses on tactic argument synthesis (there is essentially only one tactic in the underlying ITP MetaMath (Megill, 2007)).”
Proof Artifact Co-training for Theorem Proving with Language Models (2021, methodology): “Holophrasm (Whalen, 2016), MetaGen (Wang & Deng, 2020), and GPT-f (Polu & Sutskever, 2020) all use RNNs or Transformers to generate proof steps.”
Deep Network Guided Proof Search (2017, background): “Whalen (2016) proposed a complete neural network based theorem prover architecture leveraging GRU (Chung et al., 2015) networks to guide the proof search of a tableau style proof process for the MetaMath system (Megill, 2007).”
Learning to Reason in Large Theories without Imitation (2019, background): “There are a few automated theorem provers that based on reinforcement learning: Whalen [2016], Kaliszyk et al. [2018] and Zombori et al. [2019], but premise selection tends to be done by ad-hoc, hand engineered mechanisms.”
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics (2021, methodology): “…for theorem proving, language models are not a mandatory approach for Olympiad problems and this assumption is not reﬂected in miniF2F , preserving the generality and widespread applicability of the benchmark to systems similar to DeepHOL (Bansal et al., 2019a) or Holophrasm (Whalen, 2016).”
NaturalProofs: Mathematical Theorem Proving in Natural Language (2021, methodology): “others use the Coq [19, 48], Metamath [44, 42, 30], Isabelle [24], or Lean [14, 49] environments.”
Reinforcement Learning of Theorem Proving (2018, methodology): “This has been done in the connection tableau setting [48, 20, 10], saturation style setting [16, 30], and also as direct automation inside interactive theorem provers [12, 14, 49].”
Premise Selection for Theorem Proving by Deep Graph Embedding (2017, methodology): “Whalen [23] uses GRU networks to guide the exploration of partial proof trees, with formulas represented as sequences of tokens.”
Learning to Prove Theorems by Learning to Generate Theorems (2020, methodology): “same protocol of Whalen (2016) (more details in Appendix D.2) and report the number of theorems proved.”
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version) (2019, background): “Whalen [21] proposed a purely deep reinforcement learning based solution for theorem proving for the Metamath prover [22].”
HyperTree Proof Search for Neural Theorem Proving (2022, methodology): “Another similar approach, Holophrasm [12], uses a different tree-search algorithm while others [13, 14] learn the search policy along with the tactic model.”