Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

DeepMath - Deep Sequence Models for Premise Selection

Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban

TL;DR

The paper tackles premise selection for large-scale automated theorem proving by introducing a two-stage neural pipeline that eliminates hand-crafted features. It first learns character-level representations of formulas and then builds word-level embeddings that incorporate symbol definitions, enabling effective axiom conjecture pairing. Empirical results on the Mizar library show that neural approaches can rival and complement traditional hand-engineered methods, with ensembles pushing the prover to auto-prove a substantial fraction of theorems. The work demonstrates the viability of deep learning in formal reasoning tasks and highlights practical gains for theorem-proving pipelines, while outlining avenues for further enhancement.

Abstract

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.

DeepMath - Deep Sequence Models for Premise Selection

TL;DR

The paper tackles premise selection for large-scale automated theorem proving by introducing a two-stage neural pipeline that eliminates hand-crafted features. It first learns character-level representations of formulas and then builds word-level embeddings that incorporate symbol definitions, enabling effective axiom conjecture pairing. Empirical results on the Mizar library show that neural approaches can rival and complement traditional hand-engineered methods, with ensembles pushing the prover to auto-prove a substantial fraction of theorems. The work demonstrates the viability of deep learning in formal reasoning tasks and highlights practical gains for theorem-proving pipelines, while outlining avenues for further enhancement.

Abstract

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.

Paper Structure

This paper contains 15 sections, 1 equation, 6 figures, 1 table.

Table of Contents

  1. Introduction
  2. Formalization and Theorem Proving
  3. Premise Selection, Experimental Setting and Previous Results
  4. Motivation for the use of Deep Learning
  5. Overview of our approach
  6. Stage 1: Character-level models
  7. Stage 2: Word-level models
  8. Experiments
  9. Experimental Setup
  10. Metrics
  11. Network Architectures
  12. Network Training
  13. Experimental Results
  14. Conclusions
  15. Acknowledgments

Figures (6)

  • Figure 1: (top) The final statement of the Mizar formalization of the Jordan curve theorem. (bottom) The translation to first-order logic, using name mangling to ensure uniqueness across the entire corpus.
  • Figure 2: Histograms of statement lengths, occurrences of each word, and statement dependencies in the Mizar corpus translated to first order logic. The wide length distribution poses difficulties for RNN models and batching, and many rarely occurring words make it important to take definitions of words into account.
  • Figure 3: (left) Our network structure. The input sequences are either character-level (section \ref{['char-level']}) or word-level (section \ref{['word-level']}). We use separate models to embed conjecture and axiom, and a logistic layer to predict whether the axiom is useful for proving the conjecture. (right) A convolutional model.
  • Figure 4: Specification of the different embedder networks.
  • Figure :
  • ...and 1 more figures

Theorems & Definitions (1)

  • Definition : Premise selection problem