SOTAVerified

Automated Theorem Proving

The goal of Automated Theorem Proving is to automatically generate a proof, given a conjecture (the target theorem) and a knowledge base of known facts, all expressed in a formal language. Automated Theorem Proving is useful in a wide range of applications, including the verification and synthesis of software and hardware systems.

Source: Learning to Prove Theorems by Learning to Generate Theorems

Papers

Recently AddedMost HypedMost ActiveNeeds VerificationMost Verified

Showing 151–200 of 288 papers

TitleStatusHype
Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving—0
Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)—0
Social Network Processes in the Isabelle and Coq Theorem Proving Communities—0
TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning—0
Task Success is not Enough: Investigating the Use of Video-Language Models as Behavior Critics for Catching Undesirable Agent Behaviors—0
TextGraphs-16 Natural Language Premise Selection Task: Zero-Shot Premise Selection with Prompting Generative Language Models—0
The Horn Non-Clausal Class and its Polynomiality—0
The Limits of AI Explainability: An Algorithmic Information Theory Approach—0
The Mathematical Game—0
Theorem Proving Based on Semantics of DNA Strand Graph—0
The Role of Entropy in Guiding a Connection Prover—0
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers—0
Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving—0
Towards a Geometry Automated Provers Competition—0
Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agent—0
Towards Concise, Machine-discovered Proofs of Gödel's Two Incompleteness Theorems—0
Towards Evolutionary Theorem Proving for Isabelle/HOL—0
Towards Formal Fault Tree Analysis using Theorem Proving—0
Towards Machine Learning Induction—0
Towards Neural Theorem Proving at Scale—0
Towards Scientific Discovery with Generative AI: Progress, Opportunities, and Challenges—0
Towards United Reasoning for Automatic Induction in Isabelle/HOL—0
Training a First-Order Theorem Prover from Synthetic Data—0
Translating SUMO-K to Higher-Order Set Theory—0
Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers—0
Verifier Theory and Unverifiability—0
Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview—0
0-1 laws for pattern occurrences in phylogenetic trees and networks—0
Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry—0
MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation—0
3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes—0
A Categorization of Complexity Classes for Information Retrieval and Synthesis Using Natural Logic—0
A Certified Proof Checker for Deep Neural Network Verification in Imandra—0
A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation—0
Activation Steering in Neural Theorem Provers—0
A Curious New Result of Resolution Strategies in Negation-Limited Inverters Problem—0
Adversarial Learning to Reason in an Arbitrary Logic—0
Analysis of Algorithms and Partial Algorithms—0
An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic—0
Anti-unification and Generalization: A Survey—0
APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries—0
APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning—0
Applying Second-Order Quantifier Elimination in Inspecting Gödel's Ontological Proof—0
Artifical intelligence and inherent mathematical difficulty—0
Artificial Neural Networks that Learn to Satisfy Logic Constraints—0
A state vector algebra for algorithmic implementation of second-order logic—0
A Study of Continuous Vector Representationsfor Theorem Proving—0
ATG: Benchmarking Automated Theorem Generation for Generative Language Models—0
Autoformalization with Large Language Models—0
Automated Planning Techniques for Elementary Proofs in Abstract Algebra—0
Show:102550
← PrevPage 4 of 6Next →
All datasetsminiF2F-testminiF2F-validHolStep (Conditional)HOList benchmarkHolStep (Unconditional)Metamath set.mmminiF2F-curriculumCompCertCoqGym

Benchmark Results

#ModelMetricClaimedVerifiedStatus
1Kimina-Prover-Previewcumulative80.74—Unverified
2ProofAugcumulative66—Unverified
3DeepSeek-Prover-V1.5cumulative63.5—Unverified
4Subgoal-XLcumulative56.1—Unverified
5DeepSeek-Provercumulative52—Unverified
6Lyra + GPT-4cumulative47.1—Unverified
7LEGO-Prover ChatGPTcumulative47.1—Unverified
8Decomposing the Enigmacumulative45.5—Unverified
9Evaristecumulative41—Unverified
10Evariste-7dcumulative40.6—Unverified
#ModelMetricClaimedVerifiedStatus
1EvaristePass@6458.6—Unverified
2LEGO-Prover ChatGPTPass@10057—Unverified
3Lyra + GPT-4Pass@10052—Unverified
4Evariste-7dPass@6447.5—Unverified
5GPT-fPass@6447.3—Unverified
6Evariste-1dPass@6446.7—Unverified
7DSP (62B Minerva informal)Pass@10043.9—Unverified
8Lean GPT-fPass@829.3—Unverified
9Lean tidyPass@116.8—Unverified
10Metamath GPT-fPass@82—Unverified
#ModelMetricClaimedVerifiedStatus
1MPNN-DagLSTMClassification Accuracy0.92—Unverified
2FormulaNetClassification Accuracy0.9—Unverified
3FormulaNet-basicClassification Accuracy0.89—Unverified
4Siamese 1D CNN-LSTMClassification Accuracy0.83—Unverified
5Siamese 1D CNNClassification Accuracy0.82—Unverified
#ModelMetricClaimedVerifiedStatus
14-hop GNN, sub-expression sharingPercentage correct49.95—Unverified
2Tactic Dependent LoopPercentage correct38.88—Unverified
3BoW2 (extra -ves)Percentage correct36.55—Unverified
4Deeper Wider WaveNetPercentage correct32.65—Unverified
#ModelMetricClaimedVerifiedStatus
1FormulaNetClassification Accuracy0.9—Unverified
2FormulaNet-basicClassification Accuracy0.89—Unverified
31D CNNClassification Accuracy0.83—Unverified
41D CNN-LSTMClassification Accuracy0.83—Unverified
#ModelMetricClaimedVerifiedStatus
1EvaristePass@3272.4—Unverified
2GPT-fPercentage correct56.2—Unverified
3MetaGen-IL + HolophrasmPercentage correct22.1—Unverified
4HolophrasmPercentage correct14.3—Unverified
#ModelMetricClaimedVerifiedStatus
1Evariste-7dPass@6442.5—Unverified
2Evariste-1dPass@6433.6—Unverified
3EvaristePass@6432.1—Unverified
4GPT-fPass@6430.6—Unverified
#ModelMetricClaimedVerifiedStatus
1Proverbot9001Percentage correct19.36—Unverified
2CoqGym/ASTacticPercentage correct4.99—Unverified
#ModelMetricClaimedVerifiedStatus
1ASTacticPercentage correct12.2—Unverified