Upload folder using huggingface_hub
d199b14 verified 10 days ago
115 kB
# 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|all` los agrega al mismo `informal.jsonl` (por defecto `none`: 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`) | `src/ragsolver/rag/mineru_blocks.py`, `ingest_informal.run(sections=...)` |
| 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](https://github.com/MoonshotAI/Kimina-Prover-Preview/issues/11)). Corregido en `lean/verify.py` (niveles de la [guía oficial de Lean](https://lean-lang.org/doc/reference/latest/ValidatingProofs/)): `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` |