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
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
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
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 CNN-LSTMClassification Accuracy0.83—Unverified
41D CNNClassification 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