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 101–150 of 288 papers

TitleStatusHype
LemmaHead: RAG Assisted Proof Generation Using Large Language Models—0
Chain-of-Reasoning: Towards Unified Mathematical Reasoning in Large Language Models via a Multi-Paradigm Perspective—0
Proof Recommendation System for the HOL4 Theorem Prover—0
HUNYUANPROVER: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving—0
Formal Mathematical Reasoning: A New Frontier in AI—0
Towards Scientific Discovery with Generative AI: Progress, Opportunities, and Challenges—0
WithdrarXiv: A Large-Scale Dataset for Retraction StudyCode0
Improving Multimodal LLMs Ability In Geometry Problem Solving, Reasoning, And Multistep Scoring—0
Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically—0
Learning Rules Explaining Interactive Theorem Proving Tactic PredictionCode0
Alchemy: Amplifying Theorem-Proving Capability through Symbolic MutationCode0
Proof Flow: Preliminary Study on Generative Flow Network Language Model Tuning for Formal Reasoning—0
3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes—0
Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4Code0
Revealed Invariant Preference—0
Artifical intelligence and inherent mathematical difficulty—0
Lean-STaR: Learning to Interleave Thinking and Proving—0
Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agent—0
FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem ProvingCode0
Scaling Synthetic Logical Reasoning Datasets with Context-Sensitive Declarative GrammarsCode0
miniCodeProps: a Minimal Benchmark for Proving Code Properties—0
DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data—0
A Certified Proof Checker for Deep Neural Network Verification in Imandra—0
ATG: Benchmarking Automated Theorem Generation for Generative Language Models—0
Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem ProvingCode0
Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic ProvingCode0
Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry—0
Proceedings 12th International Workshop on Theorem proving components for Educational software—0
Multi-Task Learning with Multi-Task Optimization—0
Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code—0
Learning Guided Automated Reasoning: A Brief Survey—0
BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving—0
A Categorization of Complexity Classes for Information Retrieval and Synthesis Using Natural Logic—0
REFACTOR: Learning to Extract Theorems from ProofsCode0
On the (In)feasibility of ML Backdoor Detection as an Hypothesis Testing ProblemCode0
EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages—0
0-1 laws for pattern occurrences in phylogenetic trees and networks—0
Task Success is not Enough: Investigating the Use of Video-Language Models as Behavior Critics for Catching Undesirable Agent Behaviors—0
Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint SolvingCode0
Graph2Tac: Online Representation Learning of Formal Math Concepts—0
Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method—0
Automated Planning Techniques for Elementary Proofs in Abstract Algebra—0
Large Language Models' Understanding of Math: Source Criticism and Extrapolation—0
Generative Learning of Continuous Data by Tensor Networks—0
math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories—0
TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language ModelsCode0
The Mathematical Game—0
Math Agents: Computational Infrastructure, Mathematical Embedding, and Genomics—0
Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended PreprintCode0
Translating SUMO-K to Higher-Order Set Theory—0
Show:102550
← PrevPage 3 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