Autoformalization on ConNF
72.32TC@1DRIFT
Evaluation results
| Method | Links | ||||
|---|---|---|---|---|---|
| DRIFTRetrieval Strategy=DRIFT, Model=Claude-Opus-42025.10 | 72.32 | 60.35 | — | — | |
| DRIFTFormalizer=GPT-4.12025.10 | 65.76 | 54.84 | 77 | 62.33 | |
| Oracle*Retrieval Strategy=Oracle*, Model=Claude-Opus-42025.10 | 62.75 | 50.36 | — | — | |
| DRIFTFormalizer=DeepSeek-V3.12025.10 | 60.67 | 46.72 | 71.18 | 54.21 | |
| Oracle*Formalizer=GPT-4.12025.10 | 60.46 | 48.28 | 75.23 | 58.9 | |
| Oracle*Formalizer=DeepSeek-V3.12025.10 | 57.34 | 44.22 | 71.28 | 55.15 | |
| RAutoRetrieval Strategy=RAuto, Model=Claude-Opus-42025.10 | 26.64 | 18.52 | — | — | |
| DPR (RAuto)Formalizer=GPT-4.12025.10 | 24.56 | 15.19 | 31.95 | 20.08 | |
| DPR (RAuto)Formalizer=DeepSeek-V3.12025.10 | 21.96 | 12.9 | 28.2 | 17.07 | |
| Zero-shotFormalizer=Goedel-V2-8B2025.10 | 16.03 | 2.29 | 71.19 | 10.93 | |
| DPR (RAuto)Formalizer=Goedel-V2-8B2025.10 | 15.92 | 3.64 | 64.52 | 16.96 | |
| Zero-shotFormalizer=DeepSeek-V3.12025.10 | 13.42 | 8.12 | 17.59 | 11.03 | |
| Zero-shotRetrieval Strategy=Zero-shot, Model=Claude-Opus-42025.10 | 13.32 | 8.53 | — | — | |
| Oracle*Formalizer=Goedel-V2-8B2025.10 | 9.99 | 4.37 | 48.8 | 23.1 | |
| DRIFTFormalizer=Goedel-V2-8B2025.10 | 9.89 | 4.27 | 40.89 | 19.04 | |
| Zero-shotFormalizer=GPT-4.12025.10 | 7.28 | 4.47 | 11.45 | 6.76 |