docs/eval_report_v2.md

Evaluación eval-v2 — sistema por goal (docs/PLAN_MEJORA_RAG.md), reporte parcial

2026-10-15. Estado final:

• Ronda 1 completa. Ronda 2 completa (opción B): full 2/15, no_rag 2/15, baseline_auto 2/15, a US$0.109.
• Ronda 3 detenida a pedido (#111): 11/15 pares de full (2 resueltos), sin no_rag.
• baseline_auto completa en los 60.
• Comparación full contra no_rag en 30 problemas pareados: 8 frente a 9.
• Siguiente paso: el rediseño con demostrador local (docs/PLAN_REDISENO_PROVER.md, eval-v3). El guardia de costo detuvo la cadena tras la ronda 1: la proyección para las rondas 2-4 (US$0.343) superaba el saldo de la key (US$0.289). Falta tu decisión para seguir (sección 6).

Datos:

• data/eval/runs/eval-v2/ (resultados y trazas);
• data/eval/results/eval_v2_round1_check.json (guardia);
• eval_v2_analysis.json y eval_v2_stats.json (cifras de este reporte; se regeneran con data/eval/results/eval_v2_analysis.py).

---

1. Resumen

Configuración	Ronda 1 (15 problemas)	IC95 Wilson	Los 60 problemas
full (sistema nuevo con RAG por goal)	6/15	0.20-0.64	—
no_rag (sistema nuevo sin premisas recuperadas)	7/15	0.25-0.70	—
baseline_auto (sólo tácticas de Lean, 0 LLM)	5/15	0.15-0.58	11/60 (0.11-0.30)
eval-v1 full (sistema viejo)	3/15	0.07-0.45	9/60
eval-v1 no_rag	4/15	0.11-0.52	9/60
eval-v1 línea base A (LLM escribe la prueba)	—	—	5/60

Lo que dicen los datos, de más a menos firme:

1. El cambio de arquitectura es lo que más mueve el resultado. Las tácticas de Lean solas, sin una sola llamada al LLM y a US$0, resuelven 11/60, más que el sistema viejo completo (9/60). En la ronda 1, el sistema nuevo resuelve el doble que el viejo en los mismos problemas: 6-7/15 frente a 3-4/15. Esa comparación no es significativa (McNemar p = 0.375; 4 problemas sólo en v2, 1 sólo en v1) y está confundida por el cambio de proveedor del LLM y de índice.
2. Las premisas recuperadas (el RAG nuevo) no muestran efecto medible. full 6 frente a no_rag 7: un único problema distinto, a favor de no_rag. El kernel usó 1 premisa recuperada en 1 problema de los 6 resueltos. La batería cerró más pasos con premisas (26 frente a 18), pero las premisas no aparecen en los términos de prueba: grind cerró esos pasos con lo que ya sabe.
3. Los agentes aportan poco sobre la automatización en esta ronda. full resuelve 1 problema más que baseline_auto (algebra_sqineq_2unitcircatblt1) y no_rag, 2.
4. El flujo nuevo no es más barato en problemas difíciles. US$0.0036 por par en full y US$0.0032 en no_rag, con 23 600 y 16 700 tokens de entrada: lo mismo que eval-v1. La estimación de US$0.0016 que di antes salía de pares fáciles.

Con 15 problemas pareados ninguna diferencia es significativa. Completar las 4 rondas daría n = 60 para full contra no_rag.

2. Configuración

• Problemas: eval-v1 (60), en 4 rondas intercaladas (eval_v1_round{k}.jsonl = problemas k, k+4, …). Cada ronda tiene 6 de álgebra, 6 de teoría de números y 3 de combinatoria.
• Configuraciones: full, no_rag, baseline_auto (DECISIONS #96). rag_nl quedó aislada a pedido del usuario (#106).
• Modelo: DeepSeek V4 Flash vía OpenRouter, con 4 hilos. El tope de precio se subió a {0.13, 0.30} durante la ronda 1 (8 proveedores, #107), porque con el anterior sólo calificaba DeepInfra, saturado.
• Código: prompt_version: "3"; índice mathlib_full; canal denso apagado; prior de competición de 778 lemas.
• Cambios de infraestructura durante la ronda 1 (no afectan a los resultados):
  • los 429 pasaron a reintentarse hasta 10 veces, porque no se cobran (#104);
  • hubo dos reinicios de la cadena: el cambio de reintentos y la salida de rag_nl;
  • los pares interrumpidos se repitieron completos.

3. Ronda 1 por problema

Problema	Área	Dif.	full	no_rag	baseline_auto	v1 full	v1 no_rag
mathd_algebra_209	álgebra	1	✔	✔	✔	–	–
algebra_sqineq_2unitcircatblt1	álgebra	1	✔	✔	–	✔	✔
mathd_algebra_77	álgebra	1	✔	✔	✔	–	–
amc12b_2020_p13	álgebra	2	–	–	–	–	–
amc12a_2010_p11	álgebra	2	–	–	–	–	–
imo_1965_p1	álgebra	3	–	–	–	–	–
mathd_numbertheory_728	t. números	1	✔	✔	✔	✔	✔
mathd_numbertheory_403	t. números	1	✔	✔	✔	–	–
numbertheory_aneqprodakp4_anmsqrtanp1eq2	t. números	1	–	–	–	–	–
amc12a_2020_p10	t. números	2	–	–	–	–	–
amc12a_2016_p3	t. números	2	–	–	–	✔	✔
imo_1977_p5	t. números	3	–	–	–	–	–
mathd_algebra_170	combinatoria	1	–	–	–	–	–
mathd_algebra_104	combinatoria	1	✔	✔	✔	–	✔
amc12a_2002_p6	combinatoria	2	–	✔	–	–	–

Comparaciones pareadas (McNemar exacto, ronda 1):

A	B	sólo A	sólo B	p
v2 full	v2 no_rag	0	1	1.00
v2 full	baseline_auto	1	0	1.00
v2 full	v1 full	4	1	0.375
v2 no_rag	v1 no_rag	4	1	0.375

En los 60: baseline_auto contra v1 full, 7 sólo auto frente a 5 sólo v1 (p = 0.77); contra la línea base A de v1, 7 frente a 1 (p = 0.07).

4. Qué cerró cada paso y qué usó el kernel

• Pasos cerrados por la batería CLOSE (sin LLM; los cerrados por el bloque del propio modelo no se cuentan aquí):

  Config	grind (con premisas en full)	try?	nlinarith	abiertos tras CLOSE (van a FILL)
  full	23	3	—	113
  no_rag	14	3	1	128

• Premisas recuperadas que usa el término aceptado (Verdict.used_constants, #101): 1 en full, en un problema. El texto de las pruebas nombra 16 por cada grind +lax [...], pero el kernel no las usa. Los 9 pasos de diferencia en la batería se explican porque cada configuración recibe esqueletos distintos (muestras distintas del LLM), no por las premisas.

• Llamadas FILL: 19 en full y 21 en no_rag, en 15 problemas.

• Por qué fallan los problemas difíciles: sobre todo pruebas del modelo que Lean rechaza (unsolved goals, type mismatch) en pasos que ni la batería ni FILL logran cerrar. Ejemplo, amc12a_2002_p6 en full: el modelo usa Set.infinite_univ para {m | 0 < m}, y en FILL escribe un bloque en una sola línea con viñetas · encadenadas por ;. No se encontró ningún error de ensamblado: el archivo final contiene exactamente lo que se verificó paso a paso.

5. Costo

Concepto	US$
Smoke (2 corridas, 8 problemas)	0.0145
Ronda 1 (gasto de la key, incluidos ~US$0.008 de pares interrumpidos por los reinicios)	0.1143
baseline_auto, 60 problemas	0.0000
Saldo de la key	0.2892

Por par: full US$0.0036 (23 600 tokens de entrada / 9 300 de salida); no_rag US$0.0032 (16 700 / 9 800). full lleva un 42 % más de tokens de entrada por las listas de premisas con firma que van a FILL. Ningún par superó el presupuesto de 20 llamadas (máximo 15) y no hubo pares en error.

Proyección para las rondas 2-4: 90 pares pagados × ~US$0.0034 ≈ US$0.31-0.34, frente a US$0.289 de saldo. Por eso el guardia cortó, como estaba previsto.

6. Opciones para seguir (decisión del usuario)

Opción	Qué se obtiene	Costo	Tiempo
A. Subir el límite de la key en OpenRouter (≥ US$0.10 más) y correr las rondas 2-4	full contra no_rag en los 60 problemas: la única medición con potencia mínima para el aporte del RAG	~US$0.33	2-4 h
B. Correr sólo las rondas 2 y 3 con el saldo actual	45 problemas pareados	~US$0.21	1.5-3 h
C. Volver al tope barato (sólo DeepInfra) y correr las rondas 2-4	60 problemas; 17 % más barato por token. La proyección (US$0.28) queda justo en el límite del saldo y puede quedar incompleta	~US$0.28	13-16 h (429)
D. Parar aquí	Ronda 1 + baseline_auto en los 60	0	—

Recomendación: A, y si no es posible, B. Con la ronda 1 sola no se puede afirmar nada del aporte del RAG: se necesitan los pares de las otras rondas.

7. Qué significa para el objetivo del RAG

• El RAG nuevo recupera mucho mejor (recall@16 por goal 0.327 frente a <0.01, Fase 3), pero todavía no convierte eso en problemas resueltos:
  • la automatización (grind) ya conoce los lemas genéricos que trae el prior (sq_nonneg, mul_pos…), así que dárselos no le añade nada;
  • FILL los recibe, pero el término final casi nunca los usa.
• Donde el RAG podría aportar es en lemas específicos (Nat.Prime.eq_one_or_self_of_dvd, Real.log_rpow) que ni la automatización ni el modelo conocen bien. El canal que los buscaba (el índice denso) fue el que no funcionó (recall 0.028).
• Siguiente mejora candidata, a medir antes de gastar: recuperar para los goals que quedan abiertos tras la batería, en lugar de para todos. Con el dato de qué falló (el error de Lean) se buscarían lemas específicos, y se pasarían a FILL con prioridad sobre los genéricos.