Global premise retrieval on MathlibMPR v2 (test)
36.7Recall@5 (group)LeanSearch v2 (reasoning)
Evaluation results
| Method | Links | ||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| LeanSearch v2 (reasoning)Query mode=informal description + formal statement2026.05 | 36.7 | 46.1 | 50.8 | 56.4 | 57.1 | 27.5 | 30.4 | 34.8 | 43.5 | 43.5 | |
| DIVERQuery mode=informal description + formal statement, Configuration=retriever + GroupRank2026.05 | 29.7 | 38.5 | 46.2 | 52.8 | 55 | 18.8 | 24.6 | 27.5 | 33.3 | 37.7 | |
| DIVERQuery mode=informal description + formal statement, Configuration=full pipeline2026.05 | 27.7 | 38 | 46.6 | 52.8 | 55 | 18.8 | 24.6 | 29 | 33.3 | 37.7 | |
| ReasonIRQuery mode=informal description + formal statement2026.05 | 23.9 | 26.9 | 33.3 | 35.6 | 43.8 | 17.4 | 18.8 | 20.3 | 21.7 | 30.4 | |
| DIVERQuery mode=informal description + formal statement, Configuration=retriever + query expansion2026.05 | 22.2 | 27.6 | 40.8 | 43 | 47.9 | 15.9 | 17.4 | 26.1 | 27.5 | 31.9 | |
| DIVERQuery mode=informal description + formal statement, Configuration=retriever only2026.05 | 21.6 | 24.7 | 40.6 | 45.2 | 48.5 | 15.9 | 15.9 | 26.1 | 31.9 | 33.3 | |
| INF-X-RetrieverQuery mode=informal description + formal statement, Configuration=Base2026.05 | 21.2 | 28.2 | 33.9 | 40 | 42.6 | 15.9 | 18.8 | 21.7 | 24.6 | 24.6 | |
| INF-X-RetrieverQuery mode=informal description + formal statement, Configuration=+ query rewriter2026.05 | 13.2 | 17.4 | 25.2 | 28.4 | 38.3 | 10.1 | 10.1 | 17.4 | 17.4 | 24.6 | |
| LeanStateSearchQuery mode=formal proof state2026.05 | 6.5 | 9.3 | 12.5 | 16 | 20 | 2.9 | 2.9 | 7.2 | 10.1 | 13 | |
| LeanPremiseQuery mode=formal proof state2026.05 | 4.1 | 4.8 | 8 | 9.9 | 11.5 | 1.4 | 1.4 | 4.3 | 4.3 | 5.8 | |
| ReProverQuery mode=formal proof state2026.05 | 3 | 5.5 | 7.6 | 8.8 | 10.3 | 0 | 1.4 | 2.9 | 4.3 | 4.3 |