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 Added Most Hyped Most Active Needs Verification Most Verified

Showing 251–288 of 288 papers

Title	Date	Tasks	Status	Hype
Artificial Neural Networks that Learn to Satisfy Logic Constraints	Dec 8, 2017	Automated Theorem Proving	—Unverified	0
Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving	Dec 4, 2017	Automated Theorem Proving	—Unverified	0
Interactive, Intelligent Tutoring for Auxiliary Constructions in Geometry Proofs	Nov 20, 2017	Automated Theorem Proving	—Unverified	0
Premise Selection for Theorem Proving by Deep Graph Embedding	Sep 28, 2017	Automated Theorem ProvingGeneral Classification	CodeCode Available	0
Evaluating an Automata Approach to Query Containment	Sep 1, 2017	Automated Theorem ProvingText Generation	—Unverified	0
LangPro: Natural Language Theorem Prover	Aug 30, 2017	Automated Theorem ProvingNatural Language Inference	CodeCode Available	1
Robust Computer Algebra, Theorem Proving, and Oracle AI	Aug 8, 2017	Automated Theorem ProvingQuestion Answering	—Unverified	0
Count-Invariance Including Exponentials	Jul 1, 2017	Automated Theorem Proving	—Unverified	0
COVER: Covering the Semantically Tractable Questions	Apr 1, 2017	Automated Theorem ProvingSemantic Parsing	—Unverified	0
On-demand Injection of Lexical Knowledge for Recognising Textual Entailment	Apr 1, 2017	Automated Theorem ProvingInformation Retrieval	CodeCode Available	0
HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving	Mar 1, 2017	Automated Theorem ProvingBIG-bench Machine Learning	CodeCode Available	0
Theorem Proving Based on Semantics of DNA Strand Graph	Feb 15, 2017	Automated Theorem Proving	—Unverified	0
jsCoq: Towards Hybrid Theorem Proving Interfaces	Jan 25, 2017	Automated Theorem Proving	—Unverified	0
Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving	Nov 29, 2016	Automated Theorem ProvingSemantic Parsing	—Unverified	0
Blocking and Other Enhancements for Bottom-Up Model Generation Methods	Nov 28, 2016	Automated Theorem ProvingBlocking	—Unverified	0
BliStrTune: Hierarchical Invention of Theorem Proving Strategies	Nov 26, 2016	Automated Theorem Proving	—Unverified	0
Monte Carlo Tableau Proof Search	Nov 18, 2016	Automated Theorem Proving	—Unverified	0
DeepAlgebra - an outline of a program	Oct 4, 2016	Automated Theorem Proving	—Unverified	0
Social Network Processes in the Isabelle and Coq Theorem Proving Communities	Sep 22, 2016	Automated Theorem Proving	—Unverified	0
Verifier Theory and Unverifiability	Sep 1, 2016	Automated Theorem ProvingGeneral Classification	—Unverified	0
Holophrasm: a neural Automated Theorem Prover for higher-order logic	Aug 8, 2016	Automated Theorem Proving	CodeCode Available	0
Natural Solution to FraCaS Entailment Problems	Aug 1, 2016	Automated Theorem ProvingNatural Language Inference	—Unverified	0
DeepMath - Deep Sequence Models for Premise Selection	Jun 14, 2016	Automated Theorem Proving	CodeCode Available	0
Extracting Higher-Order Goals from the Mizar Mathematical Library	May 23, 2016	ArticlesAutomated Theorem Proving	—Unverified	0
GeoGebra Tools with Proof Capabilities	Mar 3, 2016	Automated Theorem ProvingBenchmarking	—Unverified	0
Analysis of Algorithms and Partial Algorithms	Jan 13, 2016	Automated Theorem Proving	—Unverified	0
Solving Geometry Problems: Combining Text and Diagram Interpretation	Sep 1, 2015	Automated Theorem ProvingMathematical Question Answering	CodeCode Available	0
Rare Speed-up in Automatic Theorem Proving Reveals Tradeoff Between Computational Time and Information Value	Jun 14, 2015	Automated Theorem Proving	—Unverified	0
Towards Formal Fault Tree Analysis using Theorem Proving	May 8, 2015	Automated Theorem Proving	—Unverified	0
GraATP: A Graph Theoretic Approach for Automated Theorem Proving in Plane Geometry	Dec 18, 2014	Automated Theorem Proving	—Unverified	0
Performance Guarantees for Schatten-p Quasi-Norm Minimization in Recovery of Low-Rank Matrices	Jul 14, 2014	Automated Theorem Proving	—Unverified	0
Learning-assisted Theorem Proving with Millions of Lemmas	Feb 11, 2014	Automated Theorem Proving	—Unverified	0
Machine Learner for Automated Reasoning 0.4 and 0.5	Feb 11, 2014	Automated Theorem Proving	—Unverified	0
A state vector algebra for algorithmic implementation of second-order logic	Dec 9, 2013	Automated Theorem Proving	—Unverified	0
HOL(y)Hammer: Online ATP Service for HOL Light	Sep 19, 2013	Automated Theorem ProvingCPU	CodeCode Available	0
READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking	Jul 8, 2013	Automated Theorem Proving	—Unverified	0
Modeling in OWL 2 without Restrictions	Dec 12, 2012	Automated Theorem Proving	—Unverified	0
Lectures on Jacques Herbrand as a Logician	Feb 26, 2009	Automated Theorem ProvingFormal Logic	CodeCode Available	0

Show:10 25 50

← PrevPage 6 of 6Next →

All datasets miniF2F-test miniF2F-valid HolStep (Conditional)HOList benchmark HolStep (Unconditional)Metamath set.mm miniF2F-curriculum CompCert CoqGym

Benchmark Results

#	Model	Metric	Claimed	Verified	Status
1	Kimina-Prover-Preview	cumulative	80.74	—	Unverified
2	ProofAug	cumulative	66	—	Unverified
3	DeepSeek-Prover-V1.5	cumulative	63.5	—	Unverified
4	Subgoal-XL	cumulative	56.1	—	Unverified
5	DeepSeek-Prover	cumulative	52	—	Unverified
6	Lyra + GPT-4	cumulative	47.1	—	Unverified
7	LEGO-Prover ChatGPT	cumulative	47.1	—	Unverified
8	Decomposing the Enigma	cumulative	45.5	—	Unverified
9	Evariste	cumulative	41	—	Unverified
10	Evariste-7d	cumulative	40.6	—	Unverified

#	Model	Metric	Claimed	Verified	Status
1	Evariste	Pass@64	58.6	—	Unverified
2	LEGO-Prover ChatGPT	Pass@100	57	—	Unverified
3	Lyra + GPT-4	Pass@100	52	—	Unverified
4	Evariste-7d	Pass@64	47.5	—	Unverified
5	GPT-f	Pass@64	47.3	—	Unverified
6	Evariste-1d	Pass@64	46.7	—	Unverified
7	DSP (62B Minerva informal)	Pass@100	43.9	—	Unverified
8	Lean GPT-f	Pass@8	29.3	—	Unverified
9	Lean tidy	Pass@1	16.8	—	Unverified
10	Metamath GPT-f	Pass@8	2	—	Unverified

#	Model	Metric	Claimed	Verified	Status
1	MPNN-DagLSTM	Classification Accuracy	0.92	—	Unverified
2	FormulaNet	Classification Accuracy	0.9	—	Unverified
3	FormulaNet-basic	Classification Accuracy	0.89	—	Unverified
4	Siamese 1D CNN-LSTM	Classification Accuracy	0.83	—	Unverified
5	Siamese 1D CNN	Classification Accuracy	0.82	—	Unverified

#	Model	Metric	Claimed	Verified	Status
1	4-hop GNN, sub-expression sharing	Percentage correct	49.95	—	Unverified
2	Tactic Dependent Loop	Percentage correct	38.88	—	Unverified
3	BoW2 (extra -ves)	Percentage correct	36.55	—	Unverified
4	Deeper Wider WaveNet	Percentage correct	32.65	—	Unverified

#	Model	Metric	Claimed	Verified	Status
1	FormulaNet	Classification Accuracy	0.9	—	Unverified
2	FormulaNet-basic	Classification Accuracy	0.89	—	Unverified
3	1D CNN-LSTM	Classification Accuracy	0.83	—	Unverified
4	1D CNN	Classification Accuracy	0.83	—	Unverified

#	Model	Metric	Claimed	Verified	Status
1	Evariste	Pass@32	72.4	—	Unverified
2	GPT-f	Percentage correct	56.2	—	Unverified
3	MetaGen-IL + Holophrasm	Percentage correct	22.1	—	Unverified
4	Holophrasm	Percentage correct	14.3	—	Unverified

#	Model	Metric	Claimed	Verified	Status
1	Evariste-7d	Pass@64	42.5	—	Unverified
2	Evariste-1d	Pass@64	33.6	—	Unverified
3	Evariste	Pass@64	32.1	—	Unverified
4	GPT-f	Pass@64	30.6	—	Unverified

#	Model	Metric	Claimed	Verified	Status
1	Proverbot9001	Percentage correct	19.36	—	Unverified
2	CoqGym/ASTactic	Percentage correct	4.99	—	Unverified

#	Model	Metric	Claimed	Verified	Status
1	ASTactic	Percentage correct	12.2	—	Unverified