| # Evaluación del RAG y del pipeline — RagSolver |
|
|
| Generado por `scripts/eval_report.py`. Metodología: `docs/PLAN_RAG.md` §10-§11; decisiones y correcciones: `docs/DECISIONS.md`. |
|
|
| ## 1. Retriever sobre Mathlib (MathlibQR, LeanSearch v2) |
|
|
| Tabla de muestra: gold de MathlibQR/MPR + premisas de miniF2F + 3000 distractores. Cobertura del gold en la tabla: **793/946 (83.8%)**. Métricas crudas (el recall condicionado a cobertura = crudo ÷ cobertura). |
|
|
| ### 1a. 946 consultas, sin rerank |
|
|
| | Variante | recall@10 | ndcg@10 | mrr | |
| |---|---|---|---| |
| | denso | 0.662 | 0.568 | 0.542 | |
| | bm25 | 0.595 | 0.481 | 0.449 | |
| | hibrido | 0.655 | 0.543 | 0.512 | |
|
|
| ### 1b. Muestra aleatoria de 100 consultas (semilla fija), 4 variantes |
|
|
| | Variante | recall@10 | ndcg@10 | mrr | |
| |---|---|---|---| |
| | denso | 0.760 | 0.631 | 0.591 | |
| | bm25 | 0.560 | 0.437 | 0.403 | |
| | hibrido | 0.660 | 0.533 | 0.501 | |
| | hibrido_rerank | 0.710 | 0.617 | 0.592 | |
| |
| ### 1c. Misma muestra de 100 consultas sobre el **índice completo de Mathlib** (`mathlib_full`, 278 160 declaraciones; DECISIONS #48, #56) |
|
|
| | Variante | recall@10 | ndcg@10 | mrr | |
| |---|---|---|---| |
| | denso | 0.410 | 0.297 | 0.268 | |
| | bm25 | 0.250 | 0.196 | 0.184 | |
| | hibrido | 0.380 | 0.276 | 0.250 | |
| | hibrido_rerank | 0.450 | 0.339 | 0.307 | |
| |
| Los números de la tabla de muestra (1a-1b) están inflados por el tamaño del pool (3 903 candidatos); 1c es la medida realista del retriever en producción. |
| |
| **Índice ANN** (`IVF_SQ`, 256 particiones, nprobes 32, refine ×5; DECISIONS #60): recall@10 respecto de la búsqueda exacta **0.989**, recall@50 0.9769 (200 consultas sintéticas); latencia densa p50 2.713 s → **0.045 s** (p95 2.887 → 0.078 s). |
|
|
| ### 1d. Misma muestra sobre el índice completo **con el índice ANN** (el que usan la demo y los agentes con `RAGSOLVER_MATHLIB_TABLE=mathlib_full`) |
| |
| | Variante | recall@10 | ndcg@10 | mrr | |
| |---|---|---|---| |
| | denso | 0.420 | 0.302 | 0.270 | |
| | bm25 | 0.250 | 0.196 | 0.184 | |
| | hibrido | 0.380 | 0.277 | 0.251 | |
| | hibrido_rerank | 0.450 | 0.339 | 0.307 | |
|
|
| ## 2. Premisas gold de miniF2F (pruebas verificadas de DeepSeek-Prover-V2) |
|
|
| Problemas: 352 (con ≥1 premisa en la tabla: 352); cobertura de premisas en la tabla: 100.0%; rerank: False. |
|
|
| | Consulta | recall@8 | recall@20 | ndcg@10 | mrr | |
| |---|---|---|---|---| |
| | enunciado informal (tabla de muestra) | 0.080 | 0.153 | 0.076 | 0.129 | |
| | enunciado formal (Lean) (tabla de muestra) | 0.118 | 0.180 | 0.106 | 0.176 | |
| | enunciado informal (índice completo) | 0.006 | 0.010 | 0.006 | 0.016 | |
| | enunciado formal (Lean) (índice completo) | 0.009 | 0.018 | 0.007 | 0.015 | |
|
|
| ## 3. Gold informal (30 consultas sobre el PDF de ejemplo) |
|
|
| - Recall@5: **1.000** (Wilson 95 %: [0.886, 1.0]); MRR: 1.000 |
| - Consultas dependientes de figura (n=15): Recall@5 = 1.000; cobertura de entidades en las descripciones de figura = 0.911 |
|
|
| ## 4. Contaminación corpus informal ↔ miniF2F-v2 |
|
|
| - Pares con similitud > 0.9: **0** de 100×488; similitud máxima observada: 0.818 |
| - Top-3 más parecidos (card, problema, sim): [[23, 'imo_1959_p1', 0.8181180953979492], [58, 'induction_divisibility_3div2tooddnp1', 0.8117700815200806], [76, 'algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2', 0.7985193729400635]] |
|
|
| ## 5. Ablaciones end-to-end (`eval-v1`) |
|
|
| | Config | n | pass@1 | IC95 Wilson | llamadas LLM (media) | tokens (media) | wall s (mediana) | precisión uso de lemas | re-recuperación OK | taxonomía de errores | |
| |---|---|---|---|---|---|---|---|---|---| |
| | full | 60 | 0.15 | [0.081, 0.261] | 7.62 | 35190 | 287.3 | 0.002 | 0.0 | {'planning': 49, 'lean_syntax': 6, 'exhausted': 33, 'misformalization': 21, 'missing_lemma': 20, 'unknown': 3, 'abandon': 5, 'llm_output_invalid:generator': 2, 'llm_output_invalid:formalizer': 9, 'llm_output_invalid:planner': 1, 'llm_output_invalid:critic': 1} | |
| | no_rag | 60 | 0.15 | [0.081, 0.261] | 7.83 | 23360 | 152.8 | None | None | {'missing_lemma': 25, 'planning': 41, 'exhausted': 29, 'lean_syntax': 5, 'llm_output_invalid:critic': 4, 'misformalization': 17, 'llm_output_invalid:formalizer': 15, 'unknown': 4, 'abandon': 2, 'llm_output_invalid:generator': 1} | |
| | no_critic | 60 | 0.067 | [0.026, 0.159] | 3.28 | 16433 | 62.4 | 0.001 | None | {'unknown': 44, 'exhausted': 44, 'llm_output_invalid:formalizer': 7, 'llm_output_invalid:generator': 4, 'llm_output_invalid:planner': 1} | |
| | baseline_a | 60 | 0.083 | [0.036, 0.181] | 1.13 | 3012 | 5.2 | None | None | {'unknown': 47, 'llm_output_invalid:baseline_a': 8} | |
| | baseline_b | 60 | 0.0 | [0.0, 0.06] | 1.05 | 2214 | 5.9 | None | None | {'llm_output_invalid:baseline_b': 3} | |
|
|
| ### Resultado por problema (✔ = prueba aceptada por el kernel) |
|
|
| | Problema | full | no_rag | no_critic | baseline_a | baseline_b | |
| |---|---|---|---|---|---| |
| | `mathd_algebra_67` | ✔ | ✔ | – | – | – | |
| | `algebra_sqineq_2unitcircatblt1` | ✔ | ✔ | ✔ | – | – | |
| | `mathd_algebra_28` | ✔ | ✔ | – | ✔ | – | |
| | `mathd_algebra_125` | ✔ | ✔ | – | ✔ | – | |
| | `mathd_algebra_342` | – | – | – | – | – | |
| | `induction_prod1p1onk3le3m1onn` | – | – | – | – | – | |
| | `mathd_algebra_214` | – | – | – | – | – | |
| | `aime_1983_p2` | – | – | – | – | – | |
| | `amc12a_2019_p12` | – | – | – | – | – | |
| | `amc12b_2003_p17` | ✔ | – | – | – | – | |
| | `mathd_algebra_437` | – | – | – | – | – | |
| | `mathd_algebra_77` | – | – | – | – | – | |
| | `amc12b_2003_p6` | – | – | – | – | – | |
| | `amc12b_2020_p13` | – | – | – | – | – | |
| | `imo_1962_p2` | – | – | – | – | – | |
| | `amc12a_2010_p11` | – | – | – | – | – | |
| | `imo_1978_p5` | – | – | – | – | – | |
| | `mathd_numbertheory_728` | ✔ | ✔ | – | ✔ | – | |
| | `mathd_numbertheory_229` | – | ✔ | ✔ | – | – | |
| | `mathd_numbertheory_233` | ✔ | – | – | – | – | |
| | `mathd_numbertheory_403` | – | – | – | – | – | |
| | `mathd_numbertheory_101` | ✔ | ✔ | ✔ | ✔ | – | |
| | `mathd_numbertheory_109` | – | – | – | – | – | |
| | `numbertheory_aneqprodakp4_anmsqrtanp1eq2` | – | – | – | – | – | |
| | `numbertheory_sqmod3in01d` | – | – | – | – | – | |
| | `amc12a_2003_p23` | – | – | – | – | – | |
| | `amc12a_2020_p10` | – | – | – | – | – | |
| | `amc12a_2008_p15` | – | – | – | – | – | |
| | `amc12a_2016_p3` | ✔ | ✔ | – | – | – | |
| | `amc12a_2002_p21` | – | – | – | – | – | |
| | `amc12b_2002_p3` | – | – | – | – | – | |
| | `imo_1977_p5` | – | – | – | – | – | |
| | `mathd_algebra_24` | – | – | – | – | – | |
| | `amc12_2000_p6` | – | – | – | – | – | |
| | `mathd_algebra_170` | – | – | – | – | – | |
| | `mathd_algebra_455` | – | – | – | – | – | |
| | `mathd_algebra_104` | – | ✔ | – | ✔ | – | |
| | `amc12a_2002_p6` | – | – | – | – | – | |
| | `amc12a_2003_p1` | – | – | – | – | – | |
| | `mathd_algebra_209` | – | – | ✔ | – | – | |
| | `imo_1987_p6` | – | – | – | – | – | |
| | `amc12a_2003_p25` | – | – | – | – | – | |
| | `amc12_2001_p5` | – | – | – | – | – | |
| | `amc12a_2020_p9` | – | – | – | – | – | |
| | `imo_1965_p1` | – | – | – | – | – | |
| | `imo_1992_p1` | – | – | – | – | – | |
| | `aime_1990_p2` | – | – | – | – | – | |
| | `numbertheory_notequiv2i2jasqbsqdiv8` | – | – | – | – | – | |
| | `imo_1981_p6` | – | – | – | – | – | |
| | `imo_2006_p3` | – | – | – | – | – | |
| | `imo_1993_p5` | – | – | – | – | – | |
| | `aime_1997_p11` | – | – | – | – | – | |
| | `mathd_numbertheory_155` | – | – | – | – | – | |
| | `mathd_algebra_398` | – | – | – | – | – | |
| | `imo_1974_p3` | – | – | – | – | – | |
| | `imo_1990_p3` | – | – | – | – | – | |
| | `mathd_algebra_185` | – | – | – | – | – | |
| | `imo_1964_p1_1` | – | – | – | – | – | |
| | `mathd_algebra_224` | – | – | – | – | – | |
| | `amc12b_2002_p11` | – | – | – | – | – | |
|
|
| ### Comparación pareada (McNemar exacto, α = 0.05; n pequeño → poca potencia) |
|
|
| | A | B | sólo A | sólo B | p | |
| |---|---|---|---|---| |
| | full | no_rag | 2 | 2 | 1.000 | |
| | full | no_critic | 7 | 2 | 0.180 | |
| | full | baseline_a | 5 | 1 | 0.219 | |
| | no_rag | no_critic | 6 | 1 | 0.125 | |
| | no_rag | baseline_a | 4 | 0 | 0.125 | |
| | no_critic | baseline_a | 3 | 4 | 1.000 | |
| |
| **Falsos positivos evitados** (propuesta §8.3): la línea base B se autoevaluó como correcta en 55/60 problemas; en 50 de ellos la formalización directa (línea base A) **no** pasa el kernel. |
| |
| ### Uso de lemas recuperados (config `full`) |
| |
| | Problema | verificados en la prueba | usados en el boceto | recuperados | |
| |---|---|---|---| |
| | `mathd_algebra_67` | 0 | 0 | 13 | |
| | `algebra_sqineq_2unitcircatblt1` | 1 | 0 | 25 | |
| | `mathd_algebra_28` | 0 | 0 | 24 | |
| | `mathd_algebra_125` | 0 | 0 | 40 | |
| | `mathd_algebra_342` | 0 | 0 | 27 | |
| | `induction_prod1p1onk3le3m1onn` | 0 | 0 | 33 | |
| | `mathd_algebra_214` | 0 | 1 | 41 | |
| | `aime_1983_p2` | 0 | 0 | 39 | |
| | `amc12a_2019_p12` | 0 | 0 | 35 | |
| | `amc12b_2003_p17` | 2 | 0 | 23 | |
| | `mathd_algebra_437` | 0 | 1 | 37 | |
| | `mathd_algebra_77` | 0 | 0 | 49 | |
| | `amc12b_2003_p6` | 0 | 0 | 36 | |
| | `amc12b_2020_p13` | 0 | 0 | 44 | |
| | `imo_1962_p2` | 0 | 0 | 15 | |
| | `amc12a_2010_p11` | 0 | 0 | 34 | |
| | `imo_1978_p5` | 0 | 0 | 30 | |
| | `mathd_numbertheory_728` | 0 | 0 | 30 | |
| | `mathd_numbertheory_229` | 0 | 0 | 22 | |
| | `mathd_numbertheory_233` | 0 | 0 | 38 | |
| | `mathd_numbertheory_403` | 0 | 2 | 29 | |
| | `mathd_numbertheory_101` | 0 | 0 | 19 | |
| | `mathd_numbertheory_109` | 0 | 0 | 28 | |
| | `numbertheory_aneqprodakp4_anmsqrtanp1eq2` | 0 | 0 | 51 | |
| | `numbertheory_sqmod3in01d` | 0 | 0 | 34 | |
| | `amc12a_2003_p23` | 0 | 0 | 27 | |
| | `amc12a_2020_p10` | 0 | 0 | 33 | |
| | `amc12a_2008_p15` | 0 | 0 | 18 | |
| | `amc12a_2016_p3` | 1 | 0 | 23 | |
| | `amc12a_2002_p21` | 0 | 0 | 51 | |
| | `amc12b_2002_p3` | 0 | 4 | 43 | |
| | `imo_1977_p5` | 0 | 0 | 55 | |
| | `mathd_algebra_24` | 0 | 0 | 36 | |
| | `amc12_2000_p6` | 0 | 0 | 50 | |
| | `mathd_algebra_170` | 0 | 0 | 60 | |
| | `mathd_algebra_455` | 0 | 0 | 38 | |
| | `mathd_algebra_104` | 0 | 0 | 53 | |
| | `amc12a_2002_p6` | 0 | 0 | 50 | |
| | `amc12a_2003_p1` | 0 | 0 | 31 | |
| | `imo_1987_p6` | 0 | 0 | 36 | |
| | `amc12a_2003_p25` | 0 | 0 | 31 | |
| | `amc12_2001_p5` | 0 | 0 | 34 | |
| | `amc12a_2020_p9` | 0 | 0 | 25 | |
| | `imo_1965_p1` | 0 | 0 | 35 | |
| | `imo_1992_p1` | 0 | 0 | 29 | |
| | `mathd_algebra_209` | 0 | 0 | 22 | |
| | `numbertheory_notequiv2i2jasqbsqdiv8` | 0 | 0 | 31 | |
| | `imo_1981_p6` | 0 | 0 | 42 | |
| | `imo_2006_p3` | 0 | 0 | 37 | |
| | `aime_1990_p2` | 0 | 0 | 37 | |
| | `imo_1993_p5` | 0 | 0 | 36 | |
| | `aime_1997_p11` | 0 | 0 | 44 | |
| | `mathd_numbertheory_155` | 0 | 0 | 50 | |
| | `mathd_algebra_398` | 0 | 0 | 25 | |
| | `imo_1974_p3` | 0 | 0 | 0 | |
| | `imo_1990_p3` | 0 | 0 | 32 | |
| | `mathd_algebra_185` | 0 | 0 | 49 | |
| | `imo_1964_p1_1` | 0 | 0 | 30 | |
| | `mathd_algebra_224` | 0 | 0 | 34 | |
| | `amc12b_2002_p11` | 0 | 0 | 32 | |
|
|
| Pruebas aceptadas (`full`): |
|
|
| - `mathd_algebra_67`: `rw [h₀, h₁] · norm_num` |
| - `algebra_sqineq_2unitcircatblt1`: `have h1 : 0 ≤ (a - b) ^ 2 := sq_nonneg (a - b) · have h2 : 2 * (a * b) ≤ a ^ 2 + b ^ 2 := by · nlinarith [h1] · ` |
| - `mathd_algebra_28`: `constructor · · rw [hS] · refine ⟨-5/4, ?_⟩ · norm_num · · intro c hc · rw [hS] at hc · rcases hc wi` |
| - `mathd_algebra_125`: `-- SG1: derive 6 * s = 36 · have h₃ : 6 * s = 36 := by · -- rewrite f using h₁ · rw [← h₁] at h₂ · -- simp` |
| - `amc12b_2003_p17`: `have hx_ne : x ≠ 0 := by · intro hx0 · have hx0' : x * y ^ 3 = 0 := by simp [hx0] · have hlog0 : Real.log (x` |
| - `mathd_numbertheory_728`: `norm_num [ZMod.natCast_zmod_val, Int.ModEq]` |
| - `mathd_numbertheory_233`: `norm_num at h₀ ⊢ · exact h₀` |
| - `mathd_numbertheory_101`: `norm_num` |
| - `amc12a_2016_p3`: `norm_num [h₀, Int.floor_eq_iff]` |
|
|
| Modelos LLM usados en la corrida (cadena por cuota diaria): ['deepseek/deepseek-v4-flash-0731']. Re-recuperaciones tras `lema faltante` en `full`: 1 (exitosas: 0). |
|
|
| ### Desglose por estrato (pass@1, n) — `eval_v1.jsonl` |
| |
| **Por partición** |
| |
| | partición | full | no_rag | no_critic | baseline_a | baseline_b | |
| |---|---|---|---|---|---| |
| | dev | 3/24 (0.12) [0.043, 0.31] | 3/24 (0.12) [0.043, 0.31] | 2/24 (0.08) [0.023, 0.258] | 2/24 (0.08) [0.023, 0.258] | 0/24 (0.00) [0.0, 0.138] | |
| | test | 6/36 (0.17) [0.079, 0.319] | 6/36 (0.17) [0.079, 0.319] | 2/36 (0.06) [0.015, 0.181] | 3/36 (0.08) [0.029, 0.218] | 0/36 (0.00) [0.0, 0.096] | |
| |
| **Por área** |
| |
| | área | full | no_rag | no_critic | baseline_a | baseline_b | |
| |---|---|---|---|---|---| |
| | algebra | 5/24 (0.21) [0.092, 0.405] | 4/24 (0.17) [0.067, 0.359] | 2/24 (0.08) [0.023, 0.258] | 2/24 (0.08) [0.023, 0.258] | 0/24 (0.00) [0.0, 0.138] | |
| | combinatorics | 0/12 (0.00) [0.0, 0.243] | 1/12 (0.08) [0.015, 0.354] | 0/12 (0.00) [0.0, 0.243] | 1/12 (0.08) [0.015, 0.354] | 0/12 (0.00) [0.0, 0.243] | |
| | number_theory | 4/24 (0.17) [0.067, 0.359] | 4/24 (0.17) [0.067, 0.359] | 2/24 (0.08) [0.023, 0.258] | 2/24 (0.08) [0.023, 0.258] | 0/24 (0.00) [0.0, 0.138] | |
|
|
| **Por nivel de dificultad** |
|
|
| | nivel de dificultad | full | no_rag | no_critic | baseline_a | baseline_b | |
| |---|---|---|---|---|---| |
| | 1 | 7/27 (0.26) [0.132, 0.447] | 8/27 (0.30) [0.159, 0.485] | 4/27 (0.15) [0.059, 0.325] | 5/27 (0.19) [0.082, 0.367] | 0/27 (0.00) [0.0, 0.125] | |
| | 2 | 2/21 (0.10) [0.027, 0.289] | 1/21 (0.05) [0.008, 0.227] | 0/21 (0.00) [0.0, 0.155] | 0/21 (0.00) [0.0, 0.155] | 0/21 (0.00) [0.0, 0.155] | |
| | 3 | 0/12 (0.00) [0.0, 0.243] | 0/12 (0.00) [0.0, 0.243] | 0/12 (0.00) [0.0, 0.243] | 0/12 (0.00) [0.0, 0.243] | 0/12 (0.00) [0.0, 0.243] | |
|
|
|
|
| ### Lectura (métricas de la propuesta §8.3) |
|
|
| - **Contribución del RAG** = pass@1(full) − pass@1(sin RAG) = 0.15 − 0.15 = **0.0** (pares discordantes (2, 2)); el contexto recuperado multiplica los tokens por 1.5×; precisión de uso de lemas = 0.002. |
| - **Robustez del refinamiento** = pass@1(full) − pass@1(sin Crítico) = **0.083** (pares discordantes (7, 2)); dentro de `full`, pass@1 tras el 1.er intento = 0.117 y final = 0.15: la ganancia atribuible a los reintentos es la diferencia entre ambos; el resto de la brecha con `sin Crítico` (mismo primer intento) es variación entre corridas. |
| - **Eficiencia**: 7.62 llamadas LLM por problema en `full` (tope RNF-3: 20), 1.13 en la línea base A. |
| - **Verificación formal vs. autoevaluación**: la línea base B se declaró correcta en 55/60 problemas; el kernel confirma 11 de esos en alguna configuración verificada. |
|
|
