Theorem Proving on ProofNet (val)
25.4AccuracyDeepSeek-Prover-V1.5-RL + RMaxTS
Evaluation results
| Method | Links | ||||
|---|---|---|---|---|---|
| DeepSeek-Prover-V1.5-RL + RMaxTSSample budget=4 x 64002024.08 | 25.4 | — | — | — | |
| DeepSeek-Prover-V1.5-SFT + RMaxTSSample budget=4 x 64002024.08 | 23.8 | — | — | — | |
| DeepSeek-Prover-V1.5-SFTSample budget=4 x 64002024.08 | 22.2 | — | — | — | |
| DeepSeek-Prover-V1.5-RLSample budget=4 x 64002024.08 | 21.6 | — | — | — | |
| Hierarchical AttentionK=64, Search Strategy=best-first search2025.04 | 11.86 | 1 | 0.5 | 18.75 | |
| DeepSeek-Prover-V1.5-BaseSample budget=32002024.08 | 10.8 | — | — | — | |
| Hierarchical AttentionK=16, Search Strategy=best-first search2025.04 | 10.73 | — | — | — | |
| Hierarchical AttentionK=32, Search Strategy=best-first search2025.04 | 10.73 | 1 | 0.5 | 12.5 | |
| BaselineK=64, Search Strategy=best-first search2025.04 | 10.17 | 2 | — | — | |
| BaselineK=16, Search Strategy=best-first search2025.04 | 9.04 | — | — | — | |
| BaselineK=32, Search Strategy=best-first search2025.04 | 9.04 | 2 | — | — |