Informal-to-Formal Proving on miniF2F (test)
24.6AccuracyDeepSeekMath-Base
Evaluation Results
| Method | Links | |
|---|---|---|
| DeepSeekMath-BaseSize=7B, Prompting=Few-shot, Prover=Isabelle + Sledgehammer2024.02 | 24.6 | |
| LlemmaSize=7B, Prompting=Few-shot, Prover=Isabelle + Sledgehammer2024.02 | 22.1 | |
| LlemmaSize=34B, Prompting=Few-shot, Prover=Isabelle + Sledgehammer2024.02 | 21.3 | |
| MistralSize=7B, Prompting=Few-shot, Prover=Isabelle + Sledgehammer2024.02 | 18 | |
| CodeLlamaSize=34B, Prompting=Few-shot, Prover=Isabelle + Sledgehammer2024.02 | 18 | |
| CodeLlamaSize=7B, Prompting=Few-shot, Prover=Isabelle + Sledgehammer2024.02 | 17.6 |