docs/eval_report_dev.md

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).

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 (f5-ablations)

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	13	0.692	[0.424, 0.873]	5.69	13740	8.6	0.011	0.0	{'lean_syntax': 8, 'exhausted': 4, 'planning': 1, 'misformalization': 1, 'missing_lemma': 4}
no_rag	13	0.769	[0.497, 0.918]	5.31	4709	5.6	None	None	{'missing_lemma': 4, 'lean_syntax': 8, 'exhausted': 3}
no_critic	13	0.462	[0.232, 0.709]	3.0	7231	6.1	0.004	None	{'unknown': 7, 'exhausted': 7}
baseline_a	13	0.615	[0.355, 0.823]	1.0	410	1.1	None	None	{'unknown': 5}
baseline_b	13	0.0	[0.0, 0.228]	1.0	412	1.5	None	None	{}

Resultado por problema (✔ = prueba aceptada por el kernel)

Problema	full	no_rag	no_critic	baseline_a	baseline_b
triv_add_zero	✔	✔	✔	✔	–
triv_add_comm	✔	✔	–	✔	–
triv_square_expand	✔	✔	✔	✔	–
triv_even_square	✔	✔	✔	✔	–
triv_dvd_trans	✔	✔	✔	✔	–
mathd_numbertheory_127	✔	✔	✔	✔	–
mathd_algebra_160	–	✔	–	–	–
mathd_numbertheory_1124	–	–	–	–	–
induction_1pxpownlt1pnx	–	–	–	–	–
mathd_algebra_440	✔	✔	–	✔	–
mathd_numbertheory_495	–	–	–	–	–
mathd_numbertheory_342	✔	✔	✔	✔	–
mathd_numbertheory_222	✔	✔	–	–	–

Comparación pareada (McNemar exacto, α = 0.05; n pequeño → poca potencia)

A	B	sólo A	sólo B	p
full	no_rag	0	1	1.000
full	no_critic	3	0	0.250
full	baseline_a	1	0	1.000
no_rag	no_critic	4	0	0.125
no_rag	baseline_a	2	0	0.500
no_critic	baseline_a	0	2	0.500

Falsos positivos evitados (propuesta §8.3): la línea base B se autoevaluó como correcta en 13/13 problemas; en 5 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
triv_add_zero	1	1	11
triv_add_comm	2	2	18
triv_square_expand	0	3	19
triv_even_square	0	1	13
triv_dvd_trans	0	2	18
mathd_numbertheory_127	0	0	24
mathd_algebra_160	0	0	28
mathd_numbertheory_1124	0	0	48
induction_1pxpownlt1pnx	0	3	19
mathd_algebra_440	0	0	17
mathd_numbertheory_495	0	1	25
mathd_numbertheory_342	0	0	14
mathd_numbertheory_222	0	0	21

Pruebas aceptadas (full):

• triv_add_zero: exact add_zero n
• triv_add_comm: induction b with · | zero => rw [add_zero, zero_add] · | succ b ih => rw [Nat.add_succ, ih, Nat.succ_add]
• triv_square_expand: ring
• triv_even_square: rcases h with ⟨k, rfl⟩ · use 2 * k ^ 2 · ring
• triv_dvd_trans: exact dvd_trans h1 h2
• mathd_numbertheory_127: decide
• mathd_algebra_440: linarith
• mathd_numbertheory_342: norm_num
• mathd_numbertheory_222: have h2 := Nat.gcd_mul_lcm 120 b · rewrite [h₀, h₁] at h2 · omega

Modelos LLM usados en la corrida (cadena por cuota diaria): ['gemini-3.5-flash', 'gemini-3.5-flash-lite']. Re-recuperaciones tras lema faltante en full: 3 (exitosas: 0).

Desglose por estrato (pass@1, n) — dev_all.jsonl

Por partición

partición	full	no_rag	no_critic	baseline_a	baseline_b
dev	9/13 (0.69) [0.424, 0.873]	10/13 (0.77) [0.497, 0.918]	6/13 (0.46) [0.232, 0.709]	8/13 (0.62) [0.355, 0.823]	0/13 (0.00) [0.0, 0.228]

Por área

área	full	no_rag	no_critic	baseline_a	baseline_b
algebra	4/5 (0.80) [0.376, 0.964]	5/5 (1.00) [0.566, 1.0]	2/5 (0.40) [0.118, 0.769]	4/5 (0.80) [0.376, 0.964]	0/5 (0.00) [0.0, 0.434]
induction	0/1 (0.00) [0.0, 0.793]	0/1 (0.00) [0.0, 0.793]	0/1 (0.00) [0.0, 0.793]	0/1 (0.00) [0.0, 0.793]	0/1 (0.00) [0.0, 0.793]
number_theory	5/7 (0.71) [0.359, 0.918]	5/7 (0.71) [0.359, 0.918]	4/7 (0.57) [0.25, 0.842]	4/7 (0.57) [0.25, 0.842]	0/7 (0.00) [0.0, 0.354]

Por nivel de dificultad

nivel de dificultad	full	no_rag	no_critic	baseline_a	baseline_b
1	5/5 (1.00) [0.566, 1.0]	5/5 (1.00) [0.566, 1.0]	4/5 (0.80) [0.376, 0.964]	5/5 (1.00) [0.566, 1.0]	0/5 (0.00) [0.0, 0.434]
2	4/8 (0.50) [0.215, 0.785]	5/8 (0.62) [0.306, 0.863]	2/8 (0.25) [0.071, 0.591]	3/8 (0.38) [0.137, 0.694]	0/8 (0.00) [0.0, 0.324]

Lectura (métricas de la propuesta §8.3)

• Contribución del RAG = pass@1(full) − pass@1(sin RAG) = 0.692 − 0.769 = -0.077 (pares discordantes (0, 1)); el contexto recuperado multiplica los tokens por 2.9×; precisión de uso de lemas = 0.011.
• Robustez del refinamiento = pass@1(full) − pass@1(sin Crítico) = 0.23 (pares discordantes (3, 0)); dentro de full, pass@1 tras el 1.er intento = None y final = 0.692: 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: 5.69 llamadas LLM por problema en full (tope RNF-3: 20), 1.0 en la línea base A.
• Verificación formal vs. autoevaluación: la línea base B se declaró correcta en 13/13 problemas; el kernel confirma 10 de esos en alguna configuración verificada.