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

Title	Date	Tasks	Status	Hype
Logical Neural Networks	Jun 23, 2020	Automated Theorem ProvingLogical Reasoning	CodeCode Available	1
Learning to Prove from Synthetic Theorems	Jun 19, 2020	Automated Theorem Proving	—Unverified	0
Towards United Reasoning for Automatic Induction in Isabelle/HOL	May 25, 2020	Automated Theorem Proving	—Unverified	0
Logical Inferences with Comparatives and Generalized Quantifiers	May 16, 2020	Automated Theorem ProvingNatural Language Inference	CodeCode Available	1
Towards Concise, Machine-discovered Proofs of Gödel's Two Incompleteness Theorems	May 6, 2020	Automated Theorem ProvingVocal Bursts Valence Prediction	—Unverified	0
Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)	Apr 21, 2020	Automated Theorem ProvingBIG-bench Machine Learning	—Unverified	0
Prolog Technology Reinforcement Learning Prover	Apr 15, 2020	Automated Theorem Provingreinforcement-learning	CodeCode Available	1
Towards a Geometry Automated Provers Competition	Feb 28, 2020	Automated Theorem ProvingCPU	—Unverified	0
Proceedings 8th International Workshop on Theorem Proving Components for Educational Software	Feb 27, 2020	Automated Theorem Proving	—Unverified	0
Learning to Prove Theorems by Learning to Generate Theorems	Feb 17, 2020	Automated Theorem Proving	CodeCode Available	1
OxKBC: Outcome Explanation for Factorization Based Knowledge Base Completion	Feb 14, 2020	Automated Theorem ProvingKnowledge Base Completion	CodeCode Available	0
An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic	Feb 2, 2020	Automated Theorem Proving	—Unverified	0
On Quantified Modal Theorem Proving for Modeling Ethics	Dec 30, 2019	Automated Theorem ProvingEthics	—Unverified	0
Property Invariant Embedding for Automated Reasoning	Nov 27, 2019	Automated Theorem ProvingGraph Neural Network	—Unverified	0
Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling	Nov 15, 2019	Automated Theorem ProvingDeep Learning	CodeCode Available	0
Aplib: Tactical Programming of Intelligent Agents	Nov 12, 2019	Automated Theorem Proving	CodeCode Available	0
A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving	Nov 5, 2019	Automated Theorem ProvingDeep Reinforcement Learning	CodeCode Available	1
G2SAT: Learning to Generate SAT Formulas	Oct 29, 2019	Automated Theorem Proving	CodeCode Available	0
Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic	Oct 25, 2019	Automated Theorem ProvingBIG-bench Machine Learning	CodeCode Available	0
CSPLib: Twenty Years On	Sep 30, 2019	Automated Theorem ProvingBIG-bench Machine Learning	—Unverified	0
Proceedings 35th International Conference on Logic Programming (Technical Communications)	Sep 17, 2019	Automated Theorem ProvingData Integration	—Unverified	0
Designing Game of Theorems	Jun 20, 2019	Automated Theorem ProvingGame of Go	—Unverified	0
Neural Theorem Provers Do Not Learn Rules Without Exploration	Jun 17, 2019	Automated Theorem ProvingDiagnostic	CodeCode Available	0
Multimodal Logical Inference System for Visual-Textual Entailment	Jun 10, 2019	Automated Theorem ProvingNatural Language Inference	—Unverified	0
Towards Finding Longer Proofs	May 30, 2019	Automated Theorem Provingreinforcement-learning	CodeCode Available	0
NIL: Learning Nonlinear Interpolants	May 28, 2019	Automated Theorem Proving	—Unverified	0
Learning to Reason in Large Theories without Imitation	May 25, 2019	Automated Theorem ProvingDeep Reinforcement Learning	—Unverified	0
Graph Representations for Higher-Order Logic and Theorem Proving	May 24, 2019	Automated Theorem Proving	—Unverified	0
Learning to Prove Theorems via Interacting with Proof Assistants	May 21, 2019	Automated Theorem ProvingMathematical Proofs	CodeCode Available	0
Guiding Inferences in Connection Tableau by Recurrent Neural Networks	May 20, 2019	Automated Theorem ProvingMachine Translation	CodeCode Available	0
Scalable Neural Theorem Proving on Knowledge Bases and Natural Language	May 1, 2019	Automated Theorem ProvingLink Prediction	—Unverified	0
Towards Evolutionary Theorem Proving for Isabelle/HOL	Apr 17, 2019	Automated Theorem Proving	—Unverified	0
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving	Apr 5, 2019	Automated Theorem ProvingBIG-bench Machine Learning	CodeCode Available	0
Hammering Mizar by Learning Clause Guidance	Apr 2, 2019	Automated Theorem Proving	—Unverified	0
Proceedings 7th International Workshop on Theorem proving components for Educational software	Mar 29, 2019	Automated Theorem Proving	—Unverified	0
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E	Mar 7, 2019	Automated Theorem Proving	—Unverified	0
Review on DNA Strand Algebra and its Application	Mar 4, 2019	Automated Theorem Proving	—Unverified	0
Towards Machine Learning Induction	Dec 4, 2018	Automated Theorem ProvingBIG-bench Machine Learning	—Unverified	0
Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning	Nov 2, 2018	Automated Theorem ProvingData Augmentation	—Unverified	0
Learning to Reason	Oct 12, 2018	Automated Theorem ProvingQ-Learning	—Unverified	0
Logical Rule Induction and Theory Learning Using Neural Theorem Proving	Sep 6, 2018	Automated Theorem Proving	—Unverified	0
Towards Neural Theorem Proving at Scale	Jul 21, 2018	Automated Theorem ProvingRepresentation Learning	—Unverified	0
ML + FV = ? A Survey on the Application of Machine Learning to Formal Verification	Jun 10, 2018	Automated Theorem ProvingBIG-bench Machine Learning	—Unverified	0
GamePad: A Learning Environment for Theorem Proving	Jun 2, 2018	Automated Theorem ProvingPosition	CodeCode Available	0
Automated proof synthesis for propositional logic with deep neural networks	May 30, 2018	Automated Theorem Proving	CodeCode Available	0
Reinforcement Learning of Theorem Proving	May 19, 2018	Automated Theorem Provingreinforcement-learning	—Unverified	0
Cross-checking WordNet and SUMO Using Meronymy	May 1, 2018	Automated Theorem Proving	—Unverified	0
Consistent CCG Parsing over Multiple Sentences for Improved Logical Reasoning	Apr 19, 2018	Automated Theorem ProvingFormal Logic	—Unverified	0
Improving QED-Tutrix by Automating the Generation of Proofs	Mar 5, 2018	Automated Theorem Proving	—Unverified	0
Proceedings 6th International Workshop on Theorem proving components for Educational software	Mar 2, 2018	Automated Theorem Proving	—Unverified	0

Show:10 25 50

← PrevPage 5 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