Theorem Proving on miniF2F Lean (test)
52Pass@64DeepSeekMath-Base
Evaluation results
| Method | Links | ||
|---|---|---|---|
| DeepSeekMath-BaseModel size=7B, Generation times=cumulative2024.05 | 52 | — | |
| DeepSeek-ProverModel size=7B, Generation times=655362024.05 | 50 | — | |
| DeepSeek-ProverModel size=7B, Generation times=81922024.05 | 48.8 | — | |
| DeepSeek-ProverModel size=7B, Generation times=642024.05 | 46.3 | — | |
| DeepSeek-ProverModel size=7B, Generation times=1282024.05 | 46.3 | — | |
| EvaristeOnline training statements=miniF2F-valid, Train time (A100 days)=13602022.05 | 41 | — | |
| Hypertree Proof SearchModel size=600M, Generation times=64 x 50002024.05 | 41 | — | |
| Evariste-7dOnline training statements=miniF2F-curriculum, Train time (A100 days)=16202022.05 | 40.6 | — | |
| Evariste-1dOnline training statements=miniF2F-curriculum, Train time (A100 days)=2302022.05 | 38.9 | — | |
| GPT-fTrain time (A100 days)=20002022.05 | 36.6 | — | |
| Curriculum LearningModel size=837M, Generation times=64 x 8 x 5122024.05 | 36.6 | — | |
| SupervisedTrain time (A100 days)=502022.05 | 35.3 | — | |
| Curriculum LearningModel size=837M, Generation times=8 x 8 x 5122024.05 | 34.5 | — | |
| DeepSeek-ProverModel size=7B, Generation times=1 (greedy)2024.05 | 30 | — | |
| Curriculum LearningModel size=837M, Generation times=1 x 8 x 5122024.05 | 29.6 | — | |
| Proof Artifact Co-TrainingModel size=837M, Generation times=8 x 8 x 5122024.05 | 29.2 | — | |
| DeepSeekMath-BaseModel size=7B, Generation times=1282024.05 | 27.5 | — | |
| COPRA (GPT-4)Generation times=1 x 602024.05 | 26.6 | — | |
| LlemmaModel size=7B, Generation times=1 x 32002024.05 | 26.2 | — | |
| LlemmaModel size=34B, Generation times=1 x 32002024.05 | 25.8 | — | |
| ReProverModel size=229M, Generation times=1 x 37512024.05 | 25 | — | |
| Proof Artifact Co-TrainingModel size=837M, Generation times=1 x 8 x 5122024.05 | 24.6 | — | |
| GPT-4-turbo 0409Generation times=642024.05 | 23 | — | |
| COPRA (GPT-3.5)Generation times=1 x 602024.05 | 9 | — |