Formal-to-formal theorem proving on miniF2F (test)
26.5Proven Theorems (%)ReProver (fine-tuned)
Evaluation results
| Method | Links | |
|---|---|---|
| ReProver (fine-tuned)Search=1x64, Proof Assistant=Lean 42023.10 | 26.5 | |
| LLEMMA-7bSearch=1x32, Proof Assistant=Lean 42023.10 | 26.23 | |
| LLEMMA-34bSearch=1x32, Proof Assistant=Lean 42023.10 | 25.82 | |
| COPRA (GPT-4)Search=max 60 samples, Proof Assistant=Lean 42023.10 | 23.36 | |
| Code Llama 34bSearch=1x32, Proof Assistant=Lean 42023.10 | 22.13 | |
| Code Llama 7bSearch=1x32, Proof Assistant=Lean 42023.10 | 20.49 |