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
Showing 1–10 of 288 papers
All datasetsminiF2F-testminiF2F-validHolStep (Conditional)HOList benchmarkHolStep (Unconditional)Metamath set.mmminiF2F-curriculumCompCertCoqGym
Benchmark Results
| # | 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 |