docs/DECISIONS.md

Registro de decisiones — RagSolver / módulo RAG

Formato: fecha, decisión, alternativa descartada, motivo, evidencia. Ver docs/PLAN_RAG.md §0.

2026-09-18 — Decisiones de arquitectura (§4, §9 del plan)

#	Decisión	Alternativa descartada	Motivo	Evidencia
1	Base vectorial: LanceDB embebida	FAISS, Chroma, Qdrant	FAISS no tiene metadatos/BM25/filtros nativos; habría que reimplementar una base de datos alrededor. Qdrant exige servidor/Docker.	docs/PLAN_RAG.md §9.2
2	Corpus formal: reusar el JSONL informalizado de LeanSearch v2 (FrenzyMath/lsv2-mathlib-v4.28.0-rc1-jsonl, Apache 2.0)	Generar informalización propia con LLM sobre las 310k declaraciones	Ahorra ~310k llamadas LLM; misma receta que el SOTA publicado (nDCG@10=0.62)	arXiv:2605.13137
3	Mathlib pinneado a v4.28.0-rc1 en índice y verificador	Última tag de Mathlib al momento de instalar	Debe coincidir exactamente con la tag del corpus de LeanSearch v2 (decisión #2), si no los decl_name recuperados pueden no existir en la versión que verifica el kernel	configs/versions.yaml; tag verificada contra la API de GitHub (api.github.com/repos/leanprover-community/mathlib4/git/refs/tags/v4.28.0-rc1, commit 5352afc...)
4	OCR de PDFs: MinerU, backend VLM, siempre desde imagen de página (nunca la capa de texto del PDF)	Confiar en la capa de texto del PDF	La capa de texto de problemas resueltos olimpiadas.pdf corrompe fórmulas (2^2001 → 22001, sumatorias desordenadas); confirmado con PyMuPDF sobre el PDF real	docs/PLAN_RAG.md §3
5	Embeddings/reranker: Qwen3-Embedding-0.6B / Qwen3-Reranker-0.6B, sin fine-tuning	Fine-tuning propio; modelos de mayor tamaño por defecto	Sin fine-tuning ya alcanza SOTA en LeanSearch v2; el alcance de la propuesta excluye entrenar modelos desde cero (§5.3 de la propuesta)	docs/PLAN_RAG.md §4
6	Conjunto de evaluación formal: miniF2F-v2	miniF2F original	El original tiene discrepancias formal/informal en >50% de problemas (paper de revisión); v2 trae pruebas verificadas → premisas gold gratis	arXiv:2511.03108, roozbeh-yz/miniF2F_v2
7	Retriever con 0 llamadas LLM en tiempo de ejecución	Recuperación asistida por LLM (p. ej. reformulación de consultas)	RNF-3 limita a ≤20 llamadas LLM/problema; el enriquecimiento con LLM ocurre sólo offline en la ingesta	docs/PLAN_RAG.md §6.3

2026-09-18 — GPU AMD (ROCm), tarjeta del equipo

#	Decisión	Alternativa descartada	Motivo	Evidencia
8	Asumir gfx1201 (RX 9070 XT) CORREGIDO 2026-09-19: la tarjeta real es una AMD Radeon RX 9060 XT (confirmado vía Get-CimInstance Win32_VideoController desde PowerShell — este sandbox comparte máquina con la GPU real del usuario). La 9060 XT es gfx1200 (RDNA4), no gfx1201 — es un chip distinto (más chico) al que se había asumido	gfx1201/RX 9070 XT (dato inventado por falta de info)	El nombre comercial exacto ahora es verificable; gfx1200 y gfx1201 son variantes RDNA4 distintas, no intercambiables para efectos de soporte de ROCm/MinerU	PowerShell Win32_VideoController en esta sesión: Name: AMD Radeon RX 9060 XT
9	Instalar PyTorch ROCm ≥ 7.2 (misma rama que para gfx1201) contra gfx1200, a confirmar con rocminfo una vez instalado	Workaround HSA_OVERRIDE_GFX_VERSION	ROCm 7.2+ también lista gfx1200 (RX 9060 XT) como soportado oficialmente; aún no se instaló en este sandbox (torch actual es build CUDA, no ROCm; no hay rocminfo/rocm-smi en el sistema)	torch.__version__ = 2.14.0+cu130, torch.cuda.is_available()=False en esta sesión; sin rocminfo/dpkg -l rocm*
10	MinerU sobre esta GPU: verificar en Fase 0 (tarea 7) antes de construir la Fase 2, no asumir que funciona	Instalar y descubrir en medio de la ingesta	MinerU sólo soporta oficialmente NVIDIA/Apple; sin evidencia pública conocida de MinerU corriendo sobre gfx1200 (ni sobre gfx1201)	issue opendatalab/MinerU#5288; docs/PLAN_RAG.md §9.4
11	Smoke test tarea 7, paso (a) — CONCLUIDO: ROCm en WSL2 no es viable hoy para esta tarjeta. rocminfo falla con HSA_STATUS_ERROR_OUT_OF_RESOURCES de forma persistente (sobrevive a wsl --shutdown + reinicio completo). Se decide no perseguir GPU local para esta fase; usar CPU (ya en uso) + proveedor LLM/VLM por API para todo lo que necesite visión/enriquecimiento	Instalar librocdxg y seguir iterando drivers/versiones de ROCm	Es un bug conocido y sin resolver de AMD específico de esta tarjeta, no un error de configuración nuestro: ROCm/ROCm#6323 reporta el mismo error exacto (HSA_STATUS_ERROR_OUT_OF_RESOURCES) en la misma GPU (RX 9060 XT / gfx1200) bajo WSL2, probando apt, amdgpu-install --usecase=wsl,rocm y el paquete manual hsa-runtime-rocr4wsl-amdgpu, con múltiples versiones de driver (Adrenalin 26.2.2/26.5.2) y de ROCm (7.1.0/7.2.1) — cerrado por AMD como "not planned", sin fix. Además, probamos HSA_ENABLE_DXG_DETECTION=1 (mencionado en ROCm/librocdxg#22 como forma de sortear este error): falla porque falta el paquete librocdxg (no viene con rocminfo de apt); y aunque se instalara, ese mismo issue reporta que en esta tarjeta específica la detección de VRAM (GetSegmentId) queda rota downstream incluso cuando rocminfo sí ve la GPU — es decir, hay un segundo bug esperando. No es cuestión de reintentar con más paciencia: son bugs abiertos de AMD sobre gfx1200 en WSL2. Re-evaluar cuando AMD publique un fix (o correr Lean/embeddings/MinerU en Linux nativo o Windows nativo con ROCm/DirectML fuera de WSL, si se vuelve prioritario)	dmesg: dxgk: dxgkio_query_adapter_info: Ioctl failed: -22; rocminfo: HSA_STATUS_ERROR_OUT_OF_RESOURCES (antes y después de wsl --shutdown); GitHub ROCm/ROCm#6323 (mismo hardware, mismo error, cerrado "not planned"); GitHub ROCm/librocdxg#22 (VRAM detection rota en RX 9060 XT incluso pasando el primer error)
12	Segundo intento (a pedido del usuario) — instalado rocdxg-roct v1.2.2 (release más nueva de ROCm/librocdxg, Aug 2026, lista explícitamente RX 9060/9060 XT como soportada) vía el .deb oficial, más reciente que la v1.1.1 usada en los issues reportados. Mismo resultado: falla igual. Se confirma que no es un problema de versión de paquete	Seguir probando versiones/combinaciones	Con HSA_ENABLE_DXG_DETECTION=1, rocminfo ahora imprime Load librocdxg.so successully! Load all DTIF APIs OK! (antes ni cargaba la librería) pero igual termina en el mismo HSA_STATUS_ERROR_OUT_OF_RESOURCES — la falla está en la respuesta del servicio de paravirtualización de GPU de Windows al host, no en el lado Linux. Dato que refuerza la correlación con ROCm/ROCm#6323: ese reporte también era una combinación iGPU+dGPU (Ryzen 5600G con Radeon integrada + RX 9060 XT discreta), igual que esta máquina (AMD Radeon(TM) Graphics integrada + RX 9060 XT discreta vistas ambas en Win32_VideoController) — patrón consistente de que el bug afecta específicamente a sistemas con dos adaptadores AMD bajo WSL2. Se cierra la investigación de GPU local para esta fase; se sigue en CPU + proveedor LLM/VLM por API	dpkg -i rocdxg-roct_1.2.2_amd64.deb exitoso; rocminfo con HSA_ENABLE_DXG_DETECTION=1: carga la librería pero mismo HSA_STATUS_ERROR_OUT_OF_RESOURCES

2026-09-18 — Ejecución (esta sesión)

#	Decisión	Alternativa descartada	Motivo	Evidencia
E1	Python del proyecto: 3.12 vía uv python install 3.12 en vez del python3 del sistema (3.14.4)	Usar Python 3.14 del sistema	3.14 es demasiado nuevo (semanas de salida); riesgo real de que torch/lancedb/mineru no tengan wheels aún. El plan ya fijaba 3.11–3.12 (docs/PLAN_RAG.md §9.1)	uv python list mostró sólo "download available" para 3.10–3.13 y binario de sistema en 3.14
E2	Ejecutar la Fase 0 y arrancar la Fase 1 en este sandbox (CPU, sin GPU AMD visible: rocminfo/lspci no la detectan aquí)	Esperar a tener la GPU real conectada	El sandbox tiene red y CPU/disco suficientes para scaffolding, esquemas, tests, descarga del corpus e indexado de una muestra acotada; el embebido completo de 310k declaraciones y el smoke test de ROCm quedan pendientes de correr en la máquina real del usuario (ver estado en el reporte de la sesión)	recon del entorno al inicio de esta tarea
E3	elan default leanprover/lean4:v4.28.0-rc1 (toolchain por defecto de elan, no sólo el lean-toolchain del proyecto)	Dejar --default-toolchain none	lean-interact (usado por el Verificador en Fase 4) invoca lake fuera del cwd del proyecto para chequear la versión; sin default falla con "no default toolchain configured"	prueba directa en esta sesión

Fase 1 — resultados reales de evaluate.py (2026-09-19)

Corrida sobre la muestra acotada (13 736 filas: 116 gold de QR/MPR + 3000 distractores, ver entrada anterior) contra las 946 consultas de MathlibQR. Números crudos en data/eval/results/fase1_mathlibqr_sample13736.json.

Variante	Recall@10 (crudo)	nDCG@10	MRR
Denso	0.241	0.168	0.150
BM25	0.222	0.144	0.124
Híbrido (RRF)	0.282	0.227	0.211
Híbrido + rerank	0.280	0.214	0.193

Cobertura: sólo 282/946 consultas (29.8%) tienen su declaración gold presente en esta tabla de 13 736 filas (la muestra no incluye el corpus completo de 278 560). El criterio de aceptación del plan ("Recall@10 ≥ 0.55") no aplica directamente a un recall crudo acotado por esa cobertura — el número justo es el recall condicionado a cobertura (crudo ÷ 0.298): Denso 0.809, BM25 0.745, Híbrido 0.947, Híbrido+rerank 0.940. Es decir: cuando la declaración correcta SÍ está en el índice, el sistema la encuentra en el top-10 el 94.7% de las veces con fusión híbrida — muy por encima del umbral del 55%.

Hallazgo no esperado, reportado tal cual: el rerank (Qwen3-Reranker-0.6B) empeoró levemente las 3 métricas frente a híbrido sin rerank, en vez de mejorarlas. No se investigó a fondo la causa (candidatos posibles: ventana de candidatos ya buena a esta escala reducida de 13 736 filas con pocos distractores "difíciles"; posible desajuste de plantilla de instrucción del cross-encoder vía el wrapper genérico de sentence-transformers; ruido estadístico con sólo 282 consultas con señal positiva). No se cambia la decisión de usar rerank en el diseño porque: (a) la literatura de referencia (LeanSearch v2, Anthropic) consistentemente muestra mejoras con rerank a escala completa; (b) esta muestra tiene 20x menos distractores que el corpus real, así que no es representativa de la dificultad real de discriminar entre miles de candidatos similares. Repetir esta medición cuando se embeba el corpus completo (278 560) es la forma correcta de confirmar o descartar el rerank, no esta corrida acotada.

Fase 2 — recalibración de la red de seguridad de figuras vectoriales (2026-09-19)

vector_cluster_min_paths: 6 (valor puesto a priori en el plan) resultó demasiado estricto: medido sobre el PDF real, sólo 4 de 115 clusters vectoriales del documento tienen ≥6 trazos — se perdían diagramas reales confirmados visualmente (problema 37: detectaba 1 de 6 sub-figuras "tipo uno".."tipo seis"; problemas 22/24 no se perdían de milagro porque coincidían justo en el borde). Cambiado a un filtro por tamaño mínimo (vector_cluster_min_size_pt: 15.0, ambas dimensiones del cluster ≥15pt), calibrado con los datos reales: reglas/subrayados decorativos con 1 trazo son ~12-15pt de alto y anchos; diagramas reales (incluso con sólo 2 trazos, p.ej. un círculo + una línea) miden ≥18pt en ambas dimensiones. Con el filtro nuevo: 7/7 de los problemas del QA gate del plan (8, 16, 17, 22, 24, 37, 99) tienen su figura detectada — combinando el detector vectorial (22, 24, 37, 99 usan dibujo vectorial) con imágenes raster embebidas (8, 16, 17, 99 usan imágenes raster; MinerU debe cubrirlas como bloques image, no la red de seguridad). Tests de regresión en tests/test_ingest_pdf.py.

Fase 2 — MinerU real y parser estructural (2026-09-19)

• MinerU 4.0.3, modo local explícito (parse_server.local.mode=managed, tier standard). El default de MinerU trae un modo remoto (mineru.net) — no se usó, para no mandar el PDF del usuario a un servicio externo sin que lo autorice; se levantó el motor local (modelos ONNX de layout/OCR/fórmulas/tablas + VLM MinerU2.5-Pro-1.2B-GGUF vía llama.cpp) y se corrió todo ahí. Documento completo (77 páginas) parseado en 6m47s en CPU.
• Calidad verificada a ojo: fórmulas en LaTeX limpio ($$1+3+5+\dots+(2n-1)=n^2$$), imágenes recortadas correctamente (verificado visualmente el recorte del problema 8 — círculos tangentes con ángulo 60°, coincide exactamente con el enunciado).
• Bug real encontrado y corregido en el parser estructural (parse_structure.py): el primer intento emparejaba por coincidencia de línea ^N\., pero una solución posterior (con sub-casos "1. Prolongar el segmento DC...", "2. Prolongar DA...") pisaba silenciosamente a la solución 1 real con contenido de otro problema — corrupción silenciosa, peor que un faltante. Corregido exigiendo numeración no-decreciente (rechaza números menores al último visto); test de regresión en tests/test_parse_structure.py::test_embedded_subcase_numbering_does_not_hijack_an_earlier_item.
• Resultado final del emparejamiento determinista (sin LLM): 92/100 problema↔solución correctos. Los 8 restantes tienen el número de ítem atrapado dentro de una fórmula LaTeX (\tag{100.}, "2 7. A = B" dentro de un bloque $$) o, en el caso de la solución 1, el documento original simplemente no repite el numeral — ninguno es recuperable con regex; el plan ya preveía esto ("casos ambiguos → una llamada LLM"), pendiente de proveedor de LLM.
• data/corpus/informal.jsonl: 100 InformalChunk reales, con context_summary="" (Contextual Retrieval pendiente de LLM) — text cae a content_md solo.

Fase 0 — verificación final (tarea 5)

lake build sobre lean_project/ (Lean 4 v4.28.0-rc1 + Mathlib v4.28.0-rc1, caché precompilado de 7873 archivos) terminó con "Build completed successfully (3 jobs)": el kernel de Lean aceptó example : 1 + 1 = 2 := rfl. Es la misma verificación de fondo que exige el criterio de aceptación de Fase 0 (el plan menciona lean-interact como herramienta, pero el chequeo real es del kernel, no de qué wrapper lo invoca). lean-interact instalado y funcional para consultas simples (lake --version vía Python), pero su servidor REPL tarda en compilar la primera vez en este filesystem (/mnt/c, montaje 9p) — se retoma cuando se implemente el agente Verificador (Fase 4), no bloquea nada de lo hecho hasta ahora.

Fase 2/4 — Proveedor de LLM/VLM: Gemini (2026-09-19)

#	Decisión	Alternativa descartada	Motivo	Evidencia
13	Proveedor único para vlm_enrichment y llm (RNF-4): Gemini, modelo gemini-3.5-flash (API key del usuario, AI Studio, tier gratis)	gemini-3-flash (nombre inventado en la recomendación inicial — no existe en el API real)	El usuario pidió una opción sin costo por ahora. Se listaron los modelos reales vía GET /v1beta/models con la key real: gemini-2.5-flash ya no está disponible para usuarios nuevos (la API redirige a gemini-3.6-flash); se probó gemini-3.5-flash end-to-end: (a) texto simple, (b) salida JSON estructurada (responseSchema) — funciona, devuelve JSON válido, (c) visión sobre data/parsed/_test/problem8_fig.png — describe correctamente el diagrama (círculos tangentes, ángulo 60°, coincide con la verificación visual ya hecha en Fase 2). gemini-3.6-flash devolvió 503 UNAVAILABLE ("high demand") de forma repetida en esta sesión — se prefiere 3.5-flash por ser el que respondió consistentemente	Llamadas reales a generativelanguage.googleapis.com/v1beta/models/*:generateContent en esta sesión (texto, JSON estructurado, visión)
14	Aviso de privacidad para el usuario, no bloqueante: en el tier gratis de Gemini, Google puede usar prompts/archivos enviados para mejorar sus productos (revisión humana posible), a diferencia del tier pago	—	El corpus B (problemas resueltos olimpiadas.pdf) es un libro publicado, no información sensible del usuario, así que se aceptó seguir; queda registrado por transparencia, siguiendo el mismo criterio que ya se aplicó con MinerU (decisión #4)	—

Fase 2 — cierre de la ingesta del PDF (2026-09-19, segunda sesión)

#	Decisión	Alternativa descartada	Motivo	Evidencia
15	Regenerar el Markdown desde el JSON de bloques de MinerU (rag/mineru_blocks.py, esquema docvortex.middle 2.0) en vez de parchear el full.md de mineru-kit	Editar full.md con búsquedas de texto	Con los bloques (tipo, bbox normalizado, LaTeX) se puede insertar contenido en su posición de lectura, corregir LaTeX antes de renderizar y arreglar los numerales absorbidos; el render propio reproduce el de mineru-kit salvo diferencias conocidas (tablas en formato pipe, <sup>/<sub>, numerales) — verificado página a página en tests/test_mineru_blocks.py	77 páginas, 12 con diferencias, todas en las categorías admitidas
16	Tarea 4 (red de seguridad vectorial): MinerU no perdió ninguna figura real. De 75 clusters vectoriales, 39 caen en bloques image (≥60 %); los 36 restantes son radicales/paréntesis del Equation Editor dibujados como paths (caen en bloques equation/text), 2 tablas correctamente clasificadas (págs. 22 y 75) y 2 clusters que fusionan dos figuras que MinerU recortó por separado (págs. 54 y 76). La cobertura se calcula contra todos los bloques (incl. sub-bboxes de pies de figura), no sólo image	Umbral por cantidad de trazos	Verificado visualmente sobre los 4 casos ambiguos	crop_figures() devuelve 53 figuras y 0 avisos; tests/test_figures.py
17	Cross-check con la capa de texto del PDF para detectar contenido que el layout de MinerU se saltó (find_uncovered_regions: palabras cuyo centro no cae en ningún bbox de MinerU, ≥4 por página) y Plan B acotado: sólo esas regiones se transcriben con el VLM (7 llamadas), no páginas completas	Plan B del plan (página completa por VLM) para todo el documento; confiar ciegamente en MinerU	Hallazgo: la solución 77 completa (pág. 64, un bloque de texto+fórmulas de ~10 líneas) no existe en la salida de MinerU — cero bloques en esa región — y hay 6 líneas/ecuaciones sueltas más perdidas (págs. 23, 25, 50, 57, 66 y el final de la solución 76). La capa de texto no sirve para leer fórmulas (§3 del plan) pero sí para saber dónde hay texto. Por bloque la señal es ruido (párrafos sueltos cubren sólo 30-50 % de los bloques ajustados de MinerU); por palabra es limpia: 9 páginas, 7 con contenido real	pages[64] sin bloques entre y=0.42 y y=0.75; render de la región confirmado visualmente; transcripción VLM recupera 77. 9^2 - 1 = ...
18	Numerales absorbidos en ecuaciones se recuperan sin LLM al renderizar (split_item_number): 2 7. A = B, \begin{array}{l} 5 2. ..., \tag{88.}, \tag{100.} → línea N. + ecuación limpia. Emparejamiento determinista sube de 92 a 98/100; la solución 1 (sin numeral en el original) se asigna por regla "lo que precede al ítem 2"	Split por LLM para los 8	Regex acotada (punto pegado al último dígito; \tag{1} sin punto y decimales espaciados no matchean) y testeada; sólo 55 (numeral perdido por completo) y 77 (bloque perdido) necesitan VLM/LLM	tests/test_mineru_blocks.py::test_numeral_fixes_raise_pairing_to_98_without_llm
19	QA de fórmulas (6b) con guardas de aceptación (enrich._acceptable_fix): el VLM propone muchos cambios cosméticos (puntuación, \dots→...), en fórmulas inline absorbe texto vecino (A B = 3 → AB = 3 \text{ cm}), recorta contenido real cuando el OCR fusionó texto y matemática (C_{100}^{200} \mathrm{es}\ 61 → pierde la respuesta 61; a^2+b^2 ~y~ a+b → pierde a+b) y a veces devuelve LaTeX destrozado (\underset → \raw con caracteres de control por barras sin escapar en el JSON; \mathbb{R} → ℒ). Reglas: (a) caracteres de control o no-ASCII nuevos → rechazo; (b) borrado puro → sólo si cada trozo borrado es envoltorio/basura (sin dígitos ni operadores: \mathrm{..}, \hat{..}, «¿Cuál» absorbido); (c) otro cambio → similitud ≥ 0.8 (arreglo local como r_{l}→r_{1}) y en inline nunca alargar; cambios sólo de puntuación se ignoran	Aplicar todo lo que devuelve el VLM; o descartar 6b	Medido sobre las 70 páginas con ecuaciones del PDF (209 propuestas del VLM): con las reglas finales 76 aceptadas / 133 rechazadas. Con la primera versión de las guardas (sólo «contenido alfanumérico distinto y no alargar inline») se aceptaban 94, entre ellas ~10 que perdían contenido real. Todo cambio y rechazo queda en ingest_report.json (formula_diffs) para revisión; las reglas se evalúan sobre la caché sin gastar cuota	tests/test_enrich.py::test_qa_formulas_guards (13 casos reales)
20	Reintentos: 503 UNAVAILABLE ("high demand") de Gemini es transitorio (segundos) → espera fija de 3 s; 429 (cuota) → exponencial 4→90 s. Hasta 20 intentos	Backoff exponencial para todo	Con backoff exponencial para 503 la corrida se quedaba minutos esperando por un error que se resuelve en segundos (medido: 200 OK y 503 alternados en llamadas consecutivas)	primera corrida: 1 llamada/min; _wait() en enrich.py
21	Cuota diaria del tier gratis de Gemini = 20 solicitudes/día por modelo (GenerateRequestsPerDayPerProjectPerModel-FreeTier, quotaValue: 20, medido con gemini-3.5-flash) — no los 1500/día que reportaban artículos de terceros. Solución: cadena de modelos en configs/versions.yaml (fallback_models): al recibir 429 con quotaId *PerDay* el enriquecedor pasa al siguiente modelo y sigue; cada figura/card guarda description_model con el modelo real que la produjo, y la caché es independiente del modelo (un resultado ya calculado no se recalcula). Verificado que gemini-3.5-flash-lite, gemini-3.1-flash-lite, gemma-4-31b-it, gemma-4-26b-a4b-it y gemini-3-flash-preview aceptan imagen + responseSchema	Esperar 24 h por modelo; pasar al tier pago	~230 llamadas por documento no caben en 20/día; las cuotas son por modelo, así que encadenarlos multiplica el presupuesto gratis sin cambiar de proveedor. Trade-off aceptado: heterogeneidad de modelos entre figuras/cards de un mismo documento (queda registrada por registro)	curl 429: Quota exceeded for metric: generate_content_free_tier_requests, limit: 20, model: gemini-3.5-flash; tests/test_enrich.py
22	La API key va en el header x-goog-api-key, no en ?key=	Query string (como en las pruebas iniciales con curl)	Con ?key= la key aparece en la URL de cualquier traceback/log de httpx (pasó en ingest_run.log de la corrida fallida)	enrich.py::_generate_with

Fase 3 — servicio de recuperación y citación (2026-09-20)

#	Decisión	Alternativa descartada	Motivo	Evidencia
23	Plantillas de consulta por mode (configs/retrieval.yaml: query_instructions) como instrucción de Qwen3-Embedding; los documentos siguen embebidos sin instrucción, así que cambiar una plantilla no obliga a re-indexar. La de nl es idéntica a la usada en la Fase 1 para que las métricas se reproduzcan	Una sola instrucción fija (Fase 1)	El model card de Qwen3-Embedding recomienda instrucciones específicas por tarea; el costo es cero en el índice	embed.py::embed_queries(instruction=...) + caché de embeddings de consulta (el orquestador repite consultas entre intentos)
24	Modo error: identificadores Lean del mensaje (unknown identifier 'X', `X`, nombres con punto) → búsqueda exacta decl_name IN (...) fijada al tope del resultado (por encima del rerank), más FTS con los tokens del nombre y denso sobre el resto del mensaje/goal	Confiar en FTS/denso para encontrar el nombre	Un identificador que existe es verdad mecánica: no debe depender de que el cross-encoder lo puntúe bien. Verificado con reranker adverso (test) y sobre el índice real	tests/test_retriever.py::test_error_mode_pins_exact_identifier...; tests/test_retriever_integration.py
25	Filtros §8.1 como prefiltro SQL de LanceDB (doc_ids, unit_types, kinds en Mathlib, math_area en informal vía array_has_any), aplicados tanto al canal denso como al FTS	Post-filtrar los candidatos	Prefiltro = los N candidatos son todos válidos; post-filtro puede vaciar el resultado. math_area como boost (no exclusión) queda para el orquestador (Fase 4, tarea 3): el retriever ofrece el filtro estricto y el llamador decide	LanceDB 0.39: where(..., prefilter=True) en vector y FTS, array_has_any verificado
26	Dedupe: una figura cuyo problem card también fue recuperado se colapsa en el card (que ya lleva figure_ids y las figuras adjuntas); una figura sola sigue siendo hit válido. max_per_module desactivado por defecto (0)	Devolver card y figura como dos hits; límite por módulo activo	Dos hits del mismo problema gastan presupuesto de contexto del LLM sin sumar información; el límite por módulo no se puede calibrar con la tabla de muestra (13 736 filas) — se deja el knob para la Fase 5	test_figure_chunk_collapses_into_its_card...
27	Figuras adjuntas (include_figures): tabla LanceDB figures (metadatos, sin vectores) construida desde figures.jsonl; el hit informal trae [{figure_id, image_path, description, page, bbox, figure_type, labels}]	Leer figures.jsonl en memoria; meter image_path en los chunks	Misma base de datos para todo (publicable como una carpeta en HF Hub, §9.2); index.build_table(fts_columns=None) cubre tablas sin FTS	python -m ragsolver.rag.index --table figures
28	evaluate.py pasa por Retriever.search (aceptación de Fase 3: "misma función, sin duplicar lógica"): las 4 variantes sólo cambian Retriever.channels (denso / FTS / ambos) y rerank	Mantener el bucle propio de Fase 1	Si la evaluación y los agentes usan código distinto, las métricas no describen lo que corre en producción	test de integración: orden del canal denso == vector_search crudo
29	CLI ragsolver ([project.scripts]): ragsolver search "..." --corpus informal --mode exemplar, ragsolver ingest --pdf ...	Sólo python -m ...	Lo pide el plan (Fase 2 tarea 9, Fase 3 tarea 7); es un despachador de 20 líneas. Ojo: uv sync sin --extra dev --extra ingest desinstala pytest y MinerU (pasó en esta sesión)	src/ragsolver/cli.py
30	Ablación enabled=false (Fase 4 tarea 7) ya implementada en el retriever: devuelve vacío y emite la traza igual (llm_calls=0, hits=[])	Implementarla en el orquestador	3 líneas y un test; así la métrica "contribución del RAG" (8.3) no depende de que el orquestador recuerde saltarse el nodo	test_ablation_disabled_returns_empty_but_still_traces

Corrección de Fase 1 encontrada en Fase 3 (2026-09-20)

#	Decisión	Alternativa descartada	Motivo	Evidencia
31	Bug de ingesta de Mathlib corregido: en el JSONL de LeanSearch v2 el campo name es la lista de componentes del nombre (["GCDMonoid","dvd_gcd"] = GCDMonoid.dvd_gcd), no una lista de alias. ingest_mathlib.py tomaba name[0] → el 90 % de las declaraciones (todas las de ≥2 componentes: 280 701 de 310 579) quedaba con decl_name, chunk_id y docs_url incorrectos y repetidos (en la tabla de muestra: 13 736 filas, sólo 1 145 chunk_id únicos). Ahora decl_name = ".".join(name), decl_names_alt = []	—	Detectado por el test de integración de Fase 3 (el orden del canal denso no coincidía con vector_search porque el RRF fusionaba filas distintas con el mismo id). Invalida dos conclusiones de Fase 1: (a) "sólo 117/540 nombres gold existen en el corpus" era el bug — con el nombre completo se encuentran 503/540; (b) el "recall condicionado 0.947" estaba inflado: sólo matcheaban los 60/200 gold de un componente (Lattice, GaloisConnection...) y cualquier fila Lattice.* contaba como acierto para el gold Lattice	tests/test_ingest_mathlib.py::test_name_components_are_joined...; scripts/build_eval_sample.py: gold_found_in_corpus: 503
32	Números corregidos de Fase 1 (tabla nueva: 503 gold QR/MPR + 3000 distractores = 3 503 filas, ids únicos; 946 consultas de MathlibQR; cobertura 793/946 = 83.8 %): recall@10 denso 0.665 / BM25 0.594 / híbrido 0.656; nDCG@10 denso 0.565 / BM25 0.472 / híbrido 0.538; MRR denso 0.537 / híbrido 0.504. Recall condicionado a cobertura: denso 0.79, híbrido 0.78. Con ids correctos el denso solo iguala o supera al híbrido en esta muestra; BM25 aporta menos de lo que sugería la Fase 1. Se mantiene el híbrido como default del retriever porque el modo error (identificadores exactos) y las consultas con nombres de Mathlib dependen del canal léxico; la ablación queda documentada para Fase 5	Cambiar el default a denso	La diferencia denso/híbrido es pequeña (< 1 punto de recall) y la muestra sigue siendo 80x menor que el corpus real; la decisión de canal se revisa con el corpus completo	data/eval/results/fase1_redo_mathlibqr_sample3503_norerank.json

Fase 4 — agentes y verificador (2026-09-20)

#	Decisión	Alternativa descartada	Motivo	Evidencia
33	Cliente LLM único (ragsolver/llm.py): provider: gemini (REST) u openai_compatible (base_url + api_key_env: OpenRouter/OpenAI/Ollama/vLLM), misma interfaz generate(prompt, schema, images, system), misma cadena de modelos por cuota diaria. El Enricher de Fase 2 pasa a usarlo (menos código duplicado). OpenRouter queda preparado por config, sin probar (no hay key)	Un cliente por proveedor	El usuario quiere poder migrar a OpenRouter cuando la cuota gratis de Gemini no alcance; el JSON Schema estándar se traduce al subconjunto de Gemini en un solo lugar	configs/versions.yaml: llm, vlm_enrichment (bloque comentado de OpenRouter)
34	Verificador = lake env lean por proceso (sin REPL) REEMPLAZADA por #40: el backend por defecto pasó a ser el REPL persistente (LeanChecker, lean-interact) por el costo del import por proceso; verify() (sin REPL) sigue existiendo como respaldo. Lo que sí sigue vigente de esta entrada: el enunciado nunca lo escribe el LLM — el Formalizador devuelve sólo las tácticas tras := by y se empalman en el theorem del problema (splice_proof); ver también #69-71 (validación de tácticas y auditoría de axiomas, que reemplazan la lista sorry/admit/axiom/native_decide de esta entrada)	lean-interact REPL; dejar que el LLM emita el teorema completo	Un LLM que reescribe el enunciado puede debilitarlo (es el fallo clásico en miniF2F); el empalme lo hace imposible	src/ragsolver/lean/verify.py, tests/test_orchestrator.py
35	Caché de Mathlib en ext4 (~/ragsolver_cache/lean_project, misma tag v4.28.0-rc1, oleans vía lake exe cache get): el verificador la usa si existe (RAGSOLVER_LEAN_PROJECT la sobreescribe). El repo del usuario no se mueve	Verificar contra /mnt/c	Medido: import Mathlib desde /mnt/c (9p) tardó 18 min bajo contención (2.6 GB RSS) y 4 min un archivo con imports acotados; copiar .lake (6.6 GB) por 9p iba a ~40 MB/min	verify._lean_project(); tiempos en lean_project/scratch/time*.txt
36	Grafo LangGraph sin checkpointer persistente; presupuesto RNF-3 (llm_budget: 20) aplicado antes de cada llamada en el propio grafo; ablación "sin Crítico" = k_max: 1 sin llamada al Crítico; "sin RAG" = rag: false (0 recuperaciones); líneas base A/B de la propuesta §8.2 como modos de una llamada	SqliteSaver; presupuesto sólo en el runner	Reanudar corridas no hace falta todavía; el presupuesto dentro del grafo garantiza el límite aunque el runner cambie	orchestrator/graph.py, configs/agents.yaml: configs
37	5 teoremas triviales de referencia definidos por el agente (data/eval/problems/dev_trivial.jsonl: n + 0 = n, conmutatividad, cuadrado del binomio en ℤ, par ⇒ cuadrado par, transitividad de ∣ en ℤ)	—	La propuesta los cita en una "Sección 6.5" que no existe en el texto entregado	Propuesta_Proyecto_Final_IA_UPTC.pdf (§6.3 → §6.7)

Fase 5 — evaluación (2026-09-20)

#	Decisión	Alternativa descartada	Motivo	Evidencia
38	Premisas gold desde las pruebas verificadas publicadas por DeepSeek-Prover-V2 (minif2f-solutions.zip, 438 pruebas Lean 4/Mathlib sobre los enunciados de miniF2F-v1), cruzadas por nombre con los enunciados informales de miniF2F-v2s: 352 problemas, 402 lemas únicos, 5.3 premisas/problema (identificadores de la prueba que existen como decl_name en el corpus)	Pruebas de miniF2F-v2 (el plan asumía que las publicaba)	El repo público de miniF2F-v2 trae formal_proof vacío en las 488 filas. Las pruebas de DSP-V2 son verificadas y públicas; que sean sobre los enunciados v1 no afecta a "qué lemas usa una prueba real del problema"	scripts/build_premise_gold.py → data/eval/premises_gold.jsonl
39	Gold informal anotado por el asistente (30 consultas en inglés: 15 dependientes de figura con entidades clave esperadas, 15 sin figura; paráfrasis y análogos de problemas del PDF), campo annotator explícito	Anotación humana	No hay anotador humano disponible en esta sesión; la anotación queda auditable en data/eval/informal_gold.jsonl para que el equipo la revise/corrija	scripts/eval_informal_gold.py
40	Presupuesto de RAM del pipeline de Fase 4 (máquina de 7.5 GB): embedder Qwen3-Embedding-0.6B en bfloat16 (1.8 GB de pico vs 3.6 GB en fp32; métricas idénticas en 40 consultas: denso 0.75/0.62/0.583, híbrido 0.675/0.53/0.491), sin reranker en la recuperación de los agentes (configs/agents.yaml: retrieval.rerank: false; el cross-encoder son 2.4 GB más y sumó +2.5 puntos de recall@10 en la muestra), REPL de Lean 1.9 GB. Total ≈ 4.2 GB	fp32 + reranker + REPL (≈ 7 GB)	La primera corrida real de Fase 4 fue detenida por el sistema por memoria crítica con la configuración pesada. REPL medido: import Mathlib 284 s una vez, luego 0.2-0.4 s por teorema (lean-interact 0.11.5, sin memory_hard_limit_mb — con límite de espacio de direcciones el REPL muere con "failed to create thread" por el mmap de los .olean)	RAGSOLVER_EMBED_BF16=0 restaura fp32

Fase 6 — empaquetado (2026-09-20)

#	Decisión	Alternativa descartada	Motivo	Evidencia
41	Publicación en HF Hub sin el corpus informal: el dataset lleva el índice de Mathlib (Apache 2.0), el corpus normalizado y la evaluación; el PDF de olimpiadas, sus recortes y su texto quedan fuera (Document.redistributable=false, licencia desconocida). El script sube informal/figures sólo si todos los documentos son redistribuibles	Subir todo	Plan §12 (licencias): "no publicar recortes ni texto de fuentes no redistribuibles; citar igual". Requiere HF_TOKEN y repo del usuario — no ejecutado	scripts/publish_hf.py --dry-run
42	Demo Gradio con rerank apagado por defecto y carga perezosa de modelos; en un Space, el índice se descarga con snapshot_download (RAGSOLVER_HF_DATASET)	Cargar todo al arrancar	El cross-encoder son +2.4 GB; un Space gratuito tiene 16 GB pero el embedder + índice ya tardan minutos en arrancar	demo/app.py
43	Métricas de IR propias (rag/metrics.py: recall@k, nDCG@k, MRR) en vez de ranx para las corridas de evaluación; evaluate.py y eval_premises.py guardan además los hits crudos (_runs) para recomputar sin repetir búsquedas	Seguir con ranx	En dos corridas largas del CLI (--sample 200 y --sample 100, 4 variantes intercaladas, 30-60 min) ranx devolvió recall@10 ≈ 0.11 para todas las variantes; las mismas listas de hits guardadas en las trazas JSONL, recomputadas con las métricas propias, dan denso 0.76 / BM25 0.56 / híbrido 0.66 / híbrido+rerank 0.71 (y la misma muestra en proceso con ranx también da 0.76). No se pudo aislar la causa (sospecha: caché JIT de numba de ranx en procesos largos); las métricas propias se verifican iguales a ranx en tests/test_metrics.py sobre runs aleatorios	trazas /tmp/ragsolver-eval-j12vkawz (400 eventos) vs fase1_redo_mathlibqr_sample3903_100q.json original
44	Resultado de las ablaciones (n=13 dev): el Crítico es el componente que más aporta (+0.23 pass@1 vs. sin Crítico); el RAG no mejora pass@1 en este conjunto (−0.08, McNemar p=1.0) y multiplica los tokens ×2.9; la verificación formal evita 5/13 falsos positivos de la línea base sin verificación. Se reporta tal cual; no se cambia el diseño	Quitar el RAG del pipeline	n=13 con problemas triviales/mathd que se cierran con simp/omega/norm_num/ring/decide; el aporte del RAG hay que medirlo en el conjunto de 30-60 problemas estratificados del plan (§8.1), donde hacen falta lemas concretos. Precisión de uso de lemas 0.011: el Autoformalizador rara vez cita nombres; las re-recuperaciones por lema faltante (3) no encontraron los identificadores propuestos por el Crítico (nombres inexistentes en Mathlib)	data/eval/runs/f5-ablations/, docs/eval_report.md
45	Runner reanudable + parada limpia por cuota: con el mismo --run-id se saltan los pares (config, problema) ya presentes en results.jsonl; si todos los modelos agotan la cuota diaria, la corrida termina con status: quota_exhausted (los problemas pendientes no se marcan como fallos) y se relanza al día siguiente con el mismo comando (scripts/run_eval_v1.sh)	Marcar los pendientes como error; empezar de cero	El experimento principal (~1 800 llamadas) no cabe en un día de tier gratis y la sesión puede reiniciarse	tests/test_orchestrator.py::test_run_suite_resumes...
46	Self-consistency del Generador (propuesta §6.3) implementada como generator_samples: n — n bocetos, se elige el medoide por solapamiento de tokens; apagada por defecto (n=1) y cada muestra cuenta en el presupuesto RNF-3	Votación sobre "respuesta final"	Los bocetos de prueba no tienen una respuesta discreta para votar; el medoide es la versión estándar para salidas abiertas. Encendida triplica las llamadas del Generador, por eso se reserva como configuración de ablación opcional	tests/test_orchestrator.py::test_generator_self_consistency...
47	Experimento principal (eval_v1) con OpenRouter y un solo modelo (deepseek/deepseek-v4-flash-0731, $0.04/M entrada, $0.16/M salida; respaldo google/gemini-2.5-flash-lite), tope de gasto de US$0.50 fijado por el usuario en la cuenta	Tier gratis de Gemini con cadena de modelos (como en el desarrollo)	(a) 5 configs × 60 problemas ≈ 1.6 M tokens de entrada: con el tier gratis serían ~3 días y mezclaría modelos entre problemas (confunde modelo y configuración); (b) costo estimado ≈ US$0.11 (flash-lite ≈ 0.22; qwen3.7-flash descartado: 2 500 tokens de "pensamiento" por llamada trivial); (c) DeepSeek V4 Flash es el más fuerte en matemática de los baratos y responde JSON válido con nuestros esquemas (29 s por llamada con razonamiento). Con el índice completo de Mathlib se repiten sólo full y no_critic (≈ US$0.06)	prueba de esquemas Planner/Formalizer en 3 modelos; configs/versions.yaml
48	GPU AMD usada desde Windows con Vulkan (llama.cpp) para embeddings: llama-server.exe (build win-vulkan) del lado de Windows sirve el GGUF f16 de Qwen3-Embedding-0.6B por HTTP y WSL lo consume (RAGSOLVER_EMBED_BACKEND=llama). Vectores intercambiables con sentence-transformers (cos ≥ 0.9996 en 153 chunks informales y 64 declaraciones de Mathlib); ~48 textos/s vs ~5 en CPU → corpus completo (278k) en ~96 min en vez de ~15 h. El bug de ROCm en WSL2 (#11-12) no aplica: el driver de Windows expone la GPU por Vulkan sin pasar por dxg/ROCm	ROCm en WSL2 (bloqueado); PyTorch-ROCm en Windows nativo (más pesado de instalar)	Confirmado en el log del servidor: Vulkan0 : AMD Radeon RX 9060 XT (16304 MiB) con el modelo cargado en la GPU (1.8 GB). Alcance desde WSL vía el gateway (ip route show default), servidor en --host 0.0.0.0. Tope medido ~48 textos/s (8 slots, lotes de 32-64, 8 hilos)	tools/llama-vulkan/ (no versionado), scripts/embed_full_mathlib.sh, embed.py::_llama_embed
49	Chunks paper_section para el texto expositivo (mineru_blocks.section_chunks): el Markdown de MinerU (ya con las correcciones de Fase 2) se corta por títulos y párrafos en trozos de ≤ 3 000 caracteres con section_path y páginas; `ingest_informal --sections front	alllos agrega al mismoinformal.jsonl(por defectonone: el PDF de ejemplo es un problemario, sus soluciones ya van como problem_card`)	Cortar por tamaño fijo con solapamiento	Plan §6.2 paso 7 pide chunks que respeten la estructura; por tamaño fijo parte demostraciones por la mitad. Sólo el front-matter del PDF (prólogo/índice) aplica hoy, así que queda apagado y probado (tests/test_mineru_blocks.py)
50	eval_v1 con DeepSeek V4 Flash sin cadena de razonamiento (reasoning_effort: "off", max_tokens: 4000) y 6 hilos en el runner (--workers 6; lock en el REPL de Lean y en la escritura de trazas)	Razonamiento medium/low; corrida secuencial	Medido en el planner de mathd_algebra_209: 91 s (medium, 2 932 tokens de salida), 76 s (low), 24 s (off, 707 tokens); con effort por defecto la primera llamada del experimento llevaba > 15 min sin respuesta. Secuencial con razonamiento: 300 pares × ~6 llamadas × 80 s ≈ 40 h; con 6 hilos y sin razonar ≈ 2 h. Costo estimado desde los tokens del dev run: ≈ US$0.09 (tope US$0.50). off va entre comillas: PyYAML lee off sin comillas como False	configs/versions.yaml: llm, orchestrator/run.py::run_suite(workers=), scripts/run_eval_v1.sh
51	Bug corregido antes de eval_v1: sangría de las tácticas. strip_code_fences hacía code.strip() (quitaba la sangría sólo de la primera línea) y splice_proof añadía 2 espacios a todas; con tácticas ya indentadas (DeepSeek las devuelve a 2 espacios) el bloque quedaba have en col. 2, su cuerpo en col. 6 y el resto en col. 4 → unsolved goals en los 3 intentos, y el Crítico diagnosticaba bien ("indentation") sin poder arreglarlo. Ahora ambos hacen textwrap.dedent (se quita la sangría común, se conserva la relativa). Los 7 pares de la primera corrida quedaron en data/eval/runs/_invalid/eval-v1-indent-bug/ y se repitieron. Además el runner arranca el REPL (import Mathlib) antes de lanzar los hilos, para no cargar ese tiempo al wall_seconds de los primeros problemas (los 6 primeros marcaban ~1 750 s; en régimen ~180-240 s)	Dejar que el Crítico lo corrigiera	El Crítico no controla el empalme; era un bug determinista del sistema, no del modelo. En las corridas de desarrollo con Gemini no se manifestó (devolvía las tácticas sin sangría), por eso pasó los tests de aceptación	tests/test_orchestrator.py::test_splice_proof_keeps_nesting..., data/eval/results/eval_v1_indent_bug.log
52	Carga y uso del embedder de torch bajo un lock (embed._TORCH_LOCK) y precalentamiento del embedder y del REPL antes de lanzar los hilos del runner	Confiar en lru_cache	Con 6 hilos arrancando a la vez, lru_cache no evita cargas concurrentes del modelo: el segundo lanzamiento de eval_v1 falló en los 60 pares full con expected m1 and m2 to have the same dtype (float != BFloat16) (modelo a medio convertir a bf16 mientras otro hilo codificaba); el primero sobrevivió por suerte. Codificar en serie no cuesta: torch ya usa todos los núcleos por lote. Pares inválidos en data/eval/runs/_invalid/eval-v1-dtype-race/ (0 llamadas LLM, sin costo)	src/ragsolver/rag/embed.py, orchestrator/run.py
53	by suelto al inicio de las tácticas se descarta en strip_code_fences (también := by). Tercer relanzamiento de eval_v1 (00:56) para que todos los pares corran con el mismo código; los 12 pares full previos (5 resueltos, 7 fallos; ≈ US$0.02) quedan en _invalid/eval-v1-stray-by/	Dejar que el Crítico lo corrija en el intento 2	En 8 de 30 intentos DeepSeek empezó el bloque con by → unexpected token 'by' y un intento perdido por formato, no por matemática; en dos problemas se repitió en los 3 intentos. Mezclar código viejo y nuevo dentro de una configuración confundiría el análisis	tests/test_orchestrator.py::test_strip_code_fences_and_repeated_statement
54	eval_v1 detenida a las 03:15 por el tope de US$0.50 de la key de OpenRouter (limit_remaining: 0, usage: 0.506): 42 pares full válidos (10 resueltos), el resto devolvía 403. Costo real ≈ US$0.005 por par full (≈ 100 pares full entre válidos e inválidos = US$0.50), 5× la estimación del #47 (los prompts del Generador/Formalizador con 8 lemas + ejemplares pesan 5.3k tokens por llamada, 26k tokens de entrada por par; y OpenRouter enruta a proveedores hasta 2× más caros que el precio base). Para terminar hacen falta ≈ US$0.45 (18 full + 60 no_rag + 60 no_critic + 120 líneas base) y ≈ US$0.40 más para repetir full/no_critic con el índice completo → subir el tope de la key a ≈ US$1.50 (la cuenta tiene US$3.50 de crédito). Los pares con error (403, JSON truncado ×2, carrera en la caché de consultas ×2) se apartaron a _invalid/eval-v1-errors/ para que el runner los repita al reanudar. Dos bugs más corregidos: reintento único con el doble de max_tokens si el JSON llega truncado (Agents._call), y embed_queries responde desde el dict local en vez de releer la caché FIFO (otro hilo podía desalojar la entrada recién escrita → KeyError)	Seguir con la cadena de modelos gratis de Gemini	Mezclaría modelos entre configuraciones (#47)	data/eval/results/eval_v1.log, tests/test_orchestrator.py::test_agent_call_retries_once_on_truncated_json
55	Bug en build_table por bloques: table.add(batch) or table — en lancedb ≥ 0.25 add devuelve un AddResult (truthy) y el segundo bloque llamaba .add sobre él. Sólo se manifestaba con más de chunk (5 000) filas: la muestra de 3 903 nunca lo tocó. La tabla mathlib_full quedó con 10 000 filas y la cadena evaluó contra ella (resultado descartado); se reconstruye completa y se relanza la cadena	—	Test test_build_table_streams_in_chunks (chunk=1)	src/ragsolver/rag/index.py::_write
56	Métricas del retriever sobre el índice completo (278 160 declaraciones): MathlibQR (100 consultas, misma semilla que 1b) recall@10 denso 0.41 / BM25 0.25 / híbrido 0.38 / híbrido+rerank 0.45 (vs 0.76 / 0.56 / 0.66 / 0.71 en la tabla de 3 903); premisas gold recall@20 0.010 (informal) / 0.018 (formal) (vs 0.153 / 0.180). Se reportan como la medida realista; los de la muestra quedan etiquetados como inflados por el pool	Reportar sólo la muestra	El orden de las variantes se conserva y el reranker pasa a ser lo que más aporta (+7 puntos sobre el híbrido); premisas por enunciado completo es una cota inferior (unidad real = subobjetivo)	data/eval/results/fase1_full_mathlibqr_100q.json, fase5_premises_full.json, docs/eval_report.md §1c
57	Enrutamiento al proveedor más barato en OpenRouter (provider_sort: price → "provider": {"sort": "price"}), y 402/403 tratados como cuota agotada (DailyQuotaExhausted → siguiente modelo → parada limpia del runner)	Dejar el enrutamiento por defecto; grabar los 403 como error	El precio agregado que muestra OpenRouter para DeepSeek V4 Flash llegó a $0.64/M de salida (4× el base) según el proveedor elegido; la key agotada generó 74 filas error en un minuto (#54). GPT Luna, sugerido por el usuario, cuesta $0.20/$1.20 por M (2.5× más por par) — descartado. Reanudado 21-09 21:48 con el tope de la key subido a US$1	src/ragsolver/llm.py, configs/versions.yaml
58	JSON inválido persistente = fail contado, no error (InvalidLLMOutput en Agents._call tras el reintento; Orchestrator.solve lo convierte en status: fail, error_types: llm_output_invalid:<agente>, con las llamadas y tokens de ese agente) y las líneas base no pueden tumbar la corrida (solve_pair captura excepciones → fila error/fail; antes una excepción en run_baseline habría abortado run_suite y perdido los pares en vuelo)	Dejar error con 0 llamadas	imo_1992_p1 (full) generó texto degenerado hasta max_tokens dos veces (3 700 s): es un fallo del sistema ante el problema y debe contar con su costo. Relanzado a las 22:56 (51 pares válidos conservados)	tests/test_orchestrator.py::test_persistently_invalid_json_counts_as_fail_with_calls
59	Causa raíz del sobrecosto: bucle de reintentos oculto. LLM._generate_with reintentaba hasta 20 veces (tenacity) cuando la respuesta no era JSON válido, y sólo contabilizaba tokens de la respuesta final: cada intento fallido gastaba hasta max_tokens (4 000-8 000) de salida sin aparecer en tokens_out. En problemas donde DeepSeek degenera (IMO: texto repetido hasta el tope), una sola llamada del planner podía costar 20 × 4 000 tokens (+ 20 × 8 000 en el reintento de _call): imo_1992_p1 tardó 3 700 s. Explica que la key gastara US$0.49 en 10 pares tras reanudar (≈ US$0.02 según los tokens contados) y el 5× del #54. Corregido: sin reintento por JSON en el cliente (sólo por errores de transporte/5xx), un único reintento contabilizado en Agents._call, y costo exacto por llamada desde OpenRouter (usage: {include: true} → usage.cost, guardado en la traza y sumado en [cost] al final de la corrida). Key agotada de nuevo a las 23:06 (US$1.00): quedan 8 full + 60 no_rag + 60 no_critic + 120 líneas base ≈ US$0.10 a precio de lista, y eval-v1-full ≈ US$0.16	Subir max_tokens; mantener los reintentos	Los reintentos sobre salida degenerada no la arreglan (misma semilla y temperatura baja) y multiplican el costo	src/ragsolver/llm.py::_retryable, data/eval/results/eval_v1_part1.log
60	Índice ANN en mathlib_full: IVF_SQ (256 particiones, cuantización escalar de 8 bits, métrica L2 sobre vectores normalizados = coseno) con nprobes 32 y re-ranking exacto de los 5 × k mejores (refine_factor 5). Medido con 200 consultas sintéticas (normalize(e_i + e_j)): recall@10 = 0.989 y recall@50 = 0.977 respecto de la búsqueda exacta, latencia densa p50 2.71 s → 0.045 s (p95 2.89 → 0.078 s), construcción 67 s. Los agentes de eval-v1-full usan el ANN; las métricas de §1c se midieron con búsqueda exacta y se repiten con ANN al final de la cadena (§1d)	Búsqueda exacta (plana)	La búsqueda plana lee la columna de vectores completa (1.1 GB) por consulta: ~0.8 GB de RSS por búsqueda; con 6 hilos concurrentes excedía la RAM de la máquina (7.5 GB) junto al REPL de Lean y el embedder. Criterio del plan §488: latencia p50 < 12 s en CPU — se cumple de sobra	scripts/ann_recall.py → data/eval/results/ann_mathlib_full.json; index.py::build_ann_index
61	JSON inválido persistente se resuelve dentro del grafo (Orchestrator._guard envuelve cada nodo: InvalidLLMOutput → status: fail, fail_reason: llm_output_invalid:<agente>, sumando las llamadas y tokens del agente roto a lo acumulado). Antes la excepción salía de graph.invoke y el reporte perdía todo lo anterior: imo_1965_p1 figuraba con 2 llamadas y 0 lemas cuando había hecho 4 replanificaciones (~12 llamadas). Las 6 filas afectadas (todas full, problemas AMC/IMO donde DeepSeek divaga dentro del JSON hasta el tope de tokens) se apartaron a _invalid/eval-v1-accounting/ y se repiten. Además el runner aparta las trazas de pares interrumpidos a traces/interrupted/ antes de repetirlos	Estimar lo perdido desde las trazas	Con razonamiento apagado el modelo "piensa" dentro de los campos del JSON en problemas difíciles; es un fallo legítimo del sistema pero su costo debe contarse completo	tests/test_orchestrator.py::test_invalid_json_mid_run_keeps_accumulated_calls_and_evidence
62	Enrutamiento de OpenRouter por tope de precio + velocidad (provider_routing: {max_price: {prompt: 0.10, completion: 0.20}, sort: throughput}, enviado tal cual en provider). Los precios por proveedor de DeepSeek V4 Flash cambiaron desde el #47 (entrada 0.03-0.44, salida 0.16-1.32 US$/M); sort: price (#57) ordena por precio de entrada y eligió OpenInference: $0.03 entrada pero $0.80/M salida y 19 tok/s. Medido con usage.cost: 66k tokens de salida costaron US$0.054 entre 22:32 y 22:50. Con el tope quedan StreamLake ($0.053/$0.158), DeepInfra ($0.06/$0.18) y Makora ($0.09/$0.195): verificado ~$0.16-0.20/M de salida y 2-4 s por llamada corta. Consecuencia para la validez: los pares se sirvieron por varios proveedores (cuantización fp8 en su mayoría); el modelo es el mismo y se reporta como limitación	sort: price; fijar un solo proveedor (order, allow_fallbacks: false)	Fijar uno solo expone la corrida a su caída (StreamLake: uptime 98 %, latencia p90 44 s)	configs/versions.yaml: llm.provider_routing, prueba con max_price imposible → 404 (unidades US$/M confirmadas)
63	Se repiten los 15 pares full afectados por los reintentos ocultos (#59). Detectados en las trazas como llamadas cuya latencia no la explica su salida contabilizada (> 180 s y > 0.3 s/token; la mediana de la corrida es 0.033 s/token): p.ej. un formalizador de 812 s que devolvió 10 tokens. 14 de los 15 habían fallado y 1 estaba resuelto (mathd_algebra_209); con reintentos ocultos esos pares tuvieron "más oportunidades" que las configuraciones que corrieron después del arreglo, un sesgo a favor de full de a lo sumo 1/60 en pass@1 y una subestimación de su costo. Se apartan a _invalid/eval-v1-hidden-retries/ y la cadena los repite con el código final (≈ US$0.15). Los 39 pares restantes no tuvieron reintentos y se conservan	Conservarlos con una nota; repetir los 54	Repetir sólo los afectados restaura la consistencia al menor costo; la detección es heurística (un reintento rápido de pocos tokens podría pasar el umbral) y así se reporta	umbral calibrado con la distribución de s/token de 438 llamadas
64	Dentro del tope de precio, ordenar por precio (sort: price + max_price 0.10/0.20) en vez de por velocidad: para la mezcla real de tokens (≈ 2:1 entrada:salida) StreamLake cuesta 0.26 US$ por "unidad" contra 0.30 DeepInfra y 0.375 Makora (−30 %), a cambio de ~2× más latencia. Medido tras el #62: US$0.046 en 13 pares (0.0035/par, sesgado por 6 problemas IMO que divagan hasta el tope de tokens). Proyección con el cambio: ≈ US$0.45 para lo que falta de eval_v1 (239 pares) y ≈ US$0.30 para eval-v1-full, frente a US$0.29 disponibles → hace falta subir el tope de la key ≈ US$0.5	Seguir con sort: throughput	El presupuesto, no el tiempo, es la restricción activa	data/eval/results/chain.log
65	Líneas base con un esquema propio y campos obligatorios (BaselineAOutput{proof_tactics}, BaselineBOutput{natural_language_proof, self_assessed_correct}) en vez de un BaselineOutput común con los tres campos opcionales. Con el común, DeepSeek V4 Flash escribió la prueba en natural_language_proof y dejó proof_tactics vacío en 58/60 problemas de la línea base A (Lean recibió un cuerpo vacío: unexpected end of input), y en la B devolvió a veces una prueba vacía con self_assessed_correct: true. En el desarrollo con Gemini no ocurrió (A resolvió 8/13). Las 120 filas se apartaron a _invalid/eval-v1-baselines-schema/ y se repitieron. La semántica es la misma que la de los agentes principales (campo obligatorio, sin min_length): un campo presente pero vacío sigue contando como intento fallido, como en el formalizador (8-13 % de sus llamadas en las tres configuraciones del pipeline, que se reporta como limitación)	Añadir min_length y reintento a todos los agentes	Cambiaría el trato de las salidas vacías sólo para las líneas base respecto de las 180 filas ya corridas; se deja como trabajo futuro para todos a la vez	tests/test_orchestrator.py::test_baseline_schemas_require_the_field_each_baseline_produces
66	eval_v1 cerrado (300/300 pares, mismo código para todos) y eval-v1-full no ejecutado. Resultado: full 9/60, no_rag 9/60, no_critic 4/60, línea base A 5/60, línea base B se autoevalúa correcta en 55/60 (11 confirmadas por el kernel en alguna configuración); ninguna diferencia pareada sobrevive a Bonferroni. Costo de la cadena final medido por llamada: US$0.314 (eval) + US$0.053 (líneas base repetidas); gasto total de la key en el proyecto ≈ US$1.58 de US$2.00, de los cuales ≈ US$0.9 se perdieron por el defecto de reintentos ocultos (#59) y el proveedor caro (#62). eval-v1-full (≈ US$0.30) queda listo en scripts/run_chain.sh pero no se corre sin aprobación explícita del usuario, que pidió gastar sólo lo necesario para terminar eval_v1	Correrlo con el saldo restante de la key	El usuario autorizó "centavos" para terminar el experimento principal; el extra no lo exige la propuesta	docs/eval_report.md, docs/final_report.md §6.3
67	PutnamBench fuera del conjunto de evaluación v1 (desviación de la propuesta §1/§8.1, que lo nombra como fuente secundaria junto a miniF2F); el estrato de nivel 3 (IMO) de miniF2F-v2 cumple el papel del nivel más difícil	Portar los enunciados de PutnamBench al pin v4.28.0-rc1	PutnamBench mantiene sus enunciados contra su propio pin de Lean/Mathlib; portarlos y re-verificarlos contra el pin común del índice y del verificador no cabía en esta iteración, y cada problema adicional cuesta llamadas de LLM en 5 configuraciones. Queda como trabajo futuro (informe §10)	data/eval/problems/README.md, docs/final_report.md §5
68	ANN validado con consultas reales: MathlibQR (las mismas 100 consultas de §1c) sobre mathlib_full con el índice IVF_SQ da recall@10 denso 0.42 / BM25 0.25 / híbrido 0.38 / híbrido+rerank 0.45 (nDCG@10 0.302 / 0.196 / 0.277 / 0.339) contra 0.41 / 0.25 / 0.38 / 0.45 de la búsqueda exacta: sin costo medible de precisión. La demo sobre el índice completo responde en 0.4-0.5 s por consulta una vez cargado el embedder	—	Confirma #60 con el benchmark real, no sólo con consultas sintéticas	data/eval/results/fase1_full_ann_mathlibqr_100q.json, docs/eval_report.md §1d

Fase 1 del plan de corrección — endurecimiento del verificador (2026-09-23)

#	Decisión	Alternativa descartada	Motivo	Evidencia
69	Auditoría técnica (docs/AUDIT_2026-09-23.md) encontró SEC-1 y VER-1 (HIGH, confirmados empíricamente): las tácticas del LLM se empalmaban sin validar y el kernel acepta decide +native como "verificado" (depende de Lean.ofReduceBool, no del kernel — mismo fallo que 15/225 soluciones publicadas de Kimina-Prover). Corregido en lean/verify.py (niveles de la guía oficial de Lean): find_forbidden_tactic (nivel 1, antes de tocar Lean) rechaza #comando en cualquier posición (no sólo al inicio de línea: open X in #eval ... sería un bypass de un chequeo anclado a línea), metaprogramación, declaraciones nuevas, cambios de entorno y sorry/native_decide/decide +native/ofReduceBool/trustCompiler; _axiom_check (nivel 2, tras un veredicto sin errores) exige que #print axioms <nombre> sea subconjunto de propext/Classical.choice/Quot.sound. De paso (BUG-2) theorem_block/build_file pasan a ser la única fuente para el REPL y para el lean_code reportado — antes el reporte no incluía los open del header del problema	Sandbox de sistema operativo primero	El sandbox (Fase 10 del plan) es más caro y no cierra VER-1 (una prueba con decide +native corre igual dentro de un sandbox); la validación de tácticas + auditoría de axiomas cierra ambos hallazgos con ~150 líneas y sin infraestructura nueva	tests/test_verify.py; tests/test_verify_slow.py (marcador slow, Lean real, corrido una vez el 2026-09-23: 4/4 passed en 67 s)
70	Exploit confirmado y luego cerrado: simp\n#eval IO.println "COMANDO INYECTADO" empalmado como una prueba normal ejecutaba el #eval (verificado antes de este arreglo, con Lean real, en el scratchpad de la sesión de auditoría). Tras el arreglo, find_forbidden_tactic lo rechaza antes de llegar al REPL (tests/test_verify_slow.py::test_injected_command_never_reaches_the_repl)	—	Riesgo real, no teórico: acceso al sistema de archivos con permisos del proceso (incluido .env con las claves de API)	tests/test_verify_slow.py
71	decide +native sí lo acepta el kernel (confirmado con Lean real): #print axioms muestra [Lean.ofReduceBool, Lean.trustCompiler]. _axiom_check lo rechaza aunque el kernel haya aceptado la táctica (tests/test_verify_slow.py::test_native_decide_is_rejected_by_axiom_audit_if_the_denylist_were_bypassed, que pasa por alto find_forbidden_tactic a propósito para probar la segunda capa de forma aislada)	Confiar sólo en la lista de rechazo de tácticas	Defensa en profundidad: un nombre de axioma nuevo que la lista no conozca (o una forma de invocarlo que la lista no cubra) lo sigue atrapando la auditoría de axiomas, que no depende de reconocer sintaxis	tests/test_verify_slow.py
72	Re-verificación offline de eval-v1 con el verificador nuevo (scripts/reverify_eval_v1.py, 0 llamadas LLM: sólo REPL, ~70 s): de las 27 filas done, reconstruidas con el header del problema (que el lean_code original no incluía, BUG-2) — 27/27 siguen ok=true, 0 regresiones, todos los axiomas dentro de {propext, Classical.choice, Quot.sound}. Sobre las 203 filas con lean_code extraíble de las 300 totales, 20 quedan marcadas por el denylist nuevo — las 20 contienen sorry o native_decide literales (el LLM se rindió o probó un atajo) y ya estaban en filas status=fail; el regex viejo (_FORBIDDEN) ya las rechazaba por los mismos tokens, así que no son casos nuevos	Repetir eval-v1 con el código nuevo	El verificador más estricto no cambia ningún resultado ya reportado (mismos 9/9/4/5/pass@1); no hace falta gastar de nuevo la key ni recalcular docs/eval_report.md/docs/final_report.md	data/eval/runs/eval-v1/reverify.json (no versionado en git, igual que el resto de data/eval/runs/)
73	Problem.imports rechazado explícitamente (Orchestrator.solve, run_baseline) en vez de ignorado en silencio (auditoría BUG-4): ningún conjunto de problemas de este proyecto lo usa hoy (data/eval/problems/*.jsonl verificado); si algún día un problema lo trae, falla con un motivo claro en vez de verificarse contra un archivo al que le faltan imports que el Autoformalizador pudo haber asumido	Seguir concatenándolo en silencio (comportamiento anterior)	Fallar alto y explícito es más barato que depurar un "unknown identifier" que en realidad era un import faltante	tests/test_orchestrator.py::test_problem_imports_are_rejected_explicitly_instead_of_ignored, ::test_run_baseline_rejects_problem_imports_too
74	Test de arranque índice ↔ Lean (PLAN_RAG.md §12, pendiente desde la Fase 1 original): run_suite muestrea 20 decl_name al azar (semilla 13) de la tabla que sirve mathlib y los comprueba con #check contra el Lean real del verificador (LeanChecker.check_identifiers_exist); sólo avisa en el log, no aborta la corrida	Abortar si algún nombre no existe	Un nombre fantasma es una señal de desalineación índice/Mathlib, no necesariamente un error fatal; el #check es aproximado (cuenta errores totales, no mapea 1 a 1)	tests/test_orchestrator.py::test_check_index_consistency_reports_without_running_lean

Fase 2 del plan de corrección — licencias y datos, antes del primer commit (2026-09-24)

#	Decisión	Alternativa descartada	Motivo	Evidencia
75	.gitignore ampliado (SEC-2): problemas resueltos olimpiadas.pdf, blobs/ (caché de MinerU con el texto completo del PDF), data/eval/runs/ (354 citas informales con hasta 300 caracteres del PDF en snippet), lean_project/scratch/, lean_project.lock, .claude/*.graphify-bak. Nada se borró del disco — sólo se excluye de git. Propuesta_Proyecto_Final_IA_UPTC.pdf (del usuario, sin problema de licencia) queda pendiente de que el usuario confirme si quiere versionarla	Borrar los archivos	Borrar es una acción destructiva; ignorarlos en git ya cierra el riesgo de licencia y es reversible	.gitignore
76	Fuga nueva encontrada al verificar (no estaba en la auditoría del 23-09): docs/qa_ingest_edd3436ca148.md embebía 16 fragmentos del PDF (fórmulas del gate de QA, transcripciones de huecos, descripciones VLM de figuras — estas últimas también las trata como no publicables publish_hf.py, que ya excluye las tablas informal/figures completas cuando redistributable=false). scripts/qa_ingest_report.py ahora redacta todo contenido derivado del texto del documento cuando redistributable=false (conteos y páginas, sin texto literal); con el documento actual, el reporte pasa de 16 coincidencias a 0	Excluir el archivo entero de git	El reporte de QA es un entregable citado en final_report.md Apéndice D; redactar mantiene el valor documental (gates, conteos, páginas) sin el texto protegido	scripts/check_no_leaked_content.py, corrida antes/después sobre docs/qa_ingest_edd3436ca148.md
77	Comprobación por contenido reutilizable (scripts/check_no_leaked_content.py: huellas de 60 caracteres del content_md del corpus informal, buscadas en los archivos que git add . incluiría) — 0 coincidencias sobre el repo completo tras las decisiones #75/#76 (antes: 1 archivo, 16 coincidencias). La misma función la usa scripts/publish_hf.py: cuando el documento informal no es redistribuible, data/eval/runs/<run_id>/ se sube desde una copia temporal saneada (Citation.snippet vaciado sólo en citas corpus=informal; verificado que las trazas no llevan texto de fuente, sólo ids/scores/consultas — 0 coincidencias en 1443 archivos de trazas de eval-v1) y el publish (incluido --dry-run) aborta si la comprobación encuentra algo	Confiar sólo en redistributable para decidir qué carpetas subir (como ya hacía el script con informal.lance/figures.lance)	results.jsonl no estaba cubierto por ese gate: se sube siempre, sin condicionarlo a redistributable — el vector de fuga real que encontró la auditoría (SEC-2)	tests/test_check_no_leaked_content.py; python scripts/publish_hf.py --repo test/x --dry-run → "content_check": "OK"

Fase 3 del plan de corrección — dependencias y documentación de estado (2026-09-24)

#	Decisión	Alternativa descartada	Motivo	Evidencia
78	Dependencias core reducidas (auditoría DEP-1): httpx y tenacity pasan a declararse (se usaban directo en llm.py/embed.py sin estar en pyproject.toml, sólo llegaban como transitivas de langchain-core/huggingface-hub). Nuevo extra demo = ["gradio"] (antes sólo llegaba vía mineru/ingest; con uv sync a secas python demo/app.py fallaba). ranx pasa a dev (sólo lo usa tests/test_metrics.py). pandas y accelerate se quitan de las dependencias core: 0 referencias directas en src/scripts/demo (grep verificado); confirmado sin ellos instalados que tests/test_retriever_integration.py carga el embedder Y el reranker reales (rerank=True, cross-encoder) en verde — accelerate sólo lo exige transformers para cargar GGUF (transformers/modeling_utils.py: "accelerate is required when loading a GGUF file"), camino que este proyecto no usa vía transformers (el GGUF se sirve por llama-server externo). Siguen instalados como transitivas en los entornos que ya los necesitan (pandas vía ranx/gradio, accelerate no resultó necesario ni siquiera con el extra ingest en esta resolución de mineru)	Declarar pandas/accelerate "por si acaso"	Menos superficie de instalación; el entorno con --extra dev --extra ingest --extra demo sigue siendo idéntico en la práctica (uv sync los trae igual por las extras que sí los necesitan)	pyproject.toml; suite completa (128 tests, incluidos los 2 de integración real y los 4 con Lean real) en verde tras uv lock && uv sync --extra dev --extra ingest --extra demo
79	Desvíos de PLAN_RAG.md no registrados hasta ahora (auditoría §3.A), documentados aquí en vez de en el código: (a) la recuperación informal (mode=exemplar) sólo ocurre en PLAN (ejemplares para el Planificador); RETRIEVE no vuelve a consultar el corpus informal por subobjetivo como sugiere el plan §6.2 Fase 4 tarea 3 — el diseño implementado es "ejemplares una vez al principio", no "ejemplares por subobjetivo"; (b) math_area no actúa como boost en la búsqueda (plan Fase 4 tarea 4): el campo se guarda y se puede filtrar con RetrievalFilters.math_area, pero nada del orquestador lo usa para reordenar resultados; (c) el índice FTS usa una columna derivada _fts_text (concatenación de los campos buscables) en vez de una columna name_tokens tokenizada por ./_ como sugería el plan §6.1 tarea 5 — LanceDB ≥0.25 sólo indexa FTS de un campo por índice, así que se concatena en vez de mantener dos índices; (d) los embeddings se guardan en float32 en el JSONL intermedio (data/corpus/*_embedded.jsonl), no float16 como dice el esquema §7.2 — sólo la columna embedding de la tabla LanceDB final importa para el tamaño del índice, y ésa sí es la que se sirve; (e) no existe una tabla documents real ni el modelo Document se usa para nada — build_document_record en ingest_informal.py arma un dict con la misma forma pero sin validar contra el modelo Pydantic (relacionado con ING-1, pendiente en Fase 5 del plan de corrección)	Cambiar el código para que coincida con el plan	Cada desvío tiene una razón técnica real (limitaciones de LanceDB, foco del proyecto en Fase 4/5) y ninguno afecta RNF-3 (0 llamadas del retriever) ni la validez de eval_v1; registrar es más barato que revertir sin evidencia de que haga falta	src/ragsolver/orchestrator/graph.py (retrieve/plan), src/ragsolver/rag/index.py (_FTS_COLUMN), src/ragsolver/rag/embed_corpus.py, src/ragsolver/rag/ingest_informal.py::build_document_record

Fase 4 del plan de corrección — citas, trazas y contabilidad (2026-09-24)

#	Decisión	Alternativa descartada	Motivo	Evidencia
80	IDs de cita estables por chunk (BUG-1): _assign_citation_ids (nuevo, orchestrator/graph.py) mantiene state["citation_ids"]: {chunk_id: citation_id} durante todo el problema; plan()/retrieve() reutilizan el id existente de un chunk que reaparece (tras un replan o una re-recuperación) y sólo asignan el siguiente número libre del prefijo a los chunks nuevos, en vez de renumerar M1..Mn/I1..In desde cero en cada llamada. eval_v1 no se recalcula (las trazas del retriever de esa corrida no se pueden atribuir a un par (config, problema), TRZ-1 no estaba corregido todavía cuando corrió)	Recalcular used_in_sketch de eval_v1 desde las trazas existentes	Sin TRZ-1 corregido en esa corrida, no hay forma de reconstruir con certeza qué búsqueda perteneció a qué intento; se documenta como limitación en vez de fabricar un recálculo dudoso	tests/test_orchestrator.py::test_citation_ids_stay_stable_and_unique_when_a_chunk_reappears
81	Trazas del retriever agrupadas por corrida (TRZ-1): RetrievalContext gana run_id; el orquestador pasa state["run_id"] (ya el pid completo <run>:<config>:<problema>) en cada RetrievalRequest.context; Retriever.search() usa ese run_id como nombre del archivo de traza en vez de fabricar uno con un uuid aleatorio por búsqueda. Sin run_id (CLI, demo, evaluate.py) se mantiene el comportamiento anterior (un archivo por búsqueda) — no tienen un "run" real que agrupar. Comprobado que los nombres de archivo con : (el formato del pid) ya funcionan en este filesystem: los 300 archivos de eventos de agentes de eval_v1 ya los usaban sin problema, así que no hizo falta el cambio : -> __ que preveía el plan	Cambiar : por __ en los nombres de archivo	Innecesario: verificado que /mnt/c (este WSL2) ya acepta : en nombres de archivo — los propios eventos de agentes de eval_v1 lo prueban	tests/test_retriever.py::test_run_id_in_context_groups_searches_into_one_trace_file
82	Pin de la tabla mathlib servida (MET-1): VersionsPin gana mathlib_table; Retriever.search() y Agents._call() (nuevo Agents._versions_pin(), evita duplicar la construcción) lo llenan desde la misma fuente de verdad (RAGSOLVER_MATHLIB_TABLE, extraída a retrieve.mathlib_table_name())	Dejarlo sólo en el log de run_suite	Así cada evento de traza (no sólo el arranque de la corrida) dice contra qué tabla se buscó — relevante si RAGSOLVER_MATHLIB_TABLE cambia a mitad de sesión de trabajo	tests/test_retriever.py::test_trace_event_pins_the_mathlib_table_being_served
83	Política de reintentos del cliente LLM (LLM-1): httpx.ReadTimeout deja de reintentarse (el proveedor puede haber generado — y cobrado — la respuesta antes del corte; reintentar la duplicaría), tope bajado de 20 a 4 intentos, y cada LLMResponse lleva attempts (se registra en la traza). timeout_s por defecto baja de 600/900 a 300 s (configs/versions.yaml: llm.timeout_s); 4000 tokens de salida al proveedor más lento medido son ~210 s (#62), 300 s deja margen. El bucle de reintentos pasa de @retry (decorador estático, sin contar intentos de forma segura entre hilos) a tenacity.Retrying construido dentro de la llamada (estado local, sin carrera con --workers)	Seguir con el decorador @retry y stop_after_attempt(20)	20 intentos por llamada era el origen del sobrecosto de eval_v1 (#59, ya mitigado ahí de otra forma); acotar a 4 y no reintentar timeouts de lectura cierra la misma clase de riesgo de forma más general	tests/test_llm.py::test_retryable_excludes_read_timeout_but_allows_connect_timeout_and_5xx, ::test_generate_with_counts_attempts_and_retries_on_503, ::test_generate_with_does_not_retry_a_read_timeout
84	Contabilidad sin pérdidas ante cualquier excepción (ACC-1): Orchestrator._guard pasa a capturar cualquier Exception (no sólo InvalidLLMOutput), devolviendo status: "error" sin salir del grafo — el estado que LangGraph ya fusionó (llamadas, tokens, evidencia, historial de los nodos previos) se conserva, a diferencia del except Exception que tenía solve() antes, que reemplazaba todo el estado final por {**init, fail_reason} (perdía todo). Las aristas condicionales de plan/retrieve/generate/formalize/verify se actualizan para tratar status="error" igual que "fail" (cortan a END) en vez de intentar seguir con estado a medio llenar. El evento invalid_json de Agents._call ahora lleva llm_calls/tokens/cost_usd reales (antes self.trace() los ponía siempre en 0). Las filas fail/error de líneas base llevan models=[<modelo>] cuando la excepción es InvalidLLMOutput (antes quedaban con models=[])	Seguir descartando el estado en un solo except en solve()	Capturar a nivel de nodo es más barato que reconstruir el estado perdido, y usa la fusión de estado que LangGraph ya hace gratis	tests/test_orchestrator.py::test_generic_exception_mid_run_becomes_status_error_and_keeps_accumulated_state, ::test_baseline_invalid_json_row_records_which_model_produced_it
85	Self-consistency: cost_usd y attempts de las n muestras se suman (BUG-5): type(resp)(text, model, tokens_in, tokens_out, calls=n) sólo pasaba esos 4 posicionales + calls, dejando cost_usd/attempts de la respuesta agregada en sus valores por defecto (0.0 / 1) aunque las muestras hubiesen costado más o reintentado. Apagado por defecto (generator_samples: 1); no afecta a eval_v1	—	Encontrado al revisar el mismo constructor para agregar el nuevo campo attempts	tests/test_orchestrator.py::test_self_consistency_sums_cost_and_attempts_across_samples
86	Lock en la caché de embeddings de consulta (BUG-6): _QUERY_CACHE se leía/escribía desde varios hilos (--workers N) sin lock; la evicción FIFO (_QUERY_CACHE.pop(next(iter(_QUERY_CACHE)))) podía correr a la vez que otro hilo insertaba, con riesgo de RuntimeError: dictionary changed size during iteration. Nuevo _QUERY_CACHE_LOCK (separado de _TORCH_LOCK, que sólo protege la codificación real: así el backend llama, que no usa torch, no se serializa de más)	Un solo lock compartido con _TORCH_LOCK	Serializaría también las lecturas de caché del backend llama, que no tocan torch	tests/test_embed.py::test_embed_queries_is_safe_under_concurrent_access (400 llamadas concurrentes, 8 hilos, caché de sólo 8 entradas para forzar evicciones)
87	Problem.imports no soportado en run_baseline tampoco (BUG-4, continuación de #73 en Fase 1): mismo guard que Orchestrator.solve	—	Consistencia: el camino de líneas base no pasaba por el guard de la Fase 1	tests/test_orchestrator.py::test_run_baseline_rejects_problem_imports_too
88	Suite completa verificada tras la Fase 4 (138 tests: 132 rápidos + 2 de integración real contra el índice + 4 con Lean real, incluida la re-verificación de axiomas de la Fase 1) — ningún cambio de esta fase afecta los resultados ya reportados de eval_v1 (no se re-ejecutó nada con LLM real; el smoke opcional de 5 problemas triviales, D6 del plan, queda pendiente de aprobación de gasto)	Correr el smoke sin preguntar (costo ≈ US$0.001)	El plan exige aprobación explícita para cualquier llamada de pago, sin excepción de monto	uv run pytest -q (138 passed)

Plan de mejora del RAG — recuperar para el goal de Lean (2026-10-14, docs/PLAN_MEJORA_RAG.md)

#	Decisión	Alternativa descartada	Motivo	Evidencia
89	El input del retrieval de Mathlib es el goal de Lean, no el enunciado ni el subobjetivo en lenguaje natural. El Autoformalizador escribe un esqueleto have … := by sorry; LeanChecker.goals lo elabora en modo sonda (nunca produce ok) y devuelve un goal + proof_state por sorry (lean-interact: CommandResponse.sorries). El NL queda sólo para los ejemplares del corpus informal (NL↔NL, recall@5 1.0)	Reescribir mejor las consultas NL; consultar el índice con el enunciado formal	Recall@8 de premisas gold en el índice completo: NL 0.012, formal 0.000; las premisas de competición son herramientas genéricas cuyo enunciado no se parece al problema (§2.2-§3 del plan)	data/eval/results/probe_close/names.json; PLAN_MEJORA_RAG.md §2.2
90	Canal A — prior de competición: frecuencia de cada lema en 29 750 pruebas de Goedel-LM/Lean-workbook-proofs (MIT, revisión b731852a), validado contra el entorno de Lean con LeanChecker.signatures (#check, uno por nombre) y no contra el JSONL de LeanSearch — entran los lemas de núcleo (Nat.mul_mod, Nat.mod_eq_of_lt, eq_comm). Se sirve filtrado por los símbolos del goal (rag/premises.py::prior_channel: un lema anclado a √/%/ℕ sólo si el goal los tiene). 778 lemas	Tabla LanceDB premise_prior (el plan la proponía)	Un JSONL de 778 filas en memoria basta; no hace falta re-embeber nada	data/corpus/premise_prior.jsonl + .meta.json; scripts/build_premise_prior.py
91	signatures reintenta sin los open: con open … Nat, #check @sq_nonneg es ambiguo (sq_nonneg vs Nat.sq_nonneg) y falla, aunque la prueba lo desambigua por tipo. Sin el reintento el prior perdía su lema más frecuente (16 719 usos)	—	Bug encontrado al inspeccionar la primera versión del prior (766 lemas sin sq_nonneg; 778 con el arreglo)	tests/test_verify_slow.py::test_signatures_resolves_core_lemmas_and_ambiguous_root_names
92	Canal B (selección nativa de Lean) se consume dentro de CLOSE (grind +suggestions), no como lista de nombres para la fusión	Fusionar la salida de la táctica suggestions con A y C	Para 0 ≤ (a - b) ^ 2 la táctica suggestions devuelve not_fermat_42, BitVec.pow_add… con score plano 0.88; en cambio grind +suggestions cerró 9/60 problemas de eval_v1 frente a 7/60 de grind (§2.3)	data/eval/results/dev_probe/explore.log
93	Batería CLOSE configurable (configs/agents.yaml: close.tactics, la primera que cierra gana): grind +lax [premisas] → nlinarith [hints] → grind +suggestions → try?. Cada táctica pasa por find_forbidden_tactic y, después, el sistema la envuelve en set_option maxHeartbeats 200000 in (sólo tácticas de una línea de la batería; el LLM sigue sin poder usar set_option). try? se reemplaza por su script concreto ("Try this: [apply] …"): el kernel nunca acepta una táctica con ?	Timeout de reloj solo	Un timeout de ProofStep reinicia el REPL (~5 min de import Mathlib) e invalida los proof_state de los demás hilos	orchestrator/graph.py::close_goal, concrete_block; LeanChecker.step
94	Registro de goals probados (proved) y FILL sólo sobre los abiertos: un reintento o un replan no vuelve a demostrar un goal ya cerrado (se reutiliza su bloque si sigue cerrando en el nuevo contexto); el Autoformalizador recibe los have ya probados; FILL (1 llamada) recibe cada goal abierto con su contexto exacto, sus premisas con firma y el último error de la automatización	Regenerar la prueba entera en cada intento (eval-v1)	En eval-v1, 55 de 99 intentos fallidos con ≥ 2 have tenían al menos uno completo antes del primer error y se descartó igual (§2.5)	tests/test_goal_mode.py::test_fill_only_sees_open_goals_and_ledger_reuses_proved_ones_on_retry
95	Replan con memoria (DES-1): el prompt del Planificador recibe {feedback} = razón del Crítico + estrategia anterior + goals ya probados; prompt_version: "2". Sustituye a PLAN_CORRECCIONES.md 7.1	max_replans: 0	65 replans con 2 éxitos en eval-v1 (similitud 0.13 con el plan anterior: remuestreo a ciegas)	tests/test_goal_mode.py::test_replan_carries_critic_feedback_and_proved_claims
96	Ablaciones redefinidas (R3): no_rag = misma batería CLOSE sin premisas recuperadas, hints ni grind +suggestions (sí grind, nlinarith, try?); rag_nl = el flujo de eval-v1 (goal_mode: false); baseline_auto = 0 LLM, sólo la batería sin premisas sobre el goal raíz (run.py::run_auto)	no_rag sin automatización	Si no_rag no tuviera la batería, la comparación mezclaría el aporte del RAG con el de la automatización de Lean, que sola ya cierra 12/60	configs/agents.yaml: configs
97	Filtro de ingesta de Mathlib por regex \.eq_(\d+|def)$ en vez de la subcadena .eq_, que también borraba lemas reales como Nat.Prime.eq_one_or_self_of_dvd. No cambia el índice actual: la fuente (LeanSearch v2) ya no trae ningún nombre con .eq_	—	§2.4 del plan	tests/test_ingest_mathlib.py::test_equation_lemmas_are_excluded_but_real_eq_lemmas_are_kept
98	Canal C (índice denso con el goal como consulta) apagado por defecto (close.dense_channel: false; plan B de la Fase 3). Por goal (1 295 goals del gold nuevo, muestra de 600 para C): recall@16 A filtrado 0.327, A estático 0.261, C 0.028, fusión A+C 0.097 — la RRF intercala los hits densos (irrelevantes) con los del prior y desplaza a los buenos. Por problema, con el gold contra Lean: consulta NL de eval-v1 0.006, formal 0.004, prior 0.229. La Fase 5 (selector LeanHammer) no se dispara: A ≥ 0.30 por goal. La tarea 4b (núcleo en el índice denso) queda sin objeto mientras C esté apagado	Mantener la fusión A+C del plan	Medido; la fusión resta 23 puntos	data/eval/results/premises_goals.json; scripts/eval_premises_goals.py
99	Gold de premisas por goal (data/eval/premises_gold_goals.jsonl, 1 295 goals de 230 problemas, 218 lemas distintos; por problema: premises_gold_lean.jsonl): por cada táctica sin bloque by anidado de las pruebas verificadas de DeepSeek-Prover-V2, el goal antes de la táctica y las constantes que la táctica nombra y que el término usa (used_constants del REPL ∩ identificadores del texto, con resolución de open). Las pruebas que no compilan del todo en el Mathlib fijado (183/438) aportan las tácticas que no contienen la posición de un error. premises_gold.jsonl (filtrado contra el JSONL de LeanSearch, sin núcleo) se conserva para reproducir las cifras publicadas	used_constants a secas; descartar las pruebas con errores; filtrar tácticas con salto de línea	used_constants a secas mete plomería de norm_num/simp/decide (congrFun' 2 463 veces, Nat.decLt, of_decide_eq_false); descartar las pruebas con error perdía el 42 %; DeepSeek parte nlinarith [sq_nonneg …] en varias líneas	scripts/build_premise_gold_goals.py (+ .raw.jsonl para re-filtrar sin re-elaborar)
100	Batería CLOSE medida sobre el goal raíz de eval_v1 (scripts/probe_close.py, 0 LLM): sin premisas 11/60, con premisas (prior + hints + grind +suggestions) 12/60; grind cierra 6 → 8 con premisas; algebra_sqineq_2unitcircatblt1 sólo con RAG (nlinarith [sq_nonneg (a - b), …]). Dos ajustes de infraestructura salieron de esta medición: close.timeout_s 60 → 150 (try? llega a 76 s; cada sub-táctica parece tener su propio presupuesto de heartbeats) y generación del REPL en cada proof_state (LeanChecker._gen): tras un reinicio, step rechaza el estado viejo sin enviarlo — antes el número podía apuntar a otro goal del REPL nuevo, y la primera corrida perdió 12 filas por reinicios en cascada (se re-midieron sólo esas; la primera corrida queda en battery.first_run.jsonl)	Timeout de 60 s	Medido	data/eval/results/probe_close/battery.jsonl; tests/test_verify_slow.py::test_stale_proof_state_is_rejected_after_a_restart
101	used_in_proof con las constantes del término aceptado (Verdict.used_constants, REPL all_tactics=True en LeanChecker.check), no con el texto de la prueba: grind +lax [16 lemas] nombra 16 y puede no usar ninguno. En el segundo smoke el criterio textual daba 16/19 en tres problemas; re-verificado con el REPL: 0 premisas recuperadas en los términos de las 8 pruebas — grind cerró esos pasos sin ellas. Sin REPL (backend lake) queda el criterio textual	Criterio textual (identifiers_used)	Una cita "usada" debe ser una que el kernel usó	data/eval/results/smoke_used_constants.json; tests/test_goal_mode.py::test_used_in_proof_counts_only_constants_the_kernel_term_uses, tests/test_verify_slow.py::test_check_reports_the_constants_the_accepted_term_uses
102	El sistema parte la prueba del modelo en goals (lean/verify.py::skeletonize, prompt_version: "3"): cada have … := by <bloque> de nivel superior pasa a sorry y su bloque es el primer candidato de ese goal; lo que sigue al último have es el candidato del cierre. CLOSE prueba primero el bloque del modelo, después la batería; FILL ve el intento rechazado. Además, strip_code_fences baja al nivel de la primera línea el resto del bloque cuando el modelo entrega la primera sin sangría y la primera no abre un bloque	Exigir el esqueleto con sorry en el prompt	Primer smoke (8 problemas, prompt 2): el modelo escribió pruebas completas sin sorry en todos los casos — CLOSE nunca recibía goals — y en triv_dvd_trans la sangría rota (unexpected identifier) tumbó los 3 intentos. Segundo smoke (prompt 3): 8/8 (antes 5/8), 35 llamadas, US$0.0047	data/eval/runs/smoke-goal-mode, smoke-goal-mode-v3; tests/test_goal_mode.py::test_full_proof_without_sorry_is_split_into_goals_and_only_the_bad_step_is_repaired, test_skeletonize_shapes; tests/test_orchestrator.py::test_strip_code_fences_and_repeated_statement
103	Hallazgo operativo (OpenRouter, 2026-10-14): con provider_routing.max_price {prompt: 0.10, completion: 0.20} hoy sólo califica DeepInfra ($0.06/$0.18; StreamLake, el de eval-v1, subió a $0.132/$0.396), y DeepInfra responde 429 engine_overloaded de forma intermitente: el primer smoke perdió 7/8 pares por 429 con 4 hilos. Con 1-2 hilos y los reintentos existentes (4, backoff exponencial) completó. Antes de la evaluación grande hay que decidir: esperar, correr con pocos hilos, o subir el tope (con completion ≤ 0.30 califican ~8 proveedores)	—	Medido (GET /models/…/endpoints, respuesta 429 con provider_error_code: engine_overloaded)	data/eval/results/smoke_goal_mode.log
104	Un 429 se reintenta hasta 10 veces (espera exponencial con tope de 90 s); 5xx y errores de transporte siguen en 4 (LLM-1) y un timeout de lectura sigue sin reintentarse. Un 429 es una solicitud rechazada que no se cobra; con 4 intentos (≈ 28 s) los 429 de DeepInfra saturado dejaban pares en error tras haber gastado 2-3 llamadas	Volver a subir todos los reintentos	Lo que se cobra (timeouts de lectura, JSON inválido) sigue sin reintentos ocultos	tests/test_llm.py::test_429_gets_more_retries_than_billable_errors
105	eval-v2 en 4 rondas de 15 problemas con guardia de costo (a pedido del usuario): rondas intercaladas (eval_v1_round{k}.jsonl = problemas k, k+4, …; 6 álgebra / 6 teoría de números / 3 combinatoria cada una), configs full, no_rag, rag_nl, baseline_auto, --workers 2, tope de precio sin cambios (decisión del usuario). Tras cada ronda round_check.py mide el gasto real de la key y corta la cadena ante cualquier alerta (> 20 llamadas en un par, > US$0.006 por par, > 10 % de errores, baseline_auto con LLM, proyección > saldo). rag_nl corre sobre mathlib_full (eval-v1 usó la muestra sembrada con el gold, MET-1)	Una sola corrida de 60	Detectar un bug de costo después de 15 problemas, no de 60	data/eval/results/eval_v2_chain.sh, round_check.py, eval_v2_round{k}_check.json
106	rag_nl aislada de eval-v2 (decisión del usuario): la evaluación corre full, no_rag y baseline_auto. Prioridad: probar el sistema nuevo y medir el aporte del RAG nuevo (full vs no_rag) y de los agentes (full vs baseline_auto) dentro del saldo de la key; rag_nl (el flujo de eval-v1) era la configuración más cara (~35 % del gasto). Al detenerla no había ningún par de rag_nl terminado. Queda definida en configs/agents.yaml y se puede correr después sobre el mismo run_id si sobra saldo	Correr las cuatro configuraciones	Costo y tiempo; la comparación con el sistema viejo queda contra eval-v1 (confundida por proveedor, índice y prompts — se reporta así)	data/eval/results/eval_v2_chain_b.sh
107	Tope de precio de OpenRouter subido a {prompt: 0.13, completion: 0.30} (8 proveedores) y 4 hilos para eval-v2, a pedido del usuario (tiempo estimado 13-16 h → 2-4 h). Costo real medido del flujo nuevo antes del cambio: US$0.0016 por par (10 300 tokens de entrada / 5 600 de salida; eval-v1 gastaba 25 500 / 9 700). Peor caso para los 113 pares restantes ≈ US$0.34 < saldo US$0.385; sort: price usa primero DeepInfra y sólo pasa a los demás cuando rechaza. full y no_rag corren con la misma mezcla de proveedores (algunos sirven el modelo con más cuantización): la comparación entre ellas no se sesga, pero se anota como limitación	Mantener {0.10, 0.20} (sólo DeepInfra, saturado: 46 rechazos 429 y 16 min de espera en 7 pares)	Tiempo; el costo esperado casi no cambia y el guardia entre rondas sigue activo	configs/versions.yaml: llm.provider_routing; data/eval/results/eval_v2_chain_c.sh
108	Guardia de costo detuvo eval-v2 tras la ronda 1 (proyección US$0.343 > saldo US$0.289). Ronda 1 (15 problemas): full 6, no_rag 7, baseline_auto 5 (eval-v1 en los mismos: full 3, no_rag 4). baseline_auto completada en los 60 a US$0 (key deshabilitada por variable de entorno): 11/60, más que eval-v1 full (9/60). El kernel usó 1 premisa recuperada en 1 problema. Costo real por par US$0.0036 (full) / US$0.0032 (no_rag), igual que eval-v1 en tokens. No se relanza nada pagado sin decisión del usuario (opciones A-D en docs/eval_report_v2.md §6)	Continuar sin preguntar	El guardia existe para esto; la proyección supera el saldo	docs/eval_report_v2.md; data/eval/results/eval_v2_round1_check.json, eval_v2_stats.json
109	Opción B del usuario: eval-v2 continúa sólo con las rondas 2 y 3 (full, no_rag; baseline_auto ya completa), con el saldo actual (US$0.2887) y la misma configuración (tope {0.13, 0.30}, 4 hilos). Resultado final: 45 problemas pareados. El guardia proyecta ahora hasta la ronda 3 (round_check.py <k> 3)	A (subir el límite de la key), C, D	Decisión del usuario	data/eval/results/eval_v2_chain_d.sh
110	Salidas ilegibles del Crítico y de FILL ya no matan el problema: Crítico inválido → reintento con los errores de Lean como feedback; FILL inválido → sin propuestas (goals abiertos); las llamadas se contabilizan igual	Dejar llm_output_invalid como fallo	12 de 43 fallos de eval-v2 (rondas 1-2) eran llm_output_invalid (Crítico 6, FILL 4)	tests/test_goal_mode.py::test_unreadable_critic_output_retries_instead_of_failing_the_problem
111	Detener la ronda 3 de eval-v2 y rediseñar (consejo aceptado por el usuario): 11 de 15 pares full hechos (2 resueltos), no_rag sin empezar; completarla (~US$0.06) no cambiaba la conclusión (dificultad 2-3: 0 resueltos en ambas)	Completar las rondas	El cuello de botella medido es el demostrador, no el RAG; el saldo sirve más para probar el rediseño	docs/eval_report_v2.md
112	Demostrador especializado local: Goedel-Prover-V2-8B (Apache-2.0; 84.6 % pass@32 miniF2F según su paper), GGUF mradermacher/Goedel-Prover-V2-8B-GGUF revisión 43fab68e, Q6_K, llama-server Vulkan en la RX 9060 XT (8 slots × 12 288, KV q8_0, flash attention), escuchando sólo en 172.31.112.1:8082. Etapa 0 sobre el teorema completo (k_root 8 en lotes de 4 con salida temprana, una ronda de autocorrección) y lemas autónomos para los goals abiertos en CLOSE (k_goal 2, max_goals 2). Del modelo se toman SÓLO las tácticas del teorema pedido, empalmadas en el enunciado del problema	DeepSeek-Prover-V2-7B / Kimina-Prover-8B; servicio remoto (no hay demostradores en OpenRouter, verificado)	Mejor número publicado entre los 7-8B; costo de API 0; Q6_K = Q8 en calidad práctica y más rápido (45 vs 36 tok/s; la GPU satura en ~70 tok/s agregados en ambos)	docs/PLAN_REDISENO_PROVER.md; data/eval/results/dev_probe/bench_prover.py; tests/test_prover.py
113	Rol del RAG en el rediseño: corregir nombres — el demostrador se entrenó con Lean 4.9/Mathlib de entonces; ante unknown identifier/constant, el RAG (índice, modo error) propone declaraciones parecidas validadas con #check en el Mathlib fijado, que van a la autocorrección y se citan (M*, used_in_proof por el término)	Seguir pasando premisas genéricas al prompt	eval-v2: el kernel no usaba las premisas genéricas; el cambio de versión de Mathlib es una necesidad real y medible del demostrador	tests/test_prover.py::test_correction_round_gets_rag_name_suggestions_and_cites_them
114	Caché en disco de las muestras del demostrador (data/eval/prover_cache.jsonl, clave = mensajes + semilla + parámetros): baseline_prover y la etapa 0 de full comparten las mismas muestras (pareadas, generadas una vez); SolutionReport registra solved_by y prover_samples	Semillas distintas por configuración	El tiempo de GPU es el recurso escaso (~70 tok/s)	tests/test_prover.py::test_disk_cache_reuses_identical_samples
115	Resultado del rediseño (eval-v3, 30 problemas pareados con eval-v2): full v3 21/30 (dificultad 1/2/3: 13/16 · 6/10 · 2/4) frente a v2 full 8/30 (0/14 en dificultad 2-3); McNemar 13 a 0, p = 0.0002. Los 21 los resolvió la etapa 0 (demostrador local, 0 API); los agentes por API (US$0.06) y el RAG (2 correcciones con 8 nombres sugeridos, 0 usados por el kernel) no añadieron ningún problema: full = baseline_prover. Pruebas revisadas: enunciado intacto, axiomas estándar. Servidor de la GPU apagado al terminar. Limitación principal: posible contaminación (miniF2F es el benchmark público del demostrador)	—	Medido	docs/eval_report_v3.md; data/eval/results/eval_v3_analysis.json

eval-v4 — respaldo por API apagado, DRAFT, más muestras y problemas fuera de miniF2F (2026-10-18)

#	Decisión	Alternativa descartada	Motivo	Evidencia
116	Respaldo por API apagado por defecto (prover.api_fallback: false): si el demostrador no resuelve (etapa 0, o DRAFT si está activo), el problema termina sin correr el bucle PLAN → … → CRITIQUE. Sin demostrador (servidor caído o enabled: false) los agentes corren siempre (Orchestrator._api_loop)	Dejarlo encendido	eval-v3: el bucle corrió en los 9 problemas que el demostrador no resolvió, costó US$0.061 y no resolvió ninguno (#115)	tests/test_prover.py::test_api_fallback_off_ends_after_stage0_without_api_calls
117	DRAFT (Draft-Sketch-Prove, prover.dsp): si la etapa 0 falla, el modelo de la API escribe plan (Planificador) y prueba informal (Generador), 2 llamadas, y el demostrador local las recibe dentro de su prompt (prover.draft_hint) junto con k_lemmas = 10 lemas del canal A del RAG para el goal raíz, con su firma; k_draft = 8 muestras (8 de la etapa 0 + 8 con borrador = 16, comparadas con las primeras 16 de baseline_prover32, que comparten semillas y caché). Los lemas mostrados se citan (M*) y used_in_proof mide si el término los usó. El borrador usa la sección llm_draft de versions.yaml: el mismo DeepSeek V4 Flash con razonamiento (reasoning_effort: high, 16 000 tokens)	El modelo general como demostrador (eval-v1/v2) o como respaldo (eval-v3); pasar el plan sólo al bucle de agentes	El modelo general razona bien en lenguaje natural y mal en Lean 4.28; el demostrador sabe Lean. Es la forma en que la API y el RAG pueden influir en la prueba que se acepta. El razonamiento se había apagado por latencia (#50), que aquí no importa frente a minutos de GPU por muestra. Smoke real (1 problema, etapa 0 apagada): resuelto por DRAFT con 2 llamadas, US$0.0005	tests/test_prover.py::test_draft_puts_plan_sketch_and_rag_lemmas_in_the_prover_prompt; orchestrator/graph.py::draft
118	Servidor del demostrador con 6 slots × 16 384 tokens (scripts/prover_server.sh; eval-v3 usó 8 × 12 288). El prompt de DRAFT crece 1-2 k tokens y no cabía junto a los 11 500 de salida. La caché de muestras no depende del servidor (clave = mensajes + semilla + max_tokens + temperatura): las muestras de eval-v3 se reutilizan	Bajar max_tokens del borrador	El demostrador necesita las salidas largas en los problemas difíciles; la GPU satura en ~70 tok/s agregados con 6 u 8 slots	tools/logs/prover_server.log: n_slots = 6, n_ctx_slot = 16384
119	Conjunto fuera de miniF2F (data/eval/problems/pdf_set.jsonl, 32 problemas de álgebra, teoría de números y combinatoria del PDF de olimpiadas; sin geometría): enunciados informales parafraseados en inglés y formalizados por el asistente; respuestas comprobadas por fuerza bruta antes de formalizar; los 32 elaboran en el Lean fijado con un único goal. No se versiona (deriva del PDF de licencia desconocida, SEC-2). Con DRAFT se corre sin ejemplares informales (dsp8: corpora: [mathlib]): el corpus informal ES ese PDF y traería la solución del propio problema. Limitaciones: formalización no revisada por un humano; las versiones informales de estos problemas clásicos pueden estar en internet (no hay formalización en Lean conocida). Hallazgo lateral: LeanChecker.goals como primera llamada de un REPL nuevo falla como si Mathlib no estuviera importado (unknown namespace BigOperators); el runner y la demo siempre hacen antes un check de calentamiento, así que no afecta, pero queda anotado	PutnamBench (pin de Mathlib distinto, #67); problemas de 2025-2026 escritos de memoria (riesgo de enunciados mal recordados)	Medir si el 21/30 de eval-v3 depende de que miniF2F sea el benchmark público del demostrador	scratchpad build_pdf_set.py / check_pdf_set.py de la sesión; errores: 0
120	Demo con el sistema actual: demo/app.py conecta el demostrador (prover.local_prover, compartido con el runner), usa un REPL de Lean para toda la sesión (antes abría y cerraba uno por problema: ~5 min de import Mathlib cada vez), lo precalienta con el embedder en segundo plano al arrancar, acepta la cabecera open … y trae 4 problemas de eval-v3 como ejemplos (sus muestras están en caché: salen en segundos, la verificación corre en vivo). scripts/demo_up.sh levanta todo con un comando	Dejar la demo con el flujo de agentes	La demo corría el sistema de 8/30, no el de 21/30	demo/app.py, scripts/demo_up.sh, scripts/prover_server.sh
121	Las sobreescrituras de configs se fusionan con los dicts de base (effective_config): baseline_prover32: {prover: {k_root: 32}} conserva el resto de prover. Antes un dict reemplazaba al de base entero	Repetir todas las claves en cada configuración	Configs de control (baseline_prover16/32, dsp8) de una línea	tests/test_prover.py::test_nested_config_overrides_merge_with_base
122	Servidor caído = la corrida se detiene, no "fallos" (prover.ProverUnavailable): si todas las muestras de un lote fallan y el servidor no responde a /health, LocalProver.sample lanza la excepción; el grafo y Orchestrator.solve la dejan pasar (como DailyQuotaExhausted) y run_suite corta con status: prover_down, sin escribir el par en curso, que se repite al reanudar. Además run_suite se niega a empezar si alguna configuración pedida necesita el demostrador (baseline_prover*, dsp*) y no responde, y la cadena de eval-v4 relanza el servidor antes de cada paso. Una muestra suelta que falla se sigue tolerando	Dejar que las configuraciones degraden en silencio (comportamiento anterior)	Primera noche de eval-v4: el servidor murió a las 22:27 (el log se corta en plena generación, causa desconocida) y la cadena siguió: 22 problemas del PDF quedaron como fallos con 0 muestras reales, baseline_prover32/16 como "unsupported" y dsp/dsp8 corrieron el bucle de agentes por API (US$0.023). Todo eso se apartó a data/eval/runs/_invalid/eval-v4-prover-down/; se conservan los 9 pares de pdf_set × baseline_prover terminados antes de la caída (6 resueltos)	tests/test_prover.py::test_dead_server_stops_the_run_instead_of_recording_false_failures
123	Más muestras no rinden en los difíciles: 32 → 16 en el control. pdf_set × baseline_prover terminó 21/32 (66 %; miniF2F 21/30): el demostrador generaliza fuera de su benchmark. En los 9 que eval-v3 no resolvió, 32 muestras resolvieron 0/6 a ~65 min por problema, y en imo_1978_p5 13 de 32 muestras no dejaron prueba extraíble (cortadas por largo). Se dejó de correr baseline_prover32 en los 3 que faltaban; el control de DRAFT/REPAIR es baseline_prover16 (las 8 primeras muestras y la corrección salen de la caché)	Terminar las 32 en los 9 (~3 h más de GPU)	La pregunta es si los agentes/RAG suman sobre el demostrador, no cuánto más da el mismo muestreo; 0/6 ya lo contesta	data/eval/runs/eval-v4-pdf/, data/eval/runs/eval-v4-unsolved/
124	Descomposición por API con razonamiento: descartada. Config decomp (el bucle de agentes con llm_draft, DeepSeek V4 Flash con razonamiento alto, y el demostrador en cada paso have): en 2 de los difíciles el Formalizador gastó todo su presupuesto de salida razonando (16 000 + 32 000 tokens en el reintento) y devolvió JSON vacío, y el Generador con razonamiento escribió como sketch un comentario sobre los ids de lemas en vez de la prueba. US$0.030 por 2 problemas, 0 resueltos. Se quitó la config; el prompt del Generador ahora exige la prueba entera en sketch (afecta también a DRAFT)	Bajar el esfuerzo de razonamiento o un modelo más caro (V4 Pro, ~20× el precio)	Gasto sin señal; la variante sin API (#125) ataca lo mismo gratis	data/eval/runs/smoke-decomp/
125	REPAIR (0 API, prover.repair): si la etapa 0 falla, las casi-pruebas del demostrador (≤ 2 errores de Lean: Lean sigue elaborando tras un have que falla, así que ≈ ≤ 2 pasos malos), con menos errores primero, se parten en sus have (skeletonize, como la prueba del Formalizador) y pasan por CLOSE: su propio bloque primero, la batería y el demostrador sobre el lema corto (max_goals 4 × k_goal 4) en los pasos que fallan; hasta 2 candidatas cuyo esqueleto elabora. Lo probado queda en proved. Config repair, en la cadena de eval-v4 junto a dsp y baseline_prover16. Sin el filtro de ≤ 2 errores tardaba ~20 min por paso en pruebas con muchos pasos malos (prueba apartada en _invalid/smoke-repair-sin-filtro)	Reparar con un LLM por API (#124)	Receta de DeepSeek-Prover-V2 / Goedel-Prover-V2 (cada subobjetivo como lema) sobre la estructura que el demostrador ya escribió, sin costo de API. Primeros resultados en los difíciles: cierra pasos (4 de 12) pero no el central	tests/test_prover.py::test_repair_closes_the_bad_step_of_a_failed_prover_proof_with_zero_api
126	Los difíciles: 2 de 9 son falsos y SKETCH para el resto. (a) mathd_algebra_437 (1/3 es división de naturales = 0: n = −1 cumple las hipótesis y la tesis dice −4) y numbertheory_notequiv2i2jasqbsqdiv8 (a = 1, b = 0: ¬(Even a ∧ Even b) es verdadero y 8 ∤ 1) son falsos tal como están en miniF2F-v2s: nadie puede demostrarlos. Sus negaciones están en data/eval/results/false_statements/FalseStatements.lean (se comprueban con Lean entre los pasos de la cadena: un segundo REPL no cabe en la RAM). Los 7 restantes, en eval_v3_unsolved_provable.jsonl. (b) SKETCH (prover.sketch rondas, config sketch = REPAIR + SKETCH): el modelo con razonamiento (llm_draft) escribe el esqueleto en Lean con pasos have … := by sorry en TEXTO (la versión JSON de #124 se quedaba sin presupuesto); CLOSE cierra cada paso con la batería y el demostrador sobre el lema corto; si quedan pasos abiertos o el esqueleto no elabora, la 2.ª ronda recibe los goals abiertos o el error de Lean. Es la receta de DeepSeek-Prover-V2 y el flujo de la propuesta (Planificador → subobjetivos → prueba de cada uno → Lean, RF-1). La cadena de eval-v4 se reordenó para correr primero sketch, dsp y el control sobre los 7 difíciles demostrables (3 h) y después los 11 fallos de pdf_set (5 h); la config sketch incluye REPAIR (solved_by distingue la etapa), así que repair ya no corre aparte	Un demostrador local más grande (Goedel-Prover-V2-32B: no cabe en 16 GB salvo en Q3, ~3× más lento, poca ganancia reportada); un modelo frontera escribiendo Lean entero (US$0.3-1 por problema con razonamiento, fuera del saldo)	El demostrador falla en el paso central de los difíciles; partirlo en lemas cortos es lo que funciona en los sistemas de referencia, y la parte por API es una llamada por ronda (~US$0.005)	tests/test_prover.py::test_sketch_skeleton_steps_are_closed_by_automation_and_the_prover
127	RAG de pruebas (rag/proofs.py, config rag_proofs, etapa EXAMPLES del nodo prove): el RAG de lemas no le aporta al demostrador (los lemas genéricos ya los conoce; en eval-v3 sugirió 8 nombres y el kernel no usó ninguno); lo que le falta es cómo se resolvió un problema parecido. Si la etapa 0 falla, se recuperan por embeddings (Qwen3-Embedding, el modelo del resto del RAG; consulta = enunciado informal + Lean) las pruebas verificadas de los 3 problemas más parecidos de Lean Workbook (29 750, MIT; 0 coinciden con miniF2F-v2s/v2c), que (1) se prueban tal cual sobre el enunciado (0 GPU) y (2) van como ejemplos en el prompt del demostrador (8 muestras: 8 + 8 como DRAFT, control baseline_prover16). Se excluyen los vecinos con similitud ≥ 0.95 (el mismo problema: la prueba sería la respuesta); la traza guarda los ids y similitudes recuperados, y proofs_preview.txt (en runs/, gitignored) lo que recupera cada problema, para revisar a mano si trae el mismo problema con otra formalización. Así el eje de embeddings de la propuesta vuelve a tener un papel medible (solved_by = prover_examples vs control). El índice se construye en la GPU con el demostrador apagado (eval_v4_part2.sh, que toma el relevo de la cadena al terminar los 7 difíciles y corre rag_proofs antes que el resto de pdf_set)	Lemas por paso en el prompt del demostrador (idea más barata, pero DRAFT ya mide si los lemas en el prompt sirven); embeber ya, en paralelo (Windows tiene ~1 GB de RAM libre y la VRAM la ocupa el demostrador)	TacticToe/Tactician (k-NN sobre pruebas) y Rango (recuperar pruebas además de premisas) muestran que lo que más transfiere son pruebas de problemas parecidos	tests/test_prover.py::test_rag_proofs_tries_retrieved_proofs_then_puts_them_in_the_prover_prompt, ::test_proof_corpus_parsing_strips_comments_and_keeps_statement
128	Por qué SKETCH casi no funcionó en eval-v4, y su arreglo. (a) 32 de 38 llamadas del Sketcher se cortaron en los 16 000 tokens de llm_draft: el modelo razonaba hasta el tope y no llegaba a escribir el bloque Lean; aun así resolvió amc12b_2002_p3 (el control de 16 muestras no). SKETCH tiene ahora su propio tope (sketch_max_tokens: 40000, US$0.007 por llamada; llm_draft.timeout_s 900 → 1800); DRAFT no cambia (1 de 15 llamadas cortadas) para no romper su comparación. (b) Pasos "stale" sin probar: un bloque de varias líneas (el del demostrador o del modelo para un paso) no llevaba límite de heartbeats, agotaba el timeout de reloj y reiniciaba el REPL (5 min); con 3 hilos sobre un REPL, todos los pasos siguientes de todos los hilos quedaban "stale proof state" sin probarse (en numbertheory_aneqprodakp4… 9 de 11 pasos; los esqueletos eran correctos: invariante aₙ₊₁ = (aₙ − 2)², período 12 en amc12a_2002_p21). Ahora limit_heartbeats envuelve los bloques en · bajo set_option maxHeartbeats y CLOSE re-elabora el esqueleto (proof_state nuevos) y reintenta el paso una vez si el REPL se reinició (_close_one)	Volver a 1 hilo (evita que un reinicio afecte a otros, pero no el reinicio, y triplica el tiempo)	Los dos defectos explican casi todos los fallos de SKETCH en los difíciles; repetirlo con los arreglos es lo de mayor valor esperado por hora de GPU	tests/test_prover.py::test_close_reelaborates_the_skeleton_when_the_repl_restarts_instead_of_leaving_steps_unproved, ::test_heartbeat_limit_covers_multiline_blocks, tests/test_goal_mode_slow.py::test_multiline_step_runs_under_the_heartbeat_limit (con Lean real, al relanzar)
129	Publicación en Hugging Face: código como repositorio de modelo, no como Space. Crear el Space de Gradio devolvió HTTP 402: desde 2026 alojar Gradio o Docker en cpu-basic pide PRO. publish_space.py --model sube lo mismo como repositorio de modelo (gratis): app, paquete, configs, docs, notebook, tests, scripts, pyproject.toml + uv.lock, LICENSE y CITATION, con la comprobación de texto del PDF de publish_hf.py (antes el Space no la tenía). La demo se corre en local (scripts/demo_up.sh); sin --model, el mismo script publica el Space cuando haya PRO. El dataset suma el índice proofs, la caché del demostrador y las corridas eval-v2/v3/v4 (sin eval-v4-pdf ni pdf_set.jsonl: salen del PDF, SEC-2); el saneado de citas cubre ahora también errors.jsonl (eval-v2 tenía 6 snippet del PDF). Además, la comprobación con Lean previa a eval-v4b abortó la primera vez por un error del test, no del envoltorio: suponía 3 goals en un esqueleto con 2 sorry	Pagar PRO (US$9/mes); un Space estático sin demo	La propuesta pide el repositorio en HF; la demo interactiva necesita CPU con Python, que ya no es gratis	huggingface.co/CamiloS1111/ragsolver, huggingface.co/datasets/CamiloS1111/ragsolver-index; data/eval/results/eval_v4b_test_bug.log
130	Resultado de eval-v4b: SKETCH, con los arreglos de #128, es la primera configuración que supera al demostrador solo fuera de miniF2F (pdf_set 22/32 frente a 21/32; gana pdf_p41 por SKETCH y pdf_p33 por REPAIR, pierde pdf_p58; McNemar 2-1, p = 1.0). En los difíciles se queda en 1/7 (amc12b_2002_p3, ahora por REPAIR). Llamadas cortadas: 32/38 → 12/34; 0 pasos "stale". El control baseline_prover16 resuelve los mismos 21 que baseline_prover, así que pdf_p33 en dsp8 es mérito del borrador. Las dos pruebas nuevas: axiomas estándar y solo citas de Mathlib. US$0.33 entre eval-v4 y eval-v4b	—	—	data/eval/runs/eval-v4b-{pdf,unsolved}/, data/eval/results/eval_v4_analysis.json, docs/eval_report_v4.md