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 201–250 of 288 papers

TitleStatusHype
Automated Reasoning in Non-classical Logics in the TPTP World—0
Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning—0
BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving—0
Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving—0
BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving—0
BliStrTune: Hierarchical Invention of Theorem Proving Strategies—0
Blocking and Other Enhancements for Bottom-Up Model Generation Methods—0
Can neural networks do arithmetic? A survey on the elementary numerical skills of state-of-the-art deep learning models—0
CD Tools -- Condensed Detachment and Structure Generating Theorem Proving (System Description)—0
Chain-of-Reasoning: Towards Unified Mathematical Reasoning in Large Language Models via a Multi-Paradigm Perspective—0
Conjectures, Tests and Proofs: An Overview of Theory Exploration—0
Consistent CCG Parsing over Multiple Sentences for Improved Logical Reasoning—0
Constrained Training of Neural Networks via Theorem Proving—0
Count-Invariance Including Exponentials—0
COVER: Covering the Semantically Tractable Questions—0
Cross-checking WordNet and SUMO Using Meronymy—0
CSPLib: Twenty Years On—0
DeepAlgebra - an outline of a program—0
DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data—0
Deriving Theorems in Implicational Linear Logic, Declaratively—0
Designing Game of Theorems—0
Efficient Neural Clause-Selection Reinforcement—0
Modelling Value-oriented Legal Reasoning in LogiKEy—0
Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code—0
Enhancing Mathematical Reasoning in Large Language Models with Self-Consistency-Based Hallucination Detection—0
Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method—0
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E—0
EuclidNet: Deep Visual Reasoning for Constructible Problems in Geometry—0
Evaluating an Automata Approach to Query Containment—0
EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages—0
Exploring Length Generalization in Large Language Models—0
Extracting Higher-Order Goals from the Mizar Mathematical Library—0
Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations—0
Faithful Logic Embeddings in HOL -- Deep and Shallow—0
Formal Mathematical Reasoning: A New Frontier in AI—0
Formal Specifications from Natural Language—0
Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically—0
From the String Landscape to the Mathematical Landscape: a Machine-Learning Outlook—0
From Width-Based Model Checking to Width-Based Automated Theorem Proving—0
Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Proving—0
Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs—0
Generative Language Modeling for Automated Theorem Proving—0
Generative Learning of Continuous Data by Tensor Networks—0
GeoGebra Tools with Proof Capabilities—0
GraATP: A Graph Theoretic Approach for Automated Theorem Proving in Plane Geometry—0
Graph2Tac: Online Representation Learning of Formal Math Concepts—0
Graph Contrastive Pre-training for Effective Theorem Reasoning—0
Graph Representations for Higher-Order Logic and Theorem Proving—0
Hammering Mizar by Learning Clause Guidance—0
Hua-Chen New Theory of Economic Optimization—0
Show:102550
← PrevPage 5 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