Autoformalization on ProofNet
94.1Compilation Pass Rate@10Kimina-7B
Evaluation Results
| Method | Links | ||
|---|---|---|---|
| Kimina-7BAugmentation=+CRAMF2025.08 | 94.1 | 7.7 | |
| Kimina-7BAugmentation=Base2025.08 | 87.4 | — | |
| Godel-V2-8BAugmentation=+CRAMF2025.08 | 87.4 | 2.1 | |
| Claude 4.1Augmentation=+CRAMF2025.08 | 85.6 | 5.5 | |
| Godel-V2-8BAugmentation=Base2025.08 | 85.6 | — | |
| Claude 4.1Augmentation=Base2025.08 | 81.1 | — | |
| Godel-V2-8BAugmentation=CRAMF2025.08 | 80.2 | 9.9 | |
| Claude 4.1Augmentation=CRAMF2025.08 | 79.7 | 10.4 | |
| Herald-7BAugmentation=+CRAMF2025.08 | 79.4 | 30.4 | |
| Gemini 2.5 FlashAugmentation=+CRAMF2025.08 | 75.1 | 5.9 | |
| Godel-V2-8BAugmentation=Base2025.08 | 73 | — | |
| Claude 4.1Augmentation=Base2025.08 | 72.2 | — | |
| Gemini 2.5 FlashAugmentation=Base2025.08 | 70.9 | — | |
| Kimina-7BAugmentation=CRAMF2025.08 | 69.3 | 6.6 | |
| Kimina-7BAugmentation=Base2025.08 | 65 | — | |
| Gemini 2.5 FlashAugmentation=CRAMF2025.08 | 63.1 | 10.7 | |
| GPT-4oAugmentation=+CRAMF2025.08 | 62.6 | 30.4 | |
| Herald-7BAugmentation=Base2025.08 | 60.9 | — | |
| Gemini 2.5 FlashAugmentation=Base2025.08 | 57 | — | |
| Herald-7BAugmentation=CRAMF2025.08 | 55.1 | 24.1 | |
| Deepseek-V3Augmentation=+CRAMF2025.08 | 53.1 | 33.4 | |
| GPT-4oAugmentation=Base2025.08 | 48 | — | |
| Herald-7BAugmentation=Base2025.08 | 44.4 | — | |
| GPT-4oAugmentation=CRAMF2025.08 | 42.2 | 41.1 | |
| Deepseek-V3Augmentation=Base2025.08 | 39.8 | — | |
| Deepseek-V3Augmentation=CRAMF2025.08 | 37 | 56.8 | |
| GPT-4oAugmentation=Base2025.08 | 29.9 | — | |
| Deepseek-V3Augmentation=Base2025.08 | 23.6 | — |