Theorem Proving on LeanDojo (novel premises)
41.11Pass@1LeanListener
Evaluation Results
| Method | Links | |
|---|---|---|
| LeanListenerPolicy Opt. Method=GRPO (#sub-goals), Online=V2025.03 | 41.11 | |
| ReProver*Notes=Newly provided pre-trained model2025.03 | 40.86 | |
| ReProver2025.03 | 26.3 | |
| ReProverretrieval=true2023.06 | 26.3 | |
| ReProver (w/o retrieval)2025.03 | 23.2 | |
| ReProverretrieval=false2023.06 | 23.2 | |
| ReProverretrieval=enabled2023.06 | 19.9 | |
| W/o retrievalretrieval=disabled2023.06 | 16.2 | |
| GPT-42025.03 | 7.4 | |
| GPT-4mode=zero-shot, tactic_candidates=35, search=best-first search2023.06 | 7.4 | |
| tidy2025.03 | 5.3 | |
| tidy2023.06 | 5.3 |