Formal theorem proving on Lean (test)
73Pass@1α-DPG
Evaluation results
| Method | Links | ||||
|---|---|---|---|---|---|
| α-DPGalpha=0.9992025.12 | 73 | 83.5 | — | — | |
| RLOO2025.12 | 71.8 | 83.5 | — | — | |
| GPG2025.12 | 71.6 | 80 | — | — | |
| GRPO2025.12 | 71.5 | 81 | — | — | |
| ReMax2025.12 | 70.4 | 85 | — | — | |
| GRPO-Rw-Ulkly2025.12 | 67.4 | 86 | — | — | |
| α-DPGalpha=0.92025.12 | 66.2 | 86 | — | — | |
| α-DPGalpha=0.752025.12 | 62.6 | 87 | — | — | |
| α-DPGalpha=0.52025.12 | 61.4 | 88.5 | — | — | |
| GRPOKL constraint=High2025.12 | 59.8 | 86.5 | — | — | |
| α-DPGalpha=0.252025.12 | 59.8 | 87 | — | — | |
| α-DPGalpha=02025.12 | 58.9 | 88 | — | — | |
| GRPO-Pass@k2025.12 | 54.8 | 87 | — | — | |
| Base SFT2025.12 | 54.2 | 86 | — | — |