DeepMath - Deep Sequence Models for Premise Selection

2016/06/14 by Alex Alemi, Alex A. Alemi, Alemi, Alex A. +12 · 1 voice · 117 citations
Computer Science · Engineering · #Artificial intelligence #Computer science #Deep learning #Engineering #Epistemology #Geography #Machine learning #Mathematics, Computing, and Information Processing #Model selection #Natural Language Processing Techniques #Philosophy #Premise #Scale (ratio) #Selection (genetic algorithm) #Sequence (biology) #Task (project management) #Topic Modeling #cs.AI #cs.LG #cs.LO

paper · pdf · doi:10.48550/arxiv.1606.04442

published in arXiv (Cornell University) (Cornell University)

openalex publication_date 2016/06/14 · arxiv created 2017/01/26 · arxiv updated 2017/01/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Citations

• Neural GPUs Learn Algorithms
• Sentence Pair Scoring: Towards Unified Framework for Text Comprehension

Cited by

• Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs
• PriorProof: A Point-in-Time Measure of Technique Novelty for Formal Proofs
• MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research
• Exploring Depth Generalization in Large Language Models for Solving Recursive Logic Tasks
• Learned Interventions in Lean 4 grind
• Agentic Program Verification
• A Sequential Set Generation Method for Predicting Set-Valued Outputs
• The Uncanny Similarity of Recurrence and Depth
• Foundation of Intelligence: Review of Math Word Problems from Human Cognition Perspective
• Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics
• Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning
• Lean Finder: Semantic Search for Mathlib That Understands User Intents
• Proof Artifact Co-training for Theorem Proving with Language Models
• Elementary Logic in Linear Space
• Non-Parametric Structural Priors for Geometry Theorem Prediction
• An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic
• Handling Open-Vocabulary Constructs in Formalizing Specifications: Retrieval-Augmented Parsing with Expert Knowledge
• Saturation-Driven Dataset Generation for LLM Mathematical Reasoning in the TPTP Ecosystem
• A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
• Hammering Mizar by Learning Clause Guidance
• Solving Formal Math Problems by Decomposition and Iterative Reflection
• Holophrasm: a neural Automated Theorem Prover for higher-order logic
• ML + FV = \heartsuit? A Survey on the Application of Machine Learning to Formal Verification
• Learning to Reason in Large Theories without Imitation
• Generating Symbolic Reasoning Problems with Transformer GANs
• Current Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc -- and We Can Do Better
• Partial Label Learning for Automated Theorem Proving
• Clarifying Before Reasoning: A Coq Prover with Structural Context
• Mathematical Reasoning in Latent Space
• From Shallow to Deep Interactions Between Knowledge Representation, Reasoning and Machine Learning (Kay R. Amel group)
• Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs
• Automated proof synthesis for propositional logic with deep neural networks
• RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation
• MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation
• Combining Symbolic Expressions and Black-box Function Evaluations in Neural Programs
• Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling
• Verifying Security Protocols using Dynamic Strategies
• Combining Axiom Injection and Knowledge Base Completion for Efficient Natural Language Inference
• Hierarchical Attention Generates Better Proofs
• AI for Mathematics: Progress, Challenges, and Prospects
• Vampire With a Brain Is a Good ITP Hammer
• SLDR-DL: A Framework for SLD-Resolution with Deep Learning
• Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification

Discussions

• DeepMath – Deep Sequence Models for Premise Selection [hn, 79 points, 14 comments]

Related

• Premise Selection for Theorem Proving by Deep Graph Embedding
• Premise selection with neural networks and distributed representation of features
• A Survey on Deep Learning for Theorem Proving
• Graph Sequence Learning for Premise Selection
• Deep Network Guided Proof Search