Mathematical Retrieval on mathlib Lean type to Lean signature (test)
65.26R@1MathLeap-Octen-8B
Evaluation Results
| Method | Links | ||||
|---|---|---|---|---|---|
| MathLeap-Octen-8BParameters=8B, Backbone=Octen2026.06 | 65.26 | 84.29 | 88.22 | 73.61 | |
| MathLeap-Qwen-8BParameters=8B, Backbone=Qwen2026.06 | 65.01 | 83.83 | 87.72 | 73.24 | |
| Octen-Embedding-8BParameters=8B2026.06 | 60.4 | 81.99 | 86.6 | 69.81 | |
| Qwen3-Embedding-8BParameters=8B2026.06 | 58 | 80.41 | 85.08 | 67.75 | |
| F2LLM-v2-14BParameters=14B2026.06 | 57.96 | 81.9 | 86.82 | 68.33 | |
| Qwen3-Embedding-4BParameters=4B2026.06 | 51.99 | 77.28 | 83.13 | 62.9 | |
| Harrier-OSS-v1-27BParameters=27B2026.06 | 48.36 | 72.91 | 79.04 | 58.97 | |
| KaLM-Gemma3-12BParameters=12B2026.06 | 45.43 | 68.88 | 75.45 | 55.48 | |
| Llama-Embed-Nemotron-8BParameters=8B2026.06 | 8.81 | 15.9 | 19.02 | 11.84 |