DeepMath - Deep Sequence Models for Premise Selection

By Geoffrey Irving, Christian Szegedy, Alexander A. Alemi, Niklas Eén, François Chollet, Josef Urban. 2016

263 citations recorded by the source corpus.

We study the effectiveness of neural sequence models for premise selection in automated theorem proving, one of the main bottlenecks in the formalization of mathematics. We propose a two stage approach for this task that yields good results for the premise selection task on the Mizar corpus while avoiding the hand-engineered features of existing state-of-the-art models. To our knowledge, this is the first time deep learning has been applied to theorem proving on a large scale.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Natural Language Processing, Prompting & Reasoning

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 Computational Theory and Mathematics

In Natural Language Processing

In Prompting & Reasoning

Citations in the corpus

Solving Quantitative Reasoning Problems with Language Models (2022, background): “Work on automation of proof assistants and automated theorem provers such as E [26], leanCoP [27], and Vampire [28] has substantially benefited from integration with machine learning methods [29, 30, 31, 32, 33].”
Generative Language Modeling for Automated Theorem Proving (2020, methodology): “DeepMath [26] explored the use of CNNs and RNNs to predict whether a premise is useful to demonstrate a given conjecture, their results were later improved with FormulaNet [27] by the use of graph neural networks, reminiscent of NeuroSAT [28].”
DeepCoder: Learning to Write Programs (2016, methodology): “Very recently, Alemi et al. (2016) used neural sequence models in tandem with an automated theorem prover. Similar to our setup, a neural network component is trained to select premises that the theorem prover can use to prove a theorem. The main differences are in the domains, and that they train o”
Learning Continuous Semantic Representations of Symbolic Expressions (2016, methodology): “However, apart from some notable exceptions (Alemi et al., 2016; Loos et al., 2017; Zaremba et al., 2014), this area has received relatively little attention in machine learning.”
Formal Mathematics Statement Curriculum Learning (2022, methodology): “…we curated and manually formalized a set of math exercises to target miniF2F . miniF2F statements being quite out of distribution compared to the distribution of statements present in mathlib (which typically includes generic theorems and lem-mas but very few exercises), we hypothesized that if…”
Autoformalization with Large Language Models (2022, background): “The revolution of deep learning then kicked off a new wave of interest in the topic starting with DeepMath [1, 33].”
INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving (2020, background): “Their performances have been improved by machine learning [30, 3, 12, 21, 33, 24, 15].”
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics (2023, background): “How to effectively reason over such a large repository of knowledge is an important unsolved problem in applying language models to mathematics [Irving et al., 2016, Wu et al., 2022b, Tworkowski et al., 2022] .”
Learning to Reason in Large Theories without Imitation (2019, methodology): “Neural networks were ﬁrst applied to premise selection for automated theorem proving in Alemi et al. [2016].”
Learning to Represent Programs with Property Signatures (2020, methodology): “Automated Theorem Proving: Synthesizing programs using machine learning is related to the idea of proving theorems using machine learning (Irving et al., 2016).”
Holophrasm: a neural Automated Theorem Prover for higher-order logic (2016, background): “Premise Selection has shown promise as a target for machine-learning techniques [8–10] and more recently deep learning [11] — the first application of deep learning to Automated Theorem Proving.”
An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic (2020, methodology): “The most simple embedding approaches consider the formula as a sequence of characters and use one-hot encodings followed by standard sequence encodings like LSTMs [ Alemi et al. , 2016 ] .”
Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs (2020, methodology): “Various methods have been used for this task, ranging from hand-crafted features and distance functions [21, 35], to classic machine learning methods like Naive Bayes [1, 7, 28], and recently to deep learning based approaches [23, 34].”
Learning to Prove Theorems by Learning to Generate Theorems (2020, methodology): “(2017); Irving et al. (2016); Kaliszyk et al.”
Premise Selection for Theorem Proving by Deep Graph Embedding (2017, methodology): “This is different from prior work on premise selection that directly applies deep networks to sequences of characters or tokens [5, 10].”
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models (2023, methodology): “Selecting useful premises is recognized as a key challenge in theorem proving [23, 24, 45, 46].”