Informal-to-formal proving on miniF2F (val)
25.8Proven Theorems RateDeepSeekMath-Base
Evaluation results
| Method | Links | |
|---|---|---|
| DeepSeekMath-BaseSize=7B, Prompting=Few-shot, Prover=Isabelle + Sledgehammer2024.02 | 25.8 | |
| LLEMMA-34bDecoding=greedy, Proof Assistant=Isabelle2023.10 | 21.03 | |
| LlemmaSize=34B, Prompting=Few-shot, Prover=Isabelle + Sledgehammer2024.02 | 21 | |
| LLEMMA-7bDecoding=greedy, Proof Assistant=Isabelle2023.10 | 20.6 | |
| LlemmaSize=7B, Prompting=Few-shot, Prover=Isabelle + Sledgehammer2024.02 | 20.6 | |
| MistralSize=7B, Prompting=Few-shot, Prover=Isabelle + Sledgehammer2024.02 | 18.9 | |
| CodeLlamaSize=34B, Prompting=Few-shot, Prover=Isabelle + Sledgehammer2024.02 | 18.5 | |
| Code Llama 34bDecoding=greedy, Proof Assistant=Isabelle2023.10 | 18.45 | |
| Code Llama 7bDecoding=greedy, Proof Assistant=Isabelle2023.10 | 16.31 | |
| CodeLlamaSize=7B, Prompting=Few-shot, Prover=Isabelle + Sledgehammer2024.02 | 16.3 | |
| SledgehammerDecoding=greedy, Proof Assistant=Isabelle2023.10 | 14.72 |