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 76–100 of 288 papers

TitleStatusHype
LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data GenerationCode0
MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation—0
APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning—0
Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving—0
Proceedings The 13th International Workshop on Theorem proving components for Educational software—0
The Limits of AI Explainability: An Algorithmic Information Theory Approach—0
Hua-Chen New Theory of Economic Optimization—0
APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries—0
Hierarchical Attention Generates Better ProofsCode0
Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification—0
Reasoning Models Can Be Effective Without Thinking—0
Enhancing Mathematical Reasoning in Large Language Models with Self-Consistency-Based Hallucination Detection—0
Reasoning Under Threat: Symbolic and Neural Techniques for Cybersecurity Verification—0
A Survey on Mathematical Reasoning and Optimization with Large Language ModelsCode0
Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview—0
Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving—0
Efficient Neural Clause-Selection Reinforcement—0
Faithful Logic Embeddings in HOL -- Deep and Shallow—0
Quantum Machine Learning in Precision Medicine and Drug Discovery -- A Game Changer for Tailored Treatments?—0
LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction—0
A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation—0
Activation Steering in Neural Theorem Provers—0
Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs—0
Proving the Coding Interview: A Benchmark for Formally Verified Code Generation—0
BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving—0
Show:102550
← PrevPage 4 of 12Next →
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