docs/PROGRESS.md

# Progreso de implementación — RagSolver

> Se actualiza mientras el agente trabaja. Última actualización: 2026-09-24.

## Estado actual

**Núcleo del proyecto (Fases 0-6 de `docs/PLAN_RAG.md`): completo y ejecutado.** Índice de Mathlib completo (278 160 declaraciones) con ANN IVF_SQ; agentes LangGraph + verificador Lean vía REPL; experimento principal `eval_v1` terminado (300/300 pares): `full` 9/60 (15 %), `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); ninguna diferencia significativa tras Bonferroni. Detalle en `docs/eval_report.md` y `docs/final_report.md` (§6-§7). `eval-v1-full` (índice completo, ≈ US$0.30) preparado en `scripts/run_chain.sh`, sin correr — requiere tu aprobación.

**Auditoría técnica (2026-09-23) y su corrección, en curso.** `docs/AUDIT_2026-09-23.md` (diagnóstico completo) y `docs/PLAN_CORRECCIONES.md` (plan por fases). Avance:
- **Fase 1 — verificador seguro (SEC-1, VER-1, BUG-2): ✅ completa.** `lean/verify.py` valida las tácticas del LLM antes de tocar Lean (rechaza comandos, metaprogramación, declaraciones nuevas, `sorry`/`native_decide`/`decide +native`) y audita `#print axioms` tras un veredicto limpio (sólo `propext`/`Classical.choice`/`Quot.sound`). Confirmado con Lean real: el exploit de inyección de la auditoría ya no se ejecuta; `decide +native` ya no pasa como "verificado". Re-verificación offline de `eval_v1` (0 llamadas LLM): **27/27 pruebas antes aceptadas siguen aceptadas, 0 regresiones** — los resultados reportados no cambian. DECISIONS #69-74.
- **Fase 2 — licencias y datos (SEC-2): ✅ completa.** `.gitignore` ampliado (PDF de ejemplo, `blobs/`, `data/eval/runs/`, artefactos de Lean); se encontró y corrigió una fuga no detectada por la auditoría (`docs/qa_ingest_edd3436ca148.md` embebía fórmulas/descripciones del PDF — ahora redactado cuando el documento no es redistribuible); `scripts/publish_hf.py` sube las corridas desde una copia saneada y aborta si encuentra texto del corpus informal en lo que va a subir. Comprobación reutilizable: `scripts/check_no_leaked_content.py` (0 coincidencias sobre el repo). DECISIONS #75-77.
- **Fase 3 — dependencias y documentación de estado: ✅ completa.** `httpx`/`tenacity` declarados, `gradio` en el extra `demo`, `ranx` movido a `dev`; `pandas`/`accelerate` quitados de las dependencias core (confirmado sin ellos: `test_retriever_integration.py` carga el embedder Y el reranker reales en verde). Documentación al día: README, `install.md` (+ tabla de variables de entorno), `interfaces.md`, `architecture.md`, `evaluate.py`, `versions.yaml`, `final_report.md` (limitaciones MET-1/DATA-1/BUG-1 añadidas, "release" atenuado a "prepared for release"). DECISIONS #78-79.
- **Fase 4 — citas, trazas y contabilidad (BUG-1, TRZ-1, LLM-1, ACC-1, BUG-5, BUG-6): ✅ completa.** Los `citation_id` ya no se renumeran en cada búsqueda (se reutilizan por `chunk_id`, sin duplicados tras un replan o una re-recuperación); las trazas del retriever de un par (config, problema) van al mismo archivo que las de sus agentes (antes, un archivo aleatorio por búsqueda); el pin de versiones registra qué tabla sirve `mathlib`; el cliente LLM ya no reintenta un timeout de lectura (podría haberse cobrado igual), baja de 20 a 4 intentos y cuenta cuántos hizo; cualquier excepción dentro de un nodo del grafo (no sólo salida JSON inválida) conserva lo acumulado en vez de perderlo; se corrigieron dos bugs de contabilidad menores (self-consistency, caché de embeddings de consulta sin lock). DECISIONS #80-88. 138 tests en verde (incluidos los de Lean real). El smoke con LLM real (D6, ≈ US$0.001) queda pendiente de tu aprobación.
- **Fases 5-10:** sin empezar. Ver `docs/PLAN_CORRECCIONES.md §7` para el orden y qué necesita una decisión tuya (D1-D8: licencia, commit, `blobs/`, alcance de la ingesta, replan, gasto, token de HF, sandbox).

**Mejora del RAG (2026-10-14): implementada (Fases 0-4 y 2b de `docs/PLAN_MEJORA_RAG.md`), medida sin LLM; falta la re-evaluación pagada (Fase 6, decisión R4).**
- El retrieval de Mathlib consulta con el *goal* de Lean. El Autoformalizador escribe un esqueleto `have … := by sorry` y el REPL devuelve un goal por `sorry`.
- Canal principal: prior de competición (778 lemas de Lean Workbook validados contra Lean, núcleo incluido). Recall@16 por goal 0.327, frente a 0.028 del índice denso, que queda apagado.
- Las premisas se consumen con una batería de tácticas (CLOSE, 0 LLM). Sobre el goal raíz de `eval_v1`: 11/60 sin premisas, 12/60 con premisas, y 4 problemas que no resolvió ninguna configuración anterior. FILL (1 llamada) sólo ve los goals abiertos.
- Los goals probados se conservan entre intentos y replans. El replan recibe el feedback del Crítico (DES-1 cerrado).
- Nuevas configuraciones: `rag_nl` (flujo de eval-v1), `baseline_auto` (0 LLM); `no_rag` usa la misma batería sin premisas.
- Smoke con LLM real (8 problemas, US$0.0145 en total): 5/8 con el prompt 2, que reveló que el modelo no escribe `sorry`. Con la partición mecánica de la prueba en goals (`skeletonize`, prompt 3): **8/8**. Medido sobre el término aceptado, ninguna premisa recuperada se usó en esas 8 pruebas: la mejora viene de la partición y de la automatización. OpenRouter: con el tope de precio actual sólo califica DeepInfra, que da 429 intermitentes (#103).
- Tests: 146 rápidos y 11 con Lean real, en verde. `DECISIONS.md` #89-#108.
- **eval-v2 (2026-10-15), parcial — `docs/eval_report_v2.md`.** Ronda 1 de 4: `full` 6/15, `no_rag` 7/15, `baseline_auto` 5/15 (eval-v1 en los mismos 15: 3 y 4). `baseline_auto` en los 60: **11/60 sin LLM**, más que eval-v1 `full` (9/60). El RAG por goal todavía no muestra efecto medible. El guardia de costo detuvo la cadena: la proyección para las rondas 2-4 (~US$0.34) supera el saldo (US$0.289). Decisión del usuario: opción B (rondas 2-3); ronda 2: 2/15 en las tres configuraciones; ronda 3 detenida para rediseñar.
- **Rediseño (2026-10-15), en evaluación — `docs/PLAN_REDISENO_PROVER.md`.** Demostrador especializado local (Goedel-Prover-V2-8B Q6_K en la GPU, 0 API) como etapa 0 y para los goals abiertos. El RAG corrige nombres de lemas renombrados entre versiones de Mathlib. Salidas ilegibles del Crítico y de FILL ya no matan el problema. Smoke real: 2/2 sin API. `DECISIONS.md` #110-#115.
- **eval-v3 (2026-10-15) — `docs/eval_report_v3.md`: el rediseño resuelve 21/30, frente a 8/30 del sistema anterior** en los mismos problemas (McNemar 13 a 0, p = 0.0002). Dificultad 2-3: de 0/14 a 8/14, con 2 problemas de IMO. Todo lo resuelve el demostrador local sin API; los agentes y el RAG no añaden problemas en su forma actual (`full` = `baseline_prover`). Costo de API: US$0.061; saldo de la key: US$0.059. Limitación: posible contaminación de miniF2F. Próximos pasos propuestos en el §5 del reporte.

**Pendiente del usuario:** LICENSE (sugerido Apache-2.0), commit en git (nada commiteado todavía), si versionar `Propuesta_Proyecto_Final_IA_UPTC.pdf`, token de HF, y si correr `eval-v1-full` (≈ US$0.30; saldo de la key ≈ US$0.42).

## Historial

Lo que sigue es el registro de cómo se llegó al estado de arriba, por fase, escrito mientras se ejecutaba cada una. Se conserva como referencia; para el estado real del proyecto usar la sección anterior.

### Restricciones reales de este sandbox (no son del proyecto, son de este entorno de ejecución)

- **RAM ajustada**: 7.3 GB totales. Con un solo proceso de embeddings/evaluación corriendo ya se usa ~75-90% + algo de swap. Por eso el agente evita correr dos cargas pesadas (embeddings, reranking, MinerU) al mismo tiempo.
- **Filesystem `/mnt/c/` (montaje 9p de WSL2) es lento** para imports de paquetes grandes (torch tardó ~150s en importar la primera vez).
- Con estas limitaciones, el trabajo de esta sesión prioriza **corridas acotadas pero reales** (nunca resultados inventados) sobre corridas completas a escala de producción. (Nota posterior: al momento de escribir esto la GPU AMD todavía no se había probado desde esta sesión — ver más abajo "GPU AMD: ✅ utilizable" — la limitación real nunca fue la falta de GPU, sino RAM/CPU del sandbox.)

### Fase 0 — Cimientos: ✅ completa

- Repo, `pyproject.toml` (Python 3.12 vía `uv`), `.gitignore`.
- `configs/versions.yaml` — pin único de versiones (Lean, Mathlib, modelos).
- `src/ragsolver/rag/schema.py` — contratos Pydantic de §7/§8 del plan + JSON Schema exportado a `docs/interfaces/`.
- Escritor de traza JSONL + tests.
- **Lean 4 (`v4.28.0-rc1`) + Mathlib (`v4.28.0-rc1`, caché precompilado 7873 archivos) instalados y verificados**: `lake build` → "Build completed successfully" — el kernel de Lean aceptó `example : 1 + 1 = 2 := rfl`.
- `docs/DECISIONS.md` con 13 decisiones registradas y su evidencia.
- 19/19 tests pasando en ese momento (ver conteo actualizado más abajo si se agregaron más).

### Fase 1 — Índice de Mathlib: código completo, corrida real en curso

Hecho:
- Descarga del corpus real de LeanSearch v2 (310 579 declaraciones) y normalización → **278 560 chunks** válidos (32 019 excluidos por filtro).
- `embed.py`, `index.py`, `retrieve.py` (con CLI), `evaluate.py` escritos, con tests de integración reales contra LanceDB (que de hecho encontraron y corrigieron 2 incompatibilidades de API con la versión instalada).
- **Hallazgo importante documentado en `DECISIONS.md`**: sólo 117/540 nombres "gold" de los benchmarks propios de LeanSearch v2 (MathlibQR+MathlibMPR) existen en el corpus JSONL que ellos mismos publicaron para esa tag. El recall contra esos benchmarks está acotado por esa cobertura, no sólo por la calidad del retriever.
- Por las limitaciones de cómputo del sandbox, se embebió una **muestra acotada real** (no simulada): 116 declaraciones gold + 3000 distractores aleatorios = 13 736 registros, con Qwen3-Embedding-0.6B en CPU (~5.5 textos/seg, ~42 min de corrida real).
- **Índice LanceDB real construido** sobre esa muestra (13 736 filas, vector + FTS).
- `evaluate.py` (Recall@10/nDCG@10/MRR, denso vs BM25 vs híbrido vs híbrido+rerank sobre MathlibQR) corrido sobre esa muestra acotada de 13 736 filas.

**Estos primeros números (recall condicionado 0.947 con fusión híbrida) quedaron invalidados por un bug de ingesta encontrado en la Fase 3** (`name[0]` en vez del nombre completo, `DECISIONS.md` #31): con el corpus renormalizado, la cobertura real y las métricas correctas son las que aparecen en la entrada de Fase 3 más abajo (recall condicionado real ≈ 0.78-0.79, no 0.947), y más tarde las del índice completo (Fase 5/#56/#68: recall@10 híbrido+rerank 0.45). Se deja esta nota en vez del número original para no repetir el error.

Fase 1 se da por **completa**. Pendiente sólo si el usuario pide explícitamente escalar a las 278 560 declaraciones completas (ver "Bloqueado" más abajo — no es un bloqueo real, es una corrida de ~14h que no se lanzó sin avisar).

### Fase 2 — Ingesta de PDFs: ✅ completa (2026-09-19, segunda sesión)

Resultado sobre `problemas resueltos olimpiadas.pdf` (detalle en `docs/qa_ingest_edd3436ca148.md` y `docs/DECISIONS.md` #15-#22):

- **100/100 problem cards emparejadas** (era 92/100). 98 por vía determinista (numerales absorbidos en ecuaciones recuperados por regex; solución 1 por regla "lo que precede al ítem 2"), la 55 por split con LLM, y la **77 recuperada de un hueco que MinerU se había saltado por completo** (pág. 64: cero bloques en media página). Ese hueco se detecta cruzando la capa de texto del PDF palabra por palabra contra los bboxes de MinerU; 7 regiones así se transcribieron con el VLM (Plan B acotado, no página completa).
- **53 figuras** recortadas (con padding para las etiquetas) y descritas con contexto del enunciado. Red de seguridad vectorial: **0 figuras perdidas por MinerU** (los 36 clusters "sin cubrir" son radicales del Equation Editor, tablas bien clasificadas o clusters fusionados). QA gate del plan: 7/7 problemas con figura; **rúbrica manual 15/15** aprobadas (umbral 13/15).
- QA de fórmulas con VLM: 209 propuestas, **76 aplicadas / 133 rechazadas** por guardas calibradas con casos reales (el VLM mete ruido de puntuación, absorbe texto vecino y a veces recorta contenido real o devuelve LaTeX destrozado). Todo cambio queda registrado para revisión.
- 100 resúmenes contextuales (Contextual Retrieval) + `math_area`, `techniques`, `theorems_used`, `difficulty`, `keywords` por card.
- Corpus: `data/corpus/informal.jsonl` (153 chunks: 100 `problem_card` + 53 `figure`), `figures.jsonl`; embebido con Qwen3-Embedding-0.6B (CPU, 215 s) e indexado en LanceDB (`data/index/lancedb/informal`, FTS incluido).
- **Búsqueda real verificada** (`python -m ragsolver.rag.retrieve "..." --corpus informal --mode exemplar`): 3 consultas en inglés → problema correcto en el puesto 1 (8, 86, 77); la geométrica trae además los chunks de figura.
- Proveedor: **Gemini** (tier gratis). Hallazgo importante: la cuota gratis es **20 solicitudes/día por modelo** en `gemini-3.5-flash` → cadena de fallback por modelo (`configs/versions.yaml: fallback_models`); en la práctica todo el enriquecimiento lo hizo `gemini-3.5-flash-lite` (su cuota diaria aguantó ~250 llamadas). Cada figura/card registra el modelo que la produjo. Caché JSONL por llamada: re-ejecutar la ingesta no repite llamadas.
- Código nuevo: `rag/mineru_blocks.py` (lector/render de bloques MinerU + cross-check capa de texto), `rag/figures.py`, `rag/enrich.py` (cliente Gemini REST con caché, reintentos y cadena de modelos), `rag/ingest_informal.py` (pipeline completo, `--skip-llm` para correr sin API), `scripts/qa_ingest_report.py`. 43 tests pasando (nuevos: `test_mineru_blocks.py`, `test_figures.py`, `test_enrich.py`).

Pendiente de Fase 2 (no bloqueante):
- Gold de OCR de 10 páginas transcritas a mano (tarea 10 del plan): requiere trabajo humano; no se fabricó.
- Chunking en `solution_step`: no hace falta para este PDF (card más larga ≈ 2 900 caracteres, muy por debajo de ~1 500 tokens).

### Fase 3 — Servicio de recuperación y citación: ✅ completa (2026-09-20)

- `Retriever.search(RetrievalRequest) -> RetrievalResult` cubre §6.3/§8: plantillas de consulta por `mode` (`configs/retrieval.yaml`), denso + FTS con **prefiltro SQL** (`doc_ids`, `unit_types`, `kinds`, `math_area`), RRF multi-consulta, rerank contra `rerank_against`, dedupe (figura ↔ su card; `max_per_module` opcional), **figuras adjuntas** desde la tabla `figures`, citas con `snippet`, traza JSONL, caché de embeddings de consulta, flags de ablación (`enabled=false` → vacío con traza).
- **Modo `error`**: identificadores Lean del mensaje → búsqueda exacta fijada al top-1 (verificado con reranker adverso y sobre el índice real).
- `evaluate.py` pasa por `Retriever.search` (misma función que los agentes). CLI `ragsolver search` / `ragsolver ingest`.
- Tests: 10 unitarios con LanceDB temporal + embedder/reranker falsos, 2 de integración sobre el índice real. Suite: 62 tests.
- **Bug grave de Fase 1 detectado y corregido** (`DECISIONS.md` #31-32): `ingest_mathlib.py` usaba `name[0]` cuando `name` es la lista de componentes del nombre → 90 % de las declaraciones con nombre/`docs_url`/`chunk_id` incorrectos y repetidos. Con el corpus renormalizado: 503/540 nombres gold existen (antes "117"); **métricas corregidas (946 consultas, cobertura 83.8 %)**: recall@10 denso 0.665 / BM25 0.594 / híbrido 0.656; nDCG@10 0.565 / 0.472 / 0.538. En 40 consultas al azar con rerank: híbrido+rerank 0.775 > denso 0.75 > híbrido 0.675 > BM25 0.525. La conclusión de Fase 1 ("recall condicionado 0.947") estaba inflada por el bug.

### Fase 4 — Grafo de agentes: ✅ completa y ejecutada (2026-09-20)

**Aceptación cumplida**: los 5 teoremas triviales de referencia se resuelven con el pipeline completo (`f4-trivial-full`: 5/5, 3 llamadas LLM cada uno, citas `used_in_proof` en `triv_add_zero` y `triv_add_comm`), ≤ 20 llamadas por problema en todas las corridas (máx. 11), `llm_calls=0` en todos los eventos del retriever.

- `ragsolver/llm.py`: cliente único Gemini / OpenAI-compatible (**OpenRouter preparado por config**, sin key), cadena de modelos por cuota diaria, contadores de tokens. El Enricher de Fase 2 lo usa.
- Agentes (`agents/agents.py`, contratos en `agents/schemas.py`, prompts en `configs/agents.yaml`): Planificador (con ejemplares del corpus informal), Generador (`used_citations`), Autoformalizador (**sólo tácticas**: el enunciado se empalma desde el problema, el LLM no puede debilitarlo), Crítico (taxonomía + `missing_identifiers` → re-recuperación en modo `error`), líneas base A/B de la propuesta §8.2.
- Orquestador LangGraph (`orchestrator/graph.py`): PLAN → RETRIEVE → GENERATE → FORMALIZE → VERIFY → CRITIQUE con presupuesto RNF-3 (≤ 20 llamadas) dentro del grafo; `SolutionReport` con citas verificadas / usadas en boceto / consultadas.
- Verificador (`lean/verify.py`): REPL persistente con `lean-interact` (`import Mathlib` una vez, ~0.3 s por teorema) usando la caché de Mathlib en ext4 (`~/ragsolver_cache/lean_project`, `DECISIONS.md` #35); respaldo por proceso `lake env lean`.
- Runner de ablaciones (`orchestrator/run.py`): `full`, `no_rag`, `no_critic`, `baseline_a`, `baseline_b` → `data/eval/runs/<run_id>/results.jsonl` + `summary.json` (pass@1 con Wilson, llamadas, tokens, precisión de uso de lemas, re-recuperación, taxonomía).
- 8 tests con LLM/verificador/retriever simulados.
- Problemas: `data/eval/problems/dev_trivial.jsonl` (5 teoremas de referencia) y `dev_minif2f.jsonl` (8 de miniF2F-v2s valid, con cabecera `open ...`).

### Fase 5 — Evaluación: ✅ ejecutada (2026-09-20) — `docs/eval_report.md`

Resultados clave (tabla de muestra de Mathlib con 3 903 filas; 13 problemas dev = 5 triviales + 8 miniF2F-v2s):
- MathlibQR (946 consultas): recall@10 denso 0.662 / BM25 0.595 / híbrido 0.655; en 100 al azar con rerank: denso 0.76 (nDCG@10 0.631), híbrido+rerank 0.71 (0.617), híbrido 0.66, BM25 0.56 — el rerank recupera lo que pierde la fusión con BM25, pero el denso solo sigue siendo el mejor en esta muestra (`DECISIONS.md` #32). Premisas gold de miniF2F (352 problemas): recall@20 0.15 (informal) / 0.18 (formal) — cota inferior, la consulta real es por subobjetivo.
- Gold informal: **30/30 en el top-5, MRR 1.0**; cobertura de entidades en figuras 0.91. Contaminación: 0 pares > 0.9 (máx. 0.818).
- Ablaciones (pass@1): `full` 9/13, `no_rag` 10/13, `no_critic` 6/13, línea base A 8/13, línea base B 0 (se autoevalúa correcta 13/13 → 5 falsos positivos evitados). **El Crítico aporta +0.23**; el RAG no aporta en este dev set (−0.08, p=1.0) y triplica los tokens: los problemas se resuelven con automatización de tácticas y casi no se citan lemas por nombre (precisión de uso de lemas 0.011). Es el resultado honesto del §8.3 con n=13; hace falta el conjunto de 30-60 problemas más difíciles del plan para medir el aporte del RAG donde importa.
- Hallazgo operativo: `ranx` devolvió métricas absurdas en dos corridas largas → métricas propias (`rag/metrics.py`) verificadas contra `ranx` (`DECISIONS.md` #43).

- Premisas gold: `scripts/build_premise_gold.py` → 352 problemas / 402 lemas desde las pruebas verificadas de DeepSeek-Prover-V2 (`DECISIONS.md` #38); `scripts/eval_premises.py` (Recall@8/@20, nDCG@10, consulta informal y formal).
- Gold informal: `data/eval/informal_gold.jsonl` (30 consultas, 15 con figura; anotado por el asistente, `DECISIONS.md` #39); `scripts/eval_informal_gold.py`.
- Contaminación: `scripts/contamination.py` (coseno card ↔ miniF2F-v2s).
- Informe: `scripts/eval_report.py` → `docs/eval_report.md` (ablaciones, IC de Wilson, taxonomía).

### Fase 6 — Empaquetado y documentación: preparada (2026-09-20)

- Documentación: `docs/architecture.md` (arquitectura implementada, flujo por problema, citación), `docs/install.md`, `docs/interfaces.md` (+ JSON Schema de los 8 contratos de agentes en `docs/interfaces/`), `docs/reproduce.md` (comandos y tiempos medidos).
- Demo Gradio `demo/app.py`: pestaña "Buscar" (hits con citas, firma Lean, `docs_url`, recortes y descripciones de figura) y "Resolver" (pipeline completo o líneas base, con presupuesto). Gradio ya estaba instalado (vía MinerU); no se lanzó en esta sesión por memoria.
- Publicación en HF Hub: `scripts/publish_hf.py` (dataset card, índice Mathlib, corpus normalizado, evaluación; **excluye** el PDF, sus recortes y su texto por `redistributable=false`). ✅ Publicado el 2026-10-22 (DECISIONS #129).
- Notebook `notebooks/01_results.ipynb`: tablas de todas las evaluaciones + McNemar exacto entre configuraciones.

### Cumplimiento de la propuesta (mapeo 2026-09-20, tarde)

| Requisito | Estado |
|---|---|
| Obj. 5 — conjunto de evaluación 30-60 estratificado con partición dev/test | ✅ `data/eval/problems/eval_v1.jsonl` (60: 24 dev / 36 test; 3 áreas × 3 niveles) + ficha `README.md`. **Parcial**: 42/60 pares `full` válidos (10 resueltos) con DeepSeek V4 Flash vía OpenRouter, 6 hilos; **detenida a las 03:15 del 21-09 por el tope de US$0.50 de la key** (DECISIONS #47, #50-#54). Se reanuda con `nohup bash scripts/run_eval_v1.sh > data/eval/results/eval_v1.log 2>&1 &` en cuanto se suba el límite (≈ US$0.85 más para todo, incluido el índice completo) |
| RF-7 — decisión por agente e intento en la traza | ✅ `request.decision` en cada `TraceEvent` + evento del verificador |
| RNF-2 — semilla fijada | ✅ `seed: 13` en `versions.yaml`, pasado a Gemini/OpenAI; verificado con llamada real |
| §8.3 — llamadas de recuperación, pass por intento | ✅ `retrieval_calls`, `pass_by_attempt` en `summary.json` |
| §8.4 — bootstrap para costo/latencia | ✅ `*_ci95_bootstrap` en `summary.json` |
| §10.2 — CITATION.cff, CI, LICENSE | ✅ `CITATION.cff` (autores: Camilo Andres Niño Amaya, Jose L. Salamanca), `.github/workflows/ci.yml`, `LICENSE` Apache-2.0 (2026-10-21) |
| §10.3 — guía de usuario, diagrama de secuencia | ✅ `docs/user_guide.md`, `docs/architecture.md` §3 |
| §10.1 — informe final en inglés (IMRaD) | ✅ borrador `docs/final_report.md` con resultados actuales y 24 referencias; §6.3 se completa con `eval_v1` |
| Obj. 7 — HF Hub + Space | ✅ publicado (2026-10-22): código en huggingface.co/CamiloS1111/ragsolver (repositorio de modelo: el Space de Gradio pide PRO, DECISIONS #129), datos en huggingface.co/datasets/CamiloS1111/ragsolver-index; demo en local |
| RF-1 — subobjetivos verificables independientemente | parcial: se verifican dentro de una sola prueba (`have`), no como lemas aislados |
| §6.3 — self-consistency del Generador | ✅ `generator_samples` (apagado por defecto; cuenta en el presupuesto) |
| Corrida principal reanudable | ✅ `scripts/run_eval_v1.sh` (salta lo hecho; corta limpio si se agota la cuota) |

### GPU AMD: ✅ utilizable vía Windows + Vulkan (llama.cpp) para embeddings (2026-09-20)

`llama-server.exe` del lado de Windows con el GGUF de Qwen3-Embedding y `RAGSOLVER_EMBED_BACKEND=llama` en WSL: vectores idénticos (cos ≥ 0.9996), ~48 textos/s (10× la CPU). El corpus completo de Mathlib (278k) se está embebiendo (~96 min) → tabla `mathlib_full` (`DECISIONS.md` #48). ROCm en WSL2 sigue sin funcionar (abajo), pero ya no hace falta para el retriever.

### GPU AMD (ROCm en WSL2): ❌ no viable hoy

La tarjeta real es una **RX 9060 XT (gfx1200)**, no la 9070 XT asumida. `rocminfo` falla con `HSA_STATUS_ERROR_OUT_OF_RESOURCES` incluso con `librocdxg` v1.2.2 y tras reiniciar WSL; es el bug abierto `ROCm/ROCm#6323` (mismo hardware, cerrado por AMD como "not planned"). Todo corre en CPU + API; re-evaluar cuando AMD publique un fix (`docs/DECISIONS.md` #8-#12).

### Bloqueado / decisiones pendientes del usuario (2026-09-23)

1. ~~**LICENSE**~~ ✅ Apache-2.0 (2026-10-21).
2. ~~**Commit en git**~~ ✅ rama `rag`.
3. ✅ (2026-10-22, DECISIONS #129) **Publicación en Hugging Face** (entregable 2 de la propuesta): `HF_TOKEN` con permiso de escritura y nombres de repo; los scripts `publish_hf.py` (dataset: índice muestra + completo con ANN, evaluación, corridas) y `publish_space.py` (demo de búsqueda) ya funcionan en `--dry-run`.
4. **`eval-v1-full`** (repetición de `full`/`no_critic` con el índice completo): ≈ US$0.30; la key tiene US$0.42 libres de su tope de US$2.00. Se lanza con `setsid nohup bash scripts/run_chain.sh > data/eval/results/chain.log 2>&1 < /dev/null &` (salta `eval_v1`, que ya está completo).
5. Opcionales: gold manual de OCR (10 páginas) para la métrica de exactitud de fórmulas; experimento adicional con un modelo local en la GPU (US$0, ~5 h; ver conversación del 22-09); PDF del informe final si el curso lo pide en ese formato.

### Noche del 22→23-09: qué quedó hecho

- **`eval_v1` completo y válido** (300/300 pares, todos consistentes con el código final): `full` 9/60 (15 %), `no_rag` 9/60, `no_critic` 4/60, línea base A 5/60; la B se autoevalúa correcta en 55/60 y el kernel confirma 11. Ninguna diferencia significativa tras Bonferroni; la variación entre corridas es del tamaño de los efectos (mismo primer intento: 7 vs 4 problemas, 2 en común). Tablas en `docs/eval_report.md` y `docs/final_report.md` §6.3.
- **Informe final v0.3** (`docs/final_report.md`): resumen, discusión, limitaciones y conclusión escritos con los resultados reales; Apéndice E con los 7 defectos encontrados durante el experimento; 71 decisiones registradas.
- **Índice ANN** del Mathlib completo validado con consultas reales: mismas métricas que la búsqueda exacta, 60× más rápido. La demo responde en ~0.5 s sobre las 278 160 declaraciones.
- **Defectos corregidos esta noche** (con test): contabilidad perdida con salidas inválidas (#61), enrutamiento caro de OpenRouter (#62, #64), sesgo por reintentos ocultos en 15 pares (#63), esquema de las líneas base (#65, que invalidaba la A: 58/60 pruebas vacías).
- **Gasto**: la key usó US$1.58 de US$2.00 (≈ US$0.9 perdidos por defectos de los días anteriores, ya corregidos). No se gastó en `eval-v1-full`.
- Notebook de resultados ejecutado, docs de instalación/uso/arquitectura/interfaces al día, scripts de publicación en HF listos (dataset y Space, en `--dry-run`), 77 tests en verde.