Autoformalization on miniF2F (test)
96TC@1Oracle*
Evaluation results
| Method | Links | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| Oracle*Formalizer=Goedel-V2-8B2025.10 | 96 | — | — | — | — | — | 28.89 | 100 | 93.33 | |
| RAutoRetrieval Strategy=RAuto, Model=Claude-Opus-42025.10 | 95.98 | — | — | — | — | — | 30.36 | — | — | |
| DPR (RAuto)Formalizer=Goedel-V2-8B2025.10 | 95.55 | — | — | — | — | — | 9.77 | 100 | 26.67 | |
| Zero-shotRetrieval Strategy=Zero-shot, Model=Claude-Opus-42025.10 | 95.09 | — | — | — | — | — | 31.25 | — | — | |
| DRIFTRetrieval Strategy=DRIFT, Model=Claude-Opus-42025.10 | 93.75 | — | — | — | — | — | 32.59 | — | — | |
| Zero-shotFormalizer=Goedel-V2-8B2025.10 | 93.33 | — | — | — | — | — | 22.22 | 100 | 93.33 | |
| DRIFTFormalizer=Goedel-V2-8B2025.10 | 93.33 | — | — | — | — | — | 26.67 | 100 | 93.33 | |
| Oracle*Retrieval Strategy=Oracle*, Model=Claude-Opus-42025.10 | 93.3 | — | — | — | — | — | 35.27 | — | — | |
| Oracle*Formalizer=DeepSeek-V3.12025.10 | 77.68 | — | — | — | — | — | 23.21 | 87.5 | 28.12 | |
| DPR (RAuto)Formalizer=GPT-4.12025.10 | 77.23 | — | — | — | — | — | 24.55 | 92.41 | 32.14 | |
| Zero-shotFormalizer=DeepSeek-V3.12025.10 | 76.34 | — | — | — | — | — | 22.77 | 87.5 | 27.23 | |
| DPR (RAuto)Formalizer=DeepSeek-V3.12025.10 | 75.89 | — | — | — | — | — | 22.77 | 87.95 | 27.68 | |
| Oracle*Formalizer=GPT-4.12025.10 | 75.45 | — | — | — | — | — | 23.66 | 89.29 | 30.36 | |
| DRIFTFormalizer=GPT-4.12025.10 | 74.55 | — | — | — | — | — | 24.55 | 92.41 | 29.02 | |
| DRIFTFormalizer=DeepSeek-V3.12025.10 | 74.11 | — | — | — | — | — | 22.77 | 88.84 | 24.55 | |
| Zero-shotFormalizer=GPT-4.12025.10 | 69.64 | — | — | — | — | — | 23.21 | 84.82 | 28.12 | |
| Monotonic Reference-Free RefinementJudges=GPT-4.1-mini, Time Step (t)=02026.01 | — | 80.33 | 53.59 | 80.19 | 54.92 | 55.69 | — | — | — | |
| Monotonic Reference-Free RefinementJudges=GPT-4.1-mini, Time Step (t)=12026.01 | — | 93.44 | 66.6 | 86.34 | 70.7 | 72.34 | — | — | — | |
| Monotonic Reference-Free RefinementJudges=GPT-4.1-mini, Time Step (t)=22026.01 | — | 93.44 | 71.11 | 88.66 | 74.8 | 75.98 | — | — | — | |
| Monotonic Reference-Free RefinementJudges=GPT-4.1-mini, Time Step (t)=32026.01 | — | 93.44 | 72.34 | 89.48 | 75.82 | 77 | — | — | — | |
| Monotonic Reference-Free RefinementJudges=GPT-4.1-mini, Time Step (t)=42026.01 | — | 93.44 | 73.57 | 89.89 | 76.84 | 77.89 | — | — | — | |
| Monotonic Reference-Free RefinementJudges=GPT-4.1-mini, Time Step (t)=52026.01 | — | 93.44 | 74.08 | 90.16 | 77.05 | 78.22 | — | — | — | |
| Monotonic Reference-Free RefinementJudges=Qwen2.5-Coder-7B, Time Step (t)=02026.01 | — | 80.33 | 29.92 | 47.27 | 16.8 | 27.61 | — | — | — | |
| Monotonic Reference-Free RefinementJudges=Qwen2.5-Coder-7B, Time Step (t)=12026.01 | — | 93.44 | 36.78 | 51.37 | 20.9 | 35.03 | — | — | — | |
| Monotonic Reference-Free RefinementJudges=Qwen2.5-Coder-7B, Time Step (t)=22026.01 | — | 93.44 | 39.04 | 52.73 | 22.75 | 36.85 | — | — | — | |
| Monotonic Reference-Free RefinementJudges=Qwen2.5-Coder-7B, Time Step (t)=32026.01 | — | 93.44 | 39.96 | 53.96 | 23.16 | 37.7 | — | — | — | |
| Monotonic Reference-Free RefinementJudges=Qwen2.5-Coder-7B, Time Step (t)=42026.01 | — | 93.44 | 40.06 | 54.51 | 23.77 | 38.13 | — | — | — | |
| Monotonic Reference-Free RefinementJudges=Qwen2.5-Coder-7B, Time Step (t)=52026.01 | — | 93.44 | 39.86 | 54.64 | 23.98 | 38.17 | — | — | — |