DeepMath - Deep Sequence Models for Premise Selection

2016/06/14 by Alex Alemi, Alex A. Alemi, Alemi, Alex A. +12 · 1 voice · 24 citations
Computer Science · #Topic Modeling #Mathematics, Computing, and Information Processing #Natural Language Processing Techniques

paper · pdf · doi:10.48550/arxiv.1606.04442

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\n to Formal Verification
• Learning to Reason in Large Theories without Imitation

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