Theorem Proving on LeanDojo (random)
53.21Pass@1LeanListener
Evaluation results
| Method | Links | |
|---|---|---|
| LeanListenerPolicy Opt. Method=GRPO (#sub-goals), Online=V2025.03 | 53.21 | |
| ReProver*Notes=Newly provided pre-trained model2025.03 | 52.76 | |
| ReProver2025.03 | 51.2 | |
| ReProverretrieval=true2023.06 | 51.2 | |
| LeanListenerPolicy Opt. Method=DPO (binary), Pairing Strategy=zero acc., Online=V2025.03 | 50.9 | |
| LeanListenerPolicy Opt. Method=DPO (binary), Pairing Strategy=hard, Online=V2025.03 | 50.85 | |
| LeanListenerPolicy Opt. Method=DPO (binary), Pairing Strategy=rand., Online=V2025.03 | 50.25 | |
| ReProver (w/o retrieval)2025.03 | 47.6 | |
| ReProverretrieval=false2023.06 | 47.6 | |
| LeanListenerPolicy Opt. Method=DPO (binary), Pairing Strategy=rand., Online=X2025.03 | 35.99 | |
| LeanListenerPolicy Opt. Method=DPO (binary), Pairing Strategy=zero acc., Online=X2025.03 | 33.18 | |
| LeanListenerPolicy Opt. Method=DPO (binary), Pairing Strategy=hard, Online=X2025.03 | 31.27 | |
| GPT-42025.03 | 29 | |
| GPT-4mode=zero-shot, tactic_candidates=35, search=best-first search2023.06 | 29 | |
| tidy2025.03 | 23.8 | |
| tidy2023.06 | 23.8 |