Informal description to Lean type retrieval on mathlib (test)
70.18R@1MathLeap-Octen-8B
Evaluation results
| Method | Links | ||||
|---|---|---|---|---|---|
| MathLeap-Octen-8BParameters=8B2026.06 | 70.18 | 88.27 | 91.64 | 78.26 | |
| MathLeap-Qwen-8BParameters=8B2026.06 | 69.34 | 88.35 | 91.72 | 77.77 | |
| F2LLM-v2-14BParameters=14B2026.06 | 67.97 | 90.42 | 93.36 | 77.78 | |
| Octen-Embedding-8BParameters=8B2026.06 | 64.06 | 87.91 | 91.43 | 74.47 | |
| Harrier-OSS-v1-27BParameters=27B2026.06 | 62.26 | 87.9 | 91.67 | 73.37 | |
| Qwen3-Embedding-8BParameters=8B2026.06 | 61.89 | 86.7 | 90.71 | 72.65 | |
| Qwen3-Embedding-4BParameters=4B2026.06 | 57.01 | 84.33 | 89.08 | 68.79 | |
| KaLM-Gemma3-12BParameters=12B2026.06 | 56.32 | 82.25 | 87.49 | 67.54 | |
| Llama-Embed-Nemotron-8BParameters=8B2026.06 | 27.87 | 52.79 | 61.72 | 38.42 |