| # Plan de acción — Módulo de Embeddings/RAG de RagSolver |
|
|
| > Documento de diseño y plan de ejecución para el agente implementador. |
| > Proyecto: *Sistema multiagente de IA generativa para resolución de problemas complejos mediante cadenas de razonamiento y verificación formal de teoremas* (UPTC, curso de IA, 13 semanas). |
| > Fecha: 2026-09-18. Idioma de trabajo interno: español; código, prompts, metadatos y reporte final en inglés. |
|
|
| --- |
|
|
| ## 0. Cómo usar este documento |
|
|
| - Es un plan **por fases, listo para ejecutar**. Cada fase tiene: objetivo, entradas, tareas numeradas, artefactos de salida, criterios de aceptación medibles y plan B. No pases a la siguiente fase sin cumplir los criterios de aceptación. |
| - **No sobre-ingeniería.** Regla: si algo no está en este plan y no lo pide un criterio de aceptación, no se construye. Nada de abstracciones con una sola implementación, ni frameworks de retriever encima de la base vectorial, ni fábricas de config. |
| - Cada decisión que te desvíe de este plan se registra en `docs/DECISIONS.md` (fecha, decisión, alternativa descartada, motivo, evidencia). |
| - Todas las versiones (Lean, Mathlib, modelos, parser, índice) se fijan en un único `configs/versions.yaml` y se copian a cada registro JSONL de ejecución (RNF-2). |
| - El código del módulo RAG vive en `src/ragsolver/rag/`. Nada del RAG debe importar nada de los agentes; los agentes importan el RAG. |
|
|
| --- |
|
|
| ## 1. Análisis del proyecto y dónde encaja el RAG |
|
|
| ### 1.1 Objetivo del sistema completo (según la propuesta) |
|
|
| Resolver problemas matemáticos de nivel olimpiada con un grafo de agentes (Planificador → Recuperador → Generador → Autoformalizador → Verificador → Crítico) donde **la única fuente de verdad es el kernel de Lean 4 + Mathlib**. Se evalúa con 30–60 problemas de miniF2F/PutnamBench (20–30 si es individual), con 5 configuraciones de ablación, una de ellas *sin RAG*. |
|
|
| ### 1.2 Qué exige la propuesta al módulo de RAG |
|
|
| | Requisito | Texto de la propuesta | Implicación de diseño | |
| |---|---|---| |
| | RF-2 | Representar subobjetivos y corpus de Mathlib con embeddings; recuperar los *k* lemas más similares antes de cada boceto | Índice sobre Mathlib; la consulta principal es un **subobjetivo** | |
| | Contrato 6.3 | Entrada: subobjetivo. Salida: lemas candidatos **con firma Lean** | La salida del recuperador debe incluir `decl_name` + `signature` + módulo | |
| | RNF-2 | Reproducibilidad: fijar versión de Mathlib, del modelo de embeddings, del LLM | Pinning en `versions.yaml`; misma versión de Mathlib en índice y verificador | |
| | RNF-3 | ≤ 20 llamadas LLM por problema resuelto | El retrieval debe costar **0 llamadas LLM en tiempo de ejecución**; todo enriquecimiento con LLM ocurre en indexación | |
| | RNF-4 | Cada agente es un módulo con contrato JSON Schema | `RetrievalRequest`/`RetrievalResult` tipados (Pydantic → JSON Schema) | |
| | RNF-5 / RF-7 | Registro JSON Lines por problema, agente e intento | Cada búsqueda emite un evento de traza con hits, scores y versiones | |
| | Riesgo §11 | "Recuperación irrelevante o ruidosa: validar la calidad con un conjunto de referencia lema-consulta **antes** de integrarlo" | Fase de evaluación del retriever aislado, con umbrales, antes de la integración | |
| | Métrica 8.3 | "Contribución del RAG": diferencia sistema completo vs. sin RAG | Flag de ablación `rag.enabled` | |
| | Alcance 5.3 | Álgebra, teoría de números, combinatoria elemental; excluye geometría sintética compleja | El corpus informal puede contener geometría (los PDFs la traen), pero el filtro `math_area` permite priorizar áreas del alcance | |
|
|
| ### 1.3 Lo que el usuario añade al alcance del RAG (este encargo) |
|
|
| 1. Además de Mathlib, el RAG debe ingerir **documentos informales** (papers, colecciones de problemas resueltos, libros) con matemática avanzada, **OCR correcto para fórmulas** y **figuras relacionadas con su texto**. |
| 2. La recuperación debe permitir **citar los documentos que ayudaron a la solución** → esquema de metadatos y objeto de citación. |
| 3. Decidir stack, base vectorial (¿FAISS?) y arquitectura completa. |
|
|
| ### 1.4 Ejes temáticos relacionados (para el marco teórico del informe) |
|
|
| - Document AI: análisis de layout, reconocimiento de fórmulas (LaTeX), orden de lectura, VLMs para OCR (MinerU 2.5, PaddleOCR-VL, GLM-OCR, olmOCR; benchmark OmniDocBench). |
| - RAG multimodal: figuras → descripciones textuales (text-summary multimodal RAG) y recuperación visual por late-interaction (ColPali/ColQwen, jina-embeddings-v4). |
| - Recuperación híbrida (denso + BM25), fusión RRF, reranking con cross-encoders, *Contextual Retrieval* (Anthropic). |
| - Premise selection para asistentes de prueba: LeanDojo/ReProver, LeanSearch v2, Lean Finder, TheoremGraph (puente informal↔formal). |
| - Evaluación de IR: Recall@k, nDCG@k, MRR; contaminación de benchmarks; licenciamiento de datos. |
| - Reproducibilidad: pinning de versiones, índices publicados en Hugging Face Hub. |
|
|
| --- |
|
|
| ## 2. Alcance del módulo RAG |
|
|
| ### 2.1 Dos corpus, dos consumidores |
|
|
| | Corpus | Contenido | Unidad de recuperación | Quién lo consume | Para qué | |
| |---|---|---|---|---| |
| | **A — Formal (Mathlib)** | 310 579 declaraciones de Mathlib v4.28.0-rc1 con descripción informal generada por LLM (corpus publicado por LeanSearch v2, Apache 2.0) | 1 declaración (nombre, firma, tipo, módulo, descripción informal) | GENERATE, FORMALIZE, CRITIQUE (re-recuperación por "lema faltante") | Anclar el boceto y la formalización en lemas reales; reducir alucinación de nombres | |
| | **B — Informal (PDFs)** | Colecciones de problemas resueltos (p. ej. *problemas resueltos olimpiadas.pdf*, 100 problemas, español), papers, apuntes | *Problem card* (enunciado + solución + figuras + resumen de técnica); sección de paper; figura descrita | PLAN (ejemplares análogos para descomponer), GENERATE (estrategias y pasos de prueba) | Razonamiento analógico: "problemas similares resueltos y la técnica que usaron" | |
|
|
| ### 2.2 Fuera de alcance |
|
|
| - Entrenar o hacer fine-tuning de embeddings (excluido por la propuesta; además LeanSearch v2 demuestra que un embedder general + reranker supera a los fine-tuned). |
| - GraphRAG / base de grafos: la dependencia entre declaraciones es una columna `dependencies`, no un grafo aparte. |
| - Un buscador visual (ColPali) en la primera entrega: se deja como Fase 7 con disparador medible (ver §11.4). |
| - OCR de manuscritos. |
|
|
| --- |
|
|
| ## 3. Diagnóstico del corpus de ejemplo (`problemas resueltos olimpiadas.pdf`) |
|
|
| Analizado con PyMuPDF (77 páginas, Word 2000 + Acrobat Distiller 4, 2002, autores Moreno Núñez & Tellechea Armenta, Universidad de Sonora; español). |
|
|
| | Hallazgo | Evidencia | Consecuencia para el pipeline | |
| |---|---|---| |
| | Es PDF **nacido digital, no escaneado**, pero la capa de texto es **matemáticamente corrupta** | `2^2001 + 3^2001` se extrae como `22001 + 32001`; `n²` como `n2`; `C(200,100)` como `C 200 100`; las fracciones y sumatorias del Equation Editor salen como tokens desordenados (`1997 1996 2 ... 6 4 2 )1 2 ( ...`) | **Nunca usar la capa de texto para fórmulas.** Todo se procesa desde la imagen renderizada de la página. La capa de texto sólo sirve como cross-check de texto plano. | |
| | Figuras = **dibujos vectoriales** (441 trazos) + 15 imágenes raster | Diagramas geométricos (circunferencias, triángulos inscritos), poliominós (problema 37), etiquetas de puntos (`A B C O D P`) como texto suelto al final de página | Detección de figuras por layout **y** por clustering de trazos vectoriales (PyMuPDF `cluster_drawings`) como red de seguridad; las etiquetas deben quedar dentro del recorte (padding). | |
| | Las figuras **no tienen pie de figura**; el texto dice "en la figura", "como muestra el dibujo" | Problemas 8, 16, 17, 22, 24, 99; solución 37 | La asociación figura↔problema es por **orden de lectura + número de ítem**, no por caption. La descripción de la figura debe generarse **con el enunciado como contexto**. | |
| | Estructura: Índice → Introducción → Problemario (1–100, pp. 8–22) → Soluciones (1–100, pp. 23–75) → Bibliografía | Índice en página 1 | Emparejar problema *N* con solución *N* entre secciones distintas. | |
| | Idioma español; consultas del sistema en inglés (miniF2F) | — | Embedder **multilingüe** obligatorio; enriquecimientos (resúmenes, descripciones de figuras, técnicas) se generan en inglés. | |
| | Contenido: mucha geometría, además de TN, álgebra y combinatoria | — | Etiquetar `math_area` por card para poder filtrar/priorizar según alcance. | |
|
|
| Estos hallazgos son generalizables a cualquier paper/libro de matemáticas: fórmulas como objetos gráficos o LaTeX renderizado, figuras vectoriales, referencias implícitas a figuras. |
|
|
| --- |
|
|
| ## 4. Estado del arte consultado y decisiones |
|
|
| | Tema | Qué hacen los proyectos de referencia | Decisión para RagSolver | Por qué | |
| |---|---|---|---| |
| | Retrieval sobre Mathlib | **LeanSearch v2** (2026): corpus de declaraciones informalizadas jerárquicamente (Qwen3-32B), embedder **Qwen3-Embedding-8B** sin fine-tuning, top-50 → **Qwen3-Reranker-8B**; nDCG@10 = 0.62 vs 0.53 del siguiente sistema; publica corpus JSONL (311k, 332 MB, Apache 2.0) y benchmarks MathlibQR/MathlibMPR. **Lean Finder** (2025): fine-tune de DeepSeek-Prover 7B con 1.4M pares sintéticos; Recall@1 64.2% vs 49.2%. **TheoremGraph** (2026): dataset informal↔formal + embeddings Qwen3 + métricas de grafo. | Reusar el **corpus JSONL de LeanSearch v2**; misma familia de modelos a escala reducida: **Qwen3-Embedding-0.6B** (4B si hay GPU) + **Qwen3-Reranker-0.6B/4B**; evaluar en MathlibQR contra sus números publicados. | Evita ~310k llamadas LLM de informalización; misma receta que el SOTA; permite comparación directa. | |
| | Parsing de PDF científico | OmniDocBench v1.6: PaddleOCR-VL-1.6 96.3, MinerU2.5 (1.2B) en el top; Gemini 3 Pro 90.3; olmOCR 85.7. LlamaIndex: el benchmark está saturado, los fallos restantes son fórmulas, gráficos, orden de lectura. Paper *When Good OCR Is Not Enough* (2026): fórmulas, estructura/orden de lectura y pérdida de vínculos figura↔texto son los errores de mayor impacto en RAG. | **MinerU ≥ 2.5 (backend VLM, forzando modo imagen)** como parser primario; **PaddleOCR-VL** como alternativa si MinerU falla en instalación/calidad; **Docling** sólo como último recurso. | MinerU da Markdown + `content_list.json` con bloques tipados, LaTeX, recortes de figuras, bbox y página: exactamente lo que necesita el esquema de metadatos. | |
| | Figuras en RAG | Patrón "multimodal RAG por resúmenes" (LangChain multi-vector, LlamaIndex): describir cada figura con un VLM, indexar la descripción, adjuntar la imagen al generar. ColPali/ColQwen3/jina-v4: recuperación visual de páginas sin OCR (ViDoRe ~84–90). | **Fase 1–2: descripciones de figuras con VLM contextualizadas por el enunciado** + imagen disponible para el generador. **Fase 7 (opcional, con disparador):** canal visual multivector. | Resuelve el problema "la figura no se relaciona con el texto" con vectores simples; ColPali añade GPU, multivector y complejidad sin evidencia aún de que haga falta. | |
| | Chunking + contexto | **Contextual Retrieval** (Anthropic): prefijo de 50–100 tokens de contexto generado por LLM antes de embeber e indexar en BM25; −49% fallos de recuperación, −67% con reranking (5.7%→1.9% en top-20). | Contextual retrieval **sólo en el corpus informal** (Mathlib ya trae descripción informal = contexto). Chunk estructural: *problem card* como unidad, con hijos (pasos, figuras). | Gran ganancia medida a bajo coste (indexación, con prompt caching). | |
| | Búsqueda | Híbrido denso + BM25 con fusión RRF, reranker cross-encoder (estándar en LeanSearch v2, Anthropic, Qdrant/LanceDB docs). | Denso (Qwen3-Embedding) + FTS/BM25 nativo de LanceDB → RRF → rerank top-50 → top-k. | BM25 captura identificadores exactos (`Nat.Prime.two_le`, tokens LaTeX); denso captura semántica; el reranker corrige el orden. | |
| | Base vectorial | FAISS = sólo índice ANN (sin metadatos, sin BM25, sin filtros nativos, sin persistencia gestionada). Chroma: filtros pero sin BM25 real. Qdrant: completo pero servidor (Docker). LanceDB: embebido, híbrido nativo, filtros SQL, multivector, formato en disco. | **LanceDB** (ver §9.2). | Menos código, cero infraestructura, publicable como carpeta en HF Hub, funciona en un Space de Gradio. | |
| | Interacción con Lean | Kimina Lean Server (REPL paralelo + caché LRU), LeanInteract (`lean-interact`, Lean 4.8–4.32), PyPantograph. | `lean-interact` para el verificador (simple); Kimina si se necesita paralelismo en experimentos. | Fuera del RAG, pero fija la restricción: **la versión de Mathlib del verificador = la del índice**. | |
| | Conjunto de evaluación | **miniF2F-v2** (2025): corrige discrepancias formal/informal en >50% de problemas y publica pruebas verificadas completas (`roozbeh-yz/miniF2F_v2`). | Usar miniF2F-v2 para el conjunto de 30–60 problemas y para extraer **premisas gold** (lemas usados en las pruebas verificadas). | Evita el riesgo de mal-formalización del §11 y da un gold set de retrieval gratis. | |
| | Corpus informal extra | NuminaMath-1.5 (~900k problemas de competencia con solución, Apache 2.0), NuminaMath-LEAN (100k formalizados). | Opcional (Fase 7) con **control de contaminación** obligatorio contra el conjunto de prueba. | Sin OCR, texto nativo con LaTeX; pero riesgo de fuga de problemas de miniF2F. | |
|
|
| --- |
|
|
| ## 5. Arquitectura completa del proyecto |
|
|
| ### 5.1 Componentes |
|
|
| ```mermaid |
| flowchart LR |
| subgraph Orq["Orquestador (LangGraph, checkpoints)"] |
| P[PLAN] --> R[RETRIEVE] --> G[GENERATE] --> F[FORMALIZE] --> V[VERIFY] |
| V -- ok --> D[DONE] |
| V -- error --> C[CRITIQUE] |
| C -- retry --> G |
| C -- replan --> P |
| C -- exhausted --> X[FAIL] |
| end |
| subgraph RAG["Módulo RAG (src/ragsolver/rag)"] |
| IDX[(LanceDB\n tablas: mathlib, informal, figures)] |
| RET[Retriever\n híbrido + rerank + citas] |
| ING1[Ingesta Mathlib] |
| ING2[Ingesta PDFs\n MinerU + VLM] |
| ING1 --> IDX |
| ING2 --> IDX |
| IDX --> RET |
| end |
| subgraph Lean["Verificador"] |
| REPL[lean-interact / REPL\n Lean 4 + Mathlib v4.28.0-rc1] |
| end |
| R --> RET |
| C --> RET |
| P -. ejemplares .-> RET |
| V --> REPL |
| Orq --> LOG[(JSONL trace)] |
| RET --> LOG |
| EVAL[Harness de evaluación\n ablaciones + métricas IR] --> Orq |
| EVAL --> RET |
| DEMO[Space Gradio] --> Orq |
| DEMO --> RET |
| ``` |
|
|
| - **Agentes** (Rol A): Planificador, Generador, Autoformalizador, Crítico. Cada uno es una función pura `state -> state_delta` con contrato Pydantic. |
| - **Verificador** (Rol B): cliente Lean; devuelve veredicto + traza; determinista. |
| - **Módulo RAG** (Rol B, este plan): ingesta (offline), índice, servicio de recuperación (online, 0 llamadas LLM), citación, evaluación. |
| - **Orquestador**: LangGraph `StateGraph` con checkpointer SQLite; el estado lleva `evidence[]` (citas acumuladas) y `retrieval_trace[]`. |
| - **Registro**: un archivo JSONL por corrida; un evento por (problema, agente, intento). |
| - **Evaluación**: script que ejecuta las 5 configuraciones sobre el conjunto dev/test y calcula pass@k, costes, contribución del RAG, precisión de uso de lemas, taxonomía de errores. |
| - **Demo**: Gradio en HF Space: pestaña "buscar" (muestra hits con citas, firma Lean y recorte de figura) y pestaña "resolver". |
|
|
| ### 5.2 Layout del repositorio (compatible con §10.2 de la propuesta) |
|
|
| ``` |
| ragsolver/ |
| ├── README.md # arquitectura + cómo ejecutar |
| ├── pyproject.toml # dependencias fijadas |
| ├── configs/ |
| │ ├── versions.yaml # lean, mathlib tag, modelos, parser, index_version |
| │ ├── retrieval.yaml # k, candidatos, pesos RRF, flags de ablación |
| │ └── ingest.yaml # dpi, tiers de MinerU, prompts de enriquecimiento |
| ├── src/ragsolver/ |
| │ ├── agents/ # planner, generator, formalizer, critic |
| │ ├── orchestrator/ # grafo LangGraph + esquema de estado |
| │ ├── lean/ # cliente REPL, plantilla de proyecto Lean |
| │ ├── rag/ |
| │ │ ├── schema.py # modelos Pydantic: Document, Chunk, Figure, Citation, RetrievalRequest/Result |
| │ │ ├── ingest_mathlib.py # corpus A |
| │ │ ├── ingest_pdf.py # corpus B: render, MinerU, estructura, figuras |
| │ │ ├── enrich.py # VLM: figuras, QA de fórmulas, resúmenes contextuales |
| │ │ ├── embed.py # Qwen3-Embedding (local o API) |
| │ │ ├── index.py # LanceDB: tablas, FTS, ANN |
| │ │ ├── retrieve.py # búsqueda híbrida, RRF, rerank, filtros, citas |
| │ │ └── evaluate.py # Recall@k, nDCG@k, MRR sobre gold sets |
| │ └── logging/ # escritor JSONL |
| ├── lean_project/ # Lean 4 + Mathlib (tag fijado) |
| ├── data/ |
| │ ├── raw/ # PDFs originales (no se publican si la licencia no lo permite) |
| │ ├── parsed/<doc_id>/ # páginas PNG, salida MinerU, recortes de figuras |
| │ ├── corpus/ # informal.jsonl, mathlib.jsonl (chunks normalizados) |
| │ ├── index/lancedb/ # tablas Lance (se publican en HF Dataset) |
| │ └── eval/ # MathlibQR, MathlibMPR, gold informal, gold figuras, premisas miniF2F-v2 |
| ├── notebooks/ # evaluación y figuras del informe |
| ├── demo/ # app Gradio |
| ├── docs/ # PLAN_RAG.md (este), DECISIONS.md, architecture.md, interfaces.md, reproduce.md |
| └── tests/ |
| ``` |
|
|
| ### 5.3 Flujo de ejecución por problema (secuencia) |
|
|
| 1. `PLAN` recibe el enunciado. **Antes** de llamar al LLM, el orquestador ejecuta una recuperación de ejemplares en el corpus informal con el enunciado como consulta (0 llamadas LLM) y los inyecta al prompt del Planificador. El Planificador devuelve subobjetivos, cada uno con `statement_nl`, `formal_hint`, `search_queries[2–3]`, `math_area`. |
| 2. `RETRIEVE` (por subobjetivo): recuperación híbrida en Mathlib con las `search_queries` + `statement_nl`; fusión RRF; rerank contra `statement_nl`; top-k lemas con firma; ejemplares informales top-3 opcionales. Registra evento JSONL. Coste LLM: 0. |
| 3. `GENERATE`: prompt = subobjetivo + lemas (nombre, firma, descripción, módulo) + ejemplares (enunciado, idea clave, cita) + descripciones de figuras (imagen opcional). Devuelve boceto y `used_citations[]`. |
| 4. `FORMALIZE`: prompt = boceto + lemas con firma exacta. Devuelve Lean. |
| 5. `VERIFY`: ejecuta Lean. Éxito → `DONE`: se marcan como **verificadas** las citas de Mathlib cuyo `decl_name` aparece en la prueba aceptada. |
| 6. `CRITIQUE`: clasifica el error; si es `lema faltante`/`unknown identifier`, dispara una re-recuperación con el mensaje de error y el goal state como consulta (0 llamadas LLM extra) y vuelve a `GENERATE`. |
| 7. Al terminar, `SolutionReport` incluye `citations[]` (verificadas, usadas en boceto, consultadas) con localizadores. |
|
|
| --- |
|
|
| ## 6. Arquitectura del módulo RAG |
|
|
| ### 6.1 Pipeline de ingesta — Corpus A (Mathlib) |
|
|
| ``` |
| HF: FrenzyMath/lsv2-mathlib-v4.28.0-rc1-jsonl |
| → normalizar a esquema Chunk (§7) → filtrar internos/instances (config) |
| → texto a embeber = informal_name + informal_description + signature |
| → Qwen3-Embedding → LanceDB tabla `mathlib` (+ FTS sobre decl_name, informal_name, informal_description, signature) |
| → evaluar en MathlibQR / MathlibMPR |
| ``` |
|
|
| ### 6.2 Pipeline de ingesta — Corpus B (PDFs) |
|
|
| ``` |
| PDF → inventario (sha256, páginas, ¿capa de texto fiable?) |
| → render páginas PNG 200 dpi (PyMuPDF), cache |
| → MinerU backend VLM, modo imagen forzado → markdown + content_list.json (bloques: text/title/equation/image/table + bbox + page_idx + LaTeX + rutas de recorte) |
| → red de seguridad de figuras vectoriales (PyMuPDF cluster_drawings) → unión de bboxes |
| → parser estructural: secciones, ítems numerados, emparejar problema N ↔ solución N, adjuntar figuras/ecuaciones al ítem (orden de lectura + referencias "figura/dibujo/fig.") |
| → enriquecimiento VLM/LLM (offline, en inglés): |
| a) descripción estructurada de cada figura, con el enunciado como contexto |
| b) QA de fórmulas: página + lista LaTeX extraída → LaTeX corregido |
| c) resumen contextual + math_area + techniques + theorems_used + difficulty por problem card |
| → chunks: problem_card (padre), solution_step (hijos si > ~1 500 tokens), figure (hijo), paper_section |
| → texto a embeber = context_summary + "\n\n" + content_md |
| → Qwen3-Embedding → LanceDB tabla `informal` (+ FTS sobre text, keywords, theorems_used) y tabla `figures` |
| → QA gates (§10, Fase 2) |
| ``` |
|
|
| Reglas duras del OCR: |
| 1. Fórmulas siempre desde imagen; la capa de texto del PDF nunca es fuente de LaTeX. |
| 2. Toda figura se guarda como recorte PNG con padding (etiquetas incluidas), con `bbox` normalizado y `page`. |
| 3. Toda figura tiene descripción generada **con el enunciado/solución al que pertenece** como contexto; sin contexto, la descripción de "un círculo con puntos A, B, C" no sirve para recuperar nada. |
| 4. Cada ítem numerado conserva `page_start/page_end/bbox` para poder citar "Problema 22, p. 11". |
| 5. Ingesta idempotente por `sha256` del documento: re-ejecutar no reprocesa lo ya hecho. |
|
|
| ### 6.3 Servicio de recuperación (online) |
|
|
| ``` |
| RetrievalRequest |
| → plantilla de consulta con instrucción (Qwen3-Embedding usa "Instruct: … \nQuery: …") |
| → por cada consulta: denso top-50 + BM25 top-50 (prefiltro SQL por corpus/math_area/doc_id) |
| → fusión RRF de todas las listas |
| → reranker (Qwen3-Reranker) sobre los 50 mejores contra statement_nl |
| → dedupe por decl_name / parent_id; máx. 3 por módulo (opcional) |
| → top-k → Citation[] + RetrievalResult + evento JSONL |
| ``` |
|
|
| Modos de consulta soportados (misma función, distinta plantilla): |
| - `nl`: subobjetivo en lenguaje natural (principal). |
| - `formal`: goal state / enunciado Lean (desde el Crítico o el Autoformalizador). |
| - `error`: mensaje de error Lean (`unknown identifier 'Nat.foo'`) → búsqueda exacta FTS del identificador + denso sobre el goal. |
| - `exemplar`: enunciado completo del problema → corpus informal. |
|
|
| ### 6.4 Citación |
|
|
| - El retriever **siempre** devuelve `Citation` por hit; el orquestador acumula `evidence[]` en el estado. |
| - Tres niveles de "ayudó a la solución", de más a menos fuerte: |
| 1. `used_in_proof = true`: el `decl_name` aparece en el código Lean **aceptado por el kernel** (verificación mecánica, sin LLM). |
| 2. `used_in_sketch = true`: el Generador declaró la cita en `used_citations[]` (salida estructurada; sin llamada extra). |
| 3. `consulted`: fue recuperada e inyectada al prompt. |
| - El informe final lista las tres categorías por separado; la métrica "precisión de uso de lemas" = verificadas / recuperadas. |
|
|
| --- |
|
|
| ## 7. Esquema de metadatos |
|
|
| Tipos: `str`, `int`, `float`, `bool`, `list[...]`, `vec[d]`. Campos marcados **(cita)** son los que construyen el localizador de la referencia. |
|
|
| ### 7.1 `documents` (uno por fuente) |
|
|
| | Campo | Tipo | Descripción | |
| |---|---|---| |
| | `doc_id` | str | Determinista: `sha256(bytes)[:12]`; para Mathlib: `mathlib-v4.28.0-rc1` | |
| | `title`, `authors`, `year` | str, list[str], int | **(cita)** | |
| | `source_type` | str | `olympiad_collection` \| `paper` \| `textbook` \| `notes` \| `mathlib` | |
| | `language` | str | ISO 639-1 (`es`, `en`) | |
| | `file_path`, `sha256`, `n_pages` | str, str, int | Origen y huella | |
| | `url`, `license`, `redistributable` | str, str, bool | Si `false`, no se publica en HF (sólo metadatos) | |
| | `parser`, `parser_version`, `parser_tier` | str | `mineru`, `2.5.x`, `standard` | |
| | `text_layer_reliable` | bool | Resultado del inventario (§10 Fase 2, tarea 1) | |
| | `ingested_at`, `index_version` | str | ISO 8601; versión del índice | |
|
|
| ### 7.2 `chunks` (núcleo común; una tabla LanceDB por corpus) |
|
|
| | Campo | Tipo | Descripción | |
| |---|---|---| |
| | `chunk_id` | str | `{doc_id}:{unit_type}:{ordinal}` (determinista, estable entre re-ingestas) | |
| | `doc_id` | str | FK a `documents` | |
| | `corpus` | str | `mathlib` \| `informal` | |
| | `unit_type` | str | `mathlib_decl` \| `problem_card` \| `solution_step` \| `figure` \| `paper_section` \| `theorem` | |
| | `parent_id`, `children_ids` | str, list[str] | Jerarquía (card → pasos/figuras) | |
| | `order` | int | Posición en orden de lectura del documento | |
| | `text` | str | **Lo que se embebe y se indexa en BM25** = `context_summary` + contenido | |
| | `content_md` | str | Contenido original (Markdown + LaTeX), idioma fuente | |
| | `context_summary` | str | Contextual retrieval (inglés, 50–100 tokens); vacío en Mathlib | |
| | `page_start`, `page_end` | int | **(cita)** 1-based | |
| | `bboxes` | list[list[float]] | **(cita)** `[page, x0, y0, x1, y1]` normalizados 0–1 | |
| | `section_path` | list[str] | **(cita)** p. ej. `["Soluciones", "22"]` | |
| | `item_number` | int | Número de problema/teorema si aplica **(cita)** | |
| | `language` | str | Idioma del `content_md` | |
| | `math_area` | list[str] | `algebra` \| `number_theory` \| `combinatorics` \| `geometry` \| `inequalities` \| `analysis` \| … | |
| | `techniques` | list[str] | Vocabulario controlado (`induction`, `pigeonhole`, `invariant`, `vieta_jumping`, `am_gm`, `angle_chasing`, …) | |
| | `theorems_used` | list[str] | Nombres informales en inglés (`Pythagorean theorem`, `inscribed angle theorem`) | |
| | `mathlib_candidates` | list[str] | (Fase 7) decl_names sugeridos para `theorems_used` | |
| | `difficulty` | int | 1–5 (LLM; sólo informal) | |
| | `keywords` | list[str] | Para BM25 | |
| | `figure_ids` | list[str] | Figuras adjuntas | |
| | `refs_to` | list[str] | chunk_ids referenciados explícitamente | |
| | `embedding` | vec[d] | float16; `d` según modelo | |
| | `embedding_model`, `embedding_dim`, `index_version` | str, int, str | Reproducibilidad | |
| | `content_sha` | str | Para detectar cambios | |
|
|
| ### 7.3 Extensión `figure` (tabla `figures`, y también como chunk con `unit_type=figure`) |
| |
| | Campo | Tipo | Descripción | |
| |---|---|---| |
| | `figure_id` | str | `{doc_id}:fig:{page}:{n}` **(cita)** | |
| | `image_path`, `image_sha` | str | Recorte PNG con padding | |
| | `page`, `bbox` | int, list[float] | **(cita)** | |
| | `detected_by` | str | `layout` \| `vector_cluster` \| `raster` \| `both` | |
| | `caption` | str | Pie original si existe (a menudo vacío) | |
| | `description` | str | Descripción estructurada en inglés (VLM), con el enunciado como contexto | |
| | `labels` | list[str] | Etiquetas de puntos/objetos (`A`, `B`, `O`, `tipo uno`) | |
| | `objects`, `relations`, `given_values` | list[str] | `circle`, `triangle ABC inscribed`, `OD ⟂ BC`, `angle DCP = 15°` | |
| | `figure_type` | str | `geometric_diagram` \| `grid` \| `plot` \| `table_image` \| `other` | |
| | `linked_chunk_ids` | list[str] | Problem card / solución a los que pertenece | |
| | `description_model`, `description_version` | str | Reproducibilidad | |
|
|
| ### 7.4 Extensión `mathlib_decl` |
| |
| | Campo | Tipo | Descripción | |
| |---|---|---| |
| | `decl_name` | str | Nombre totalmente cualificado **(cita)** | |
| | `decl_names_alt` | list[str] | Alias (el corpus trae `name` como lista) | |
| | `module_path` | str | `Mathlib.NumberTheory.Divisors` **(cita)** | |
| | `kind` | str | `theorem` \| `lemma` \| `definition` \| `instance` \| `structure` \| `class` \| `inductive` | |
| | `signature`, `type`, `value` | str | Firma formal (lo que exige el contrato 6.3), tipo, cuerpo si definición | |
| | `informal_name`, `informal_description` | str | Del corpus LeanSearch v2 | |
| | `docstring` | str | Si se extrae del fuente (opcional) | |
| | `dependencies` | list[str] | Declaraciones usadas (opcional; Fase 7) | |
| | `mathlib_tag`, `lean_version` | str | `v4.28.0-rc1`, `4.28.0-rc1` | |
| | `docs_url` | str | `https://leanprover-community.github.io/mathlib4_docs/<module/path>.html#<decl_name>` **(cita)** | |
|
|
| ### 7.5 Objeto `Citation` (salida del retriever; se persiste en la traza y en el informe) |
|
|
| | Campo | Tipo | Descripción | |
| |---|---|---| |
| | `citation_id` | str | `M1`, `M2`… (Mathlib) / `I1`, `I2`… (informal) dentro de un problema | |
| | `chunk_id`, `corpus`, `unit_type` | str | Referencia al índice | |
| | `label` | str | Legible: `Nat.Prime.two_le — Mathlib.Data.Nat.Prime.Defs` / `Moreno & Tellechea (2002), Problema 22, p. 11, fig. 22:1` | |
| | `locator` | obj | Mathlib: `{decl_name, module_path, docs_url}`; informal: `{doc_id, page_start, page_end, bboxes, item_number, figure_ids}` | |
| | `scores` | obj | `{dense, sparse, fused, rerank}` | |
| | `retrieved_for` | obj | `{problem_id, subgoal_id, attempt, agent, query_mode}` | |
| | `used_in_proof`, `used_in_sketch` | bool | Ver §6.4 | |
| | `snippet` | str | Primeras ~300 chars del `content_md` para el informe | |
|
|
| ### 7.6 Evento de traza JSONL (RNF-5) |
|
|
| Un registro por búsqueda: `run_id, problem_id, subgoal_id, attempt, agent="retriever", ts, latency_ms, llm_calls=0, tokens=0, request (RetrievalRequest completo), n_candidates, hits[{chunk_id, rank, scores}], versions{embedding_model, reranker_model, index_version, mathlib_tag}`. |
|
|
| --- |
|
|
| ## 8. Contratos del recuperador (JSON Schema vía Pydantic) |
|
|
| ### 8.1 `RetrievalRequest` |
|
|
| | Campo | Tipo | Default | Descripción | |
| |---|---|---|---| |
| | `queries` | list[str] | — | 1–4 consultas (subobjetivo + `search_queries` del Planificador) | |
| | `rerank_against` | str | `queries[0]` | Texto de referencia para el reranker | |
| | `mode` | str | `nl` | `nl` \| `formal` \| `error` \| `exemplar` | |
| | `corpora` | list[str] | `["mathlib"]` | Subconjunto de `{mathlib, informal}` | |
| | `k` | int | 8 | Resultados finales por corpus | |
| | `n_candidates` | int | 50 | Candidatos por canal antes de fusionar | |
| | `filters` | obj | `{}` | `math_area`, `doc_ids`, `unit_types`, `kinds` | |
| | `rerank` | bool | true | Flag de ablación | |
| | `include_figures` | bool | true | Adjuntar figuras de los hits informales | |
| | `context` | obj | — | `{problem_id, subgoal_id, attempt, agent}` para la traza | |
|
|
| ### 8.2 `RetrievalResult` |
|
|
| | Campo | Tipo | Descripción | |
| |---|---|---| |
| | `hits` | list[Hit] | `Hit = {chunk_id, corpus, unit_type, rank, text, content_md, metadata (subconjunto §7), figures[{figure_id, image_path, description}], citation: Citation}` | |
| | `citations` | list[Citation] | Misma información, plana, para acumular en `evidence[]` | |
| | `trace` | obj | `{latency_ms, n_candidates, versions}` | |
|
|
| ### 8.3 Contratos de los otros agentes que tocan el RAG (mínimo) |
|
|
| - `PlannerOutput.subgoals[i]` añade: `search_queries: list[str] (2–3)`, `math_area: str`. |
| - `GeneratorOutput` añade: `used_citations: list[str]` (ids `M*`/`I*`). |
| - `CriticOutput` añade: `missing_identifiers: list[str]`, `re_retrieve: bool`. |
| - `SolutionReport` añade: `citations: list[Citation]` con `used_in_proof/used_in_sketch` resueltos. |
|
|
| --- |
|
|
| ## 9. Stack tecnológico |
|
|
| ### 9.1 Selección (fijar versiones exactas en `versions.yaml` al iniciar la Fase 0) |
|
|
| | Capa | Elección | Alternativa | Notas | |
| |---|---|---|---| |
| | Lenguaje / gestor | Python 3.11–3.12, `uv` | — | MinerU exige 3.10–3.14 | |
| | Orquestación | LangGraph (StateGraph + SqliteSaver) | CrewAI | Estado tipado y checkpoints, como pide la propuesta | |
| | Verificación | `lean-interact` sobre Lean 4 + Mathlib **v4.28.0-rc1** | Kimina Lean Server (paralelismo) | Misma tag que el corpus A | |
| | Parser PDF | **MinerU ≥ 2.5 / 4.x**, backend VLM, modo imagen | PaddleOCR-VL 1.6; Docling | GPU 8 GB para tier `standard`; CPU posible para corpus pequeños; en GPU AMD ver §9.4 | |
| | Render/inspección PDF | PyMuPDF | pdfplumber | Render, `cluster_drawings`, inventario | |
| | VLM de enriquecimiento | El mismo proveedor frontier que usan los agentes (Claude / Gemini / GPT, modelo con visión) | Qwen3-VL-8B local | Un solo proveedor y una sola clave | |
| | Embeddings | **Qwen3-Embedding-0.6B** (1024 d, multilingüe, instrucciones, MRL); **4B** si hay GPU ≥ 16 GB | API: `gemini-embedding` / `text-embedding-3-large` (~46 M tokens ≈ 6–7 USD para Mathlib) | Un solo modelo para ambos corpus; en GPU AMD ver §9.4 | |
| | Reranker | **Qwen3-Reranker-0.6B** (4B con GPU) | `bge-reranker-v2-m3`; Cohere Rerank (API) | Local, 0 llamadas LLM; en GPU AMD ver §9.4 | |
| | Base vectorial | **LanceDB** (embebida): vector + FTS/BM25 nativo + RRF + filtros SQL + multivector | Qdrant (si se quiere servidor/Docker) | Ver 9.2 | |
| | Métricas IR | `ranx` | función propia de 20 líneas | Recall@k, nDCG@k, MRR | |
| | Validación de contratos | Pydantic v2 (`model_json_schema()`) | — | RNF-4 | |
| | Publicación | HF Hub: Dataset (índice Lance + corpus JSONL + recortes), Space (Gradio) | — | `snapshot_download` en el Space | |
| | Tests | pytest, embedder/reranker mock | — | Un test por pieza de lógica no trivial | |
|
|
| ### 9.2 ¿Por qué no FAISS? |
|
|
| | Necesidad del proyecto | FAISS | Chroma | Qdrant | LanceDB | |
| |---|---|---|---|---| |
| | Filtrar por `corpus`, `math_area`, `doc_id` | No (hay que envolverlo) | Sí | Sí | Sí (SQL, prefiltro) | |
| | BM25/FTS híbrido | No | Parcial (sin ranking BM25 real) | Sí (sparse vectors) | Sí (nativo, `create_fts_index`) | |
| | Fusión + reranker integrados | No | No | Parcial | Sí (RRF/lineal/cross-encoder) | |
| | Metadatos y texto junto al vector | No (id → store aparte) | Sí | Sí | Sí (tabla Arrow) | |
| | Persistencia/versionado | Dump manual | Sí | Snapshots | Carpeta en disco, formato Lance | |
| | Sin servidor, funciona en un Space | Sí | Sí | Modo local limitado / Docker | Sí | |
| | Multivector (ColPali, Fase 7) | No | No | Sí | Sí | |
| | Código extra que habría que escribir | Store de metadatos + BM25 aparte + fusión + filtros | Fusión + BM25 aparte | Cliente + despliegue | Casi ninguno | |
|
|
| FAISS es un motor ANN, no una base de conocimiento. Para citar documentos hacen falta metadatos y filtros; para identificadores de Mathlib hace falta BM25. Con FAISS se acabaría re-implementando una base de datos alrededor. **Decisión: LanceDB.** Si el equipo prefiere un servicio con Docker y varios usuarios concurrentes, Qdrant es la segunda opción; el código del retriever debe quedar detrás de una única clase para que el cambio sea local. |
|
|
| ### 9.3 Perfiles de hardware |
|
|
| - **Perfil A (GPU local o Colab T4/L4):** MinerU tier `standard`, Qwen3-Embedding-0.6B/4B, Qwen3-Reranker-0.6B/4B locales. Embeber Mathlib (311k) con 0.6B ≈ 15–30 min en T4. |
| - **Perfil B (sin GPU):** MinerU en CPU o VLM por API para parsing de páginas (≈0.01–0.03 USD/página), embeddings por API, reranker `Qwen3-Reranker-0.6B` en CPU (≈5–10 s por 50 pares; aceptable) o Cohere Rerank. |
|
|
| ### 9.4 Nota: vectorización en GPU AMD (ROCm) |
|
|
| Si el embebido/reranking se corre en una GPU AMD en vez de NVIDIA, el cambio es de **instalación y entorno**, no de arquitectura ni de elección de modelos: Qwen3-Embedding, Qwen3-Reranker y MinerU siguen siendo la elección de §9.1; PyTorch resuelve `device="cuda"` igual sobre ROCm (es el mismo alias de dispositivo), así que el código de `rag/embed.py` no cambia. Lo que sí cambia: |
|
|
| 1. **Sistema operativo.** ROCm sólo tiene ruta de cómputo oficial en Linux nativo o en **WSL2** (este proyecto ya corre en WSL2, así que es la vía a seguir); no existe ruta de cómputo GPU oficial desde Windows nativo. Usar Windows 11 22H2+ (Windows 10 tiene reportes de fallo incluso en tarjetas soportadas) y el driver Adrenalin más reciente. |
| 2. **Sobre esta tarjeta (RDNA4, 16 GB).** El nombre "RX 9080 XT" no corresponde a ningún producto AMD lanzado según la información pública disponible (los rumores existentes hablan de 24–32 GB, no 16 GB); 16 GB sí coincide con la **RX 9070 XT** (`gfx1201`), que es real — se asume esa arquitectura abajo, pero conviene confirmar el gfx exacto con `rocminfo` en la Fase 0 (tarea 7) en vez de fiarse del nombre comercial. Si es efectivamente `gfx1201`/RDNA4, es buena noticia: tiene soporte **oficial** de ROCm desde la versión 7.2 (AMD la valida en su propio CI), sin necesidad del workaround `HSA_OVERRIDE_GFX_VERSION`, y ya está confirmado funcionando en WSL2 vía `librocdxg`. Instalar ROCm ≥ 7.2 (probar la rama 7.12/7.13 si la 7.2 da problemas en WSL2) + `librocdxg`. Si `rocminfo` revela un chip distinto o más antiguo, tratarlo como Perfil B (sin GPU) hasta comprobar su soporte. |
| 3. **Instalación de PyTorch.** Wheel de ROCm, no la de CUDA por defecto (`pip install torch --index-url https://download.pytorch.org/whl/rocm<version>`, o los wheels de `repo.radeon.com` si AMD los recomienda para esa tarjeta). `sentence-transformers` (usado para Qwen3-Embedding/Reranker) funciona igual sobre ese PyTorch, sin cambios de código. |
| 4. **Flash-Attention.** El paquete `flash-attn` que recomienda la ficha de Qwen3-Embedding es CUDA-only y normalmente no compila en ROCm. Cargar los modelos con la implementación de atención por defecto (`sdpa`, o sin forzar `attn_implementation="flash_attention_2"`); se pierde algo de velocidad, no correctitud. |
| 5. **MinerU es el componente de mayor riesgo en ROCm — y aquí más que en general.** Su matriz de soporte oficial sólo cubre NVIDIA y Apple Silicon; ROCm es "no garantizado, feedback de la comunidad bienvenido". La única validación comunitaria conocida (benchmark OmniDocBench v1.6 reproducido) es sobre `gfx1100` (RDNA3, ROCm 7.2) — **no** sobre `gfx1201`/RDNA4, la arquitectura de esta tarjeta: no hay ningún reporte público de MinerU corriendo sobre RDNA4 todavía. Por eso se verifica en la Fase 0 (tarea 7) antes de construir la Fase 2 sobre ese supuesto; si falla o rinde mal, usar directamente el Plan B ya previsto en la Fase 2 (parsing de página completa por VLM vía API) en vez de perseguir el ajuste fino de ROCm. |
| 6. **LanceDB no cambia nada:** el índice, el ANN y el BM25 corren en CPU sin importar el fabricante de la GPU. |
| 7. Los tamaños de modelo recomendados (0.6B por defecto, 4B con ≥16 GB de VRAM) siguen aplicando igual; con 16 GB esta tarjeta ya califica para **Qwen3-Embedding-4B** y **Qwen3-Reranker-4B** si se prefiere algo más de calidad de retrieval sobre el 0.6B por defecto. |
|
|
| --- |
|
|
| ## 10. Fases de ejecución |
|
|
| Estimaciones para el Rol B (Formal Methods & Retrieval Lead). Mapeo al cronograma de la propuesta: Fases 0–1 en semanas 3–4, Fase 2 en 5–6, Fase 3 en 7, Fase 4 en 8–9 (la propuesta fija el RAG para la semana 9), Fase 5 en 10–11, Fase 6 en 12. |
|
|
| ### Fase 0 — Cimientos (2–3 días) |
|
|
| **Objetivo:** repositorio, entorno, versiones fijadas, esquemas y traza, con un smoke test que corre de punta a punta con mocks. |
|
|
| Tareas |
| 1. Crear el layout de §5.2; `pyproject.toml` con dependencias fijadas; `uv lock`. |
| 2. `configs/versions.yaml`: `lean`, `mathlib_tag=v4.28.0-rc1`, `embedding_model`, `embedding_dim`, `reranker_model`, `parser`, `parser_version`, `vlm_model`, `llm_model`, `index_version` (semver del índice). |
| 3. `rag/schema.py`: modelos Pydantic de §7 y §8; exportar los JSON Schema a `docs/interfaces/`. |
| 4. Escritor JSONL con el evento de §7.6; test que valida un evento contra el esquema. |
| 5. Crear `lean_project/` con Mathlib `v4.28.0-rc1`; verificar un teorema trivial con `lean-interact`. (Compartido con el Verificador; aquí sólo importa fijar la tag). |
| 6. `docs/DECISIONS.md` con las decisiones de §4 y §9 ya registradas. |
| 7. **Si el equipo vectoriza en GPU AMD:** instalar PyTorch ROCm (§9.4) y correr un smoke test en la máquina real: (a) `rocminfo` para confirmar el gfx real de la tarjeta y registrarlo en `versions.yaml` (no fiarse del nombre comercial de la caja); (b) cargar el modelo de embeddings y codificar un texto de prueba con `device="cuda"`; (c) correr MinerU sobre 1 página del PDF de ejemplo. Si (c) falla o rinde mal, registrar la decisión en `docs/DECISIONS.md` y fijar desde ya el parser en modo Plan B (VLM por API) para la Fase 2, en vez de descubrirlo a mitad de la ingesta. |
|
|
| Salidas: repo ejecutable, `versions.yaml`, esquemas JSON, test verde. |
| Aceptación: `pytest` verde; `lean-interact` verifica `example : 1 + 1 = 2 := rfl` con la tag fijada; si aplica GPU AMD, el smoke test de la tarea 7 queda documentado (éxito o fallback decidido). |
|
|
| ### Fase 1 — Corpus A: índice de Mathlib (3–4 días) |
|
|
| **Objetivo:** tabla `mathlib` en LanceDB con búsqueda híbrida y evaluación cuantitativa aislada, como exige el riesgo §11 de la propuesta. |
|
|
| Tareas |
| 1. Descargar `FrenzyMath/lsv2-mathlib-v4.28.0-rc1-jsonl` (311k registros, 332 MB). Registrar licencia (Apache 2.0) en `documents`. |
| 2. Normalizar al esquema §7.4: `decl_name = name[0]`, `module_path = ".".join(module_name)`, `docs_url` construido a partir del módulo, `text = informal_name + "\n" + informal_description + "\n\n" + signature`. |
| 3. Filtro configurable (`ingest.yaml`): excluir nombres auto-generados (`.proof_`, `.match_`, `_aux`, `.eq_`), módulos `Mathlib.Tactic.*` y `Mathlib.Deprecated.*`; `kind=instance` excluido por defecto. Medir el efecto en la tarea 6 y registrar la decisión. |
| 4. Embeber con el modelo de `versions.yaml` (documentos sin instrucción; consultas con instrucción). Guardar `embedding` en float16. |
| 5. Crear tabla `mathlib`; índice FTS sobre `decl_name` (además tokenizado por `.` y `_` en una columna `name_tokens`), `informal_name`, `informal_description`, `signature`; índice ANN (IVF-PQ o HNSW) y comprobar recall@50 ≥ 0.95 frente a búsqueda exacta en 200 consultas. |
| 6. Evaluación con `rag/evaluate.py` sobre **MathlibQR** (946 consultas) y **MathlibMPR** (69 teoremas): Recall@10, nDCG@10, MRR para 4 variantes: denso, BM25, híbrido, híbrido+rerank. Comparar con el valor publicado de LeanSearch v2 (nDCG@10 = 0.62 con modelos 8B). |
| 7. Notebook `notebooks/01_mathlib_retrieval_eval.ipynb` con la tabla de resultados (va al informe). |
|
|
| Salidas: `data/index/lancedb/mathlib`, `data/corpus/mathlib.jsonl`, tabla de métricas. |
| Aceptación: híbrido+rerank supera a denso solo en nDCG@10; Recall@10 ≥ 0.55 en MathlibQR (umbral inicial; se ajusta tras la primera medición y se documenta); latencia p50 < 2 s (GPU) / < 12 s (CPU) por consulta con rerank. |
| Plan B: si la tag de Mathlib del proyecto no puede ser `v4.28.0-rc1`, (a) preferir migrar los enunciados de miniF2F-v2 a esa tag; (b) si es imposible, reconstruir el corpus con el pipeline de extracción de LeanSearch v2 (Jixia) **sin** informalización (nombre + firma + docstring) y documentar la degradación esperada. |
|
|
| ### Fase 2 — Corpus B: ingesta de PDFs con OCR matemático y figuras (6–8 días) |
|
|
| **Objetivo:** convertir PDFs en *problem cards* y secciones con fórmulas LaTeX correctas, figuras recortadas y descritas, y metadatos de cita. |
|
|
| Tareas |
| 1. **Inventario**: por PDF, `sha256`, páginas, fuentes, nº de imágenes y trazos vectoriales, y una puntuación de fiabilidad de la capa de texto (proporción de líneas de 1–2 caracteres y de tokens matemáticos aislados). Guardar en `documents`. |
| 2. **Render**: páginas a PNG 200 dpi en `data/parsed/<doc_id>/pages/`; se reutilizan en parser, VLM y demo. |
| 3. **Parsing con MinerU** (backend VLM, modo imagen forzado; nunca capa de texto para fórmulas). Conservar `markdown`, `content_list.json` y recortes. Verificar en la versión instalada los nombres de campo de los bloques (`type`, `text`, `text_level`, `text_format=latex`, `img_path`, `image_caption`, `bbox`, `page_idx`) y adaptar el lector. |
| 4. **Red de seguridad de figuras vectoriales**: por página, `cluster_drawings()` de PyMuPDF; si un clúster con ≥ N trazos (config, p. ej. 6) no está cubierto ≥ 60 % por un bloque `image` de MinerU, recortarlo con padding (incluyendo etiquetas de texto cercanas) y registrarlo con `detected_by=vector_cluster`. Este paso existe porque el corpus de ejemplo tiene 441 trazos vectoriales de diagramas sin caption. |
| 5. **Parser estructural**: títulos → `section_path`; ítems numerados (`^\s*\d{1,3}[\.\)]`) → ítems; emparejar problema *N* ↔ solución *N* cuando existan secciones "Problemas/Problemario" y "Soluciones"; en documentos sin esa estructura, un ítem = enunciado + solución consecutivos. Figuras y ecuaciones se adjuntan al ítem que las contiene en orden de lectura; las referencias textuales ("figura", "dibujo", "fig.", "como se muestra") refuerzan el vínculo. Casos ambiguos → una llamada LLM por documento con el índice de bloques (no por página). |
| 6. **Enriquecimiento VLM** (`rag/enrich.py`, offline, en inglés, salida JSON validada con Pydantic; reintentos acotados): |
| - a) **Figura**: entrada = recorte + enunciado (y solución si existe) → `description`, `labels`, `objects`, `relations`, `given_values`, `figure_type`. Prompt fijo versionado en `configs/ingest.yaml`. |
| - b) **QA de fórmulas**: por página con ≥ 1 ecuación → imagen de página + lista de LaTeX extraído → lista corregida. Para corpus < 500 páginas: todas; para más: páginas marcadas por heurística (llaves desbalanceadas, LaTeX vacío o < 3 caracteres, `text_layer_reliable=false`) + 10 % aleatorio. |
| - c) **Card**: por problem card → `context_summary` (Contextual Retrieval, 2–3 frases: qué pide, área, idea clave, teoremas), `math_area`, `techniques`, `theorems_used`, `difficulty`. Usar prompt caching con el documento completo como prefijo cuando el proveedor lo permita. |
| 7. **Chunking**: `problem_card` (padre; `content_md` = enunciado + solución + descripciones de figuras); si la solución supera ~1 500 tokens, `solution_step` hijos con `parent_id`; cada figura además como chunk `figure` (texto = descripción + enunciado); papers → `paper_section` de 400–800 tokens con `section_path` y resumen del documento como contexto. |
| 8. **Embeber e indexar**: tabla `informal` (FTS sobre `text`, `keywords`, `theorems_used`, `techniques`) y tabla `figures`. |
| 9. **CLI** `ragsolver ingest <pdf|dir>` idempotente; `ragsolver ingest --reindex` sólo recalcula embeddings. |
| 10. **QA gates** (con el PDF de ejemplo): |
| - Gold de OCR: transcripción manual de 10 páginas (mezcla de problemas con fórmulas y soluciones). Métricas: distancia de edición normalizada en texto, tasa de coincidencia exacta de fórmulas tras normalizar LaTeX, y **cero** errores de exponente/subíndice perdidos (`2^{2001}` ≠ `22001`). |
| - Emparejamiento problema↔solución: 100/100 cards para el PDF de ejemplo. |
| - Figuras: 100 % de las figuras de los problemas 8, 16, 17, 22, 24, 37, 99 detectadas, recortadas con etiquetas visibles y descritas; revisión manual de 15 descripciones con rúbrica sí/no (¿nombra todos los puntos?, ¿relaciones correctas?, ¿valores dados?). |
|
|
| Salidas: `data/parsed/<doc_id>/…`, `data/corpus/informal.jsonl`, tablas `informal` y `figures`, reporte de QA en `docs/qa_ingest_<doc_id>.md`. |
| Aceptación: fórmulas ≥ 95 % exactas en el gold; texto ≤ 3 % distancia de edición; figuras y emparejamiento al 100 % en el PDF de ejemplo; ≥ 13/15 descripciones aprobadas. |
| Plan B: si MinerU falla en diagramas de línea o fórmulas del Equation Editor, activar el modo "página completa por VLM": una llamada por página con prompt de transcripción a Markdown+LaTeX y bloques `<figure>` con descripción; los recortes siguen viniendo de la tarea 4. Si MinerU no instala, PaddleOCR-VL con el mismo lector de bloques. |
|
|
| ### Fase 3 — Servicio de recuperación y citación (3–4 días) |
|
|
| **Objetivo:** `Retriever` único, tipado, con búsqueda híbrida, reranking, filtros, citas y traza; 0 llamadas LLM. |
|
|
| Tareas |
| 1. `rag/retrieve.py`: clase `Retriever` con `search(RetrievalRequest) -> RetrievalResult` que implementa §6.3; carga perezosa de modelos; caché LRU de embeddings de consulta. |
| 2. Plantillas de instrucción por `mode` (nl/formal/error/exemplar) en `retrieval.yaml`. |
| 3. Fusión RRF multi-consulta y multi-canal; dedupe por `decl_name`/`parent_id`; límite por módulo opcional. |
| 4. Constructor de `Citation` (labels legibles, localizadores, `docs_url`). |
| 5. Emisión de evento JSONL por búsqueda. |
| 6. Tests: RRF (orden esperado con listas conocidas), filtros (SQL), construcción de citas, contrato JSON Schema, modo `error` (identificador exacto recuperado en top-1), todo con embedder/reranker mock. Un test de integración real sobre el índice si existe. |
| 7. CLI `ragsolver search "..." --corpus mathlib --k 8` y `--mode exemplar` para inspección. |
|
|
| Salidas: `Retriever`, CLI, tests. |
| Aceptación: tests verdes; `search` sobre 20 consultas de MathlibQR reproduce las métricas de Fase 1 (misma función, sin duplicar lógica); consulta en modo `error` con `unknown identifier 'Nat.Prime.two_le'` devuelve esa declaración en el top-1. |
|
|
| ### Fase 4 — Integración en el grafo de agentes (4–5 días, con Rol A) |
|
|
| **Objetivo:** el RAG alimenta PLAN/GENERATE/FORMALIZE/CRITIQUE respetando el presupuesto de llamadas y produciendo citas verificadas. |
|
|
| Tareas |
| 1. Estado del grafo: añadir `evidence: list[Citation]`, `retrieval: dict[subgoal_id, RetrievalResult]`, `retrieval_trace`. |
| 2. PLAN: pre-recuperación de ejemplares (`mode=exemplar`, `corpora=[informal]`, `k=3`) con el enunciado; el prompt del Planificador recibe ejemplares (enunciado, `context_summary`, cita). El Planificador emite `search_queries` y `math_area` por subobjetivo (mismo call). |
| 3. RETRIEVE: por subobjetivo, `queries = [statement_nl] + search_queries`, `corpora=[mathlib, informal]`, `k=8` Mathlib / `k=3` informal; filtro `math_area` como *boost* (no exclusión). |
| 4. Formato de contexto en prompts: lemas como `name : signature — description (module)`; ejemplares como `[I1] statement — key idea — source, page`; figuras: descripción siempre; imagen sólo para los 2 primeros hits con figura y sólo si `llm_supports_vision` (config). |
| 5. GENERATE devuelve `used_citations[]`; FORMALIZE recibe firmas exactas. |
| 6. VERIFY ok → marcar `used_in_proof` por coincidencia de `decl_name` en el código aceptado; CRITIQUE con `missing_identifiers` → `mode=error` → GENERATE. |
| 7. Flags de ablación en `retrieval.yaml`: `enabled`, `corpora`, `rerank`, `k`; con `enabled=false` el nodo RETRIEVE devuelve resultado vacío y la traza lo registra. |
| 8. `SolutionReport` con `citations[]` clasificadas (verificadas / usadas en boceto / consultadas). |
|
|
| Salidas: grafo integrado; 5 teoremas triviales de referencia (§6.5 de la propuesta) resueltos con citas. |
| Aceptación: ≤ 20 llamadas LLM por problema con RAG activo, medido en la traza; `llm_calls=0` en todos los eventos del retriever; al menos un problema de dev con una cita `used_in_proof=true`. |
|
|
| ### Fase 5 — Evaluación del RAG y soporte a las ablaciones (4–5 días) |
|
|
| **Objetivo:** cuantificar el retriever aislado y su contribución end-to-end, con control de contaminación. |
|
|
| Tareas |
| 1. Gold formal propio: para cada problema del conjunto dev (miniF2F-v2), extraer los `decl_name` de Mathlib usados en la prueba verificada publicada → premisas gold; consultas = enunciado informal y formal. Métricas Recall@8/@20, nDCG@10. |
| 2. Gold informal: 30 consultas (paráfrasis de problemas del PDF y problemas nuevos análogos) → cards relevantes (anotación manual); 15 de ellas dependientes de figura. Recall@5 y "cobertura de figura" (la descripción contiene las entidades clave; rúbrica). |
| 3. Contaminación: similitud embedding > 0.9 entre cualquier card informal y cualquier problema de test → revisar y excluir del índice de evaluación; reportar el número excluido. |
| 4. Hook en el harness de ablaciones: configuraciones *sin RAG* / *con RAG*; métrica adicional "precisión de uso de lemas" = verificadas / recuperadas, y "tasa de re-recuperación exitosa" tras error `lema faltante`. |
| 5. Taxonomía de errores del retriever (para el informe): lema existe pero no se recuperó; nombre alucinado a pesar del contexto; ejemplar irrelevante; figura mal descrita. |
| 6. Notebook de resultados con tablas y figuras finales. |
|
|
| Salidas: `data/eval/*`, notebooks, tabla de contribución del RAG. |
| Aceptación: todas las métricas calculadas con intervalos (Wilson para tasas; bootstrap para medias) y reproducibles con un comando. |
|
|
| ### Fase 6 — Empaquetado y publicación (2–3 días) |
|
|
| Tareas |
| 1. HF Dataset `<org>/ragsolver-index`: carpeta LanceDB, `informal.jsonl`, `mathlib.jsonl` (o puntero al dataset de LeanSearch v2), recortes de figuras **sólo** de documentos `redistributable=true`; dataset card con licencias (Mathlib Apache 2.0, corpus LeanSearch v2 Apache 2.0, PDFs según cada licencia). |
| 2. Space Gradio: descarga del índice con `snapshot_download`; pestaña de búsqueda con citas, firma Lean, `docs_url`, recorte de figura y descripción; pestaña de resolución (si el presupuesto lo permite, con límite de llamadas). |
| 3. Documentación: `docs/architecture.md` (diagramas de §5 y §6), `docs/install.md`, `docs/interfaces.md` (JSON Schema de §8), `docs/reproduce.md` (comandos para reconstruir índice y evaluación con las versiones fijadas). |
|
|
| Aceptación: un usuario nuevo reproduce la evaluación de Fase 1 desde cero siguiendo `reproduce.md`. |
|
|
| ### Fase 7 — Extensiones opcionales (sólo si se cumple el disparador) |
|
|
| | Extensión | Disparador para hacerla | Qué implica | |
| |---|---|---| |
| | Canal visual (ColQwen3-4B o jina-embeddings-v4 multivector sobre imágenes de página, tabla multivector en LanceDB, fusión RRF con el canal de texto) | Recall@5 de las 15 consultas dependientes de figura < 0.7 tras la Fase 5 | GPU para codificar consultas; ~1 000 vectores × 128 d por página | |
| | Enlaces técnica→lema (`mathlib_candidates`) | El Generador cita teoremas informales que el Autoformalizador no encuentra | Por cada `theorems_used`, una búsqueda offline en Mathlib; sin LLM | |
| | Corpus NuminaMath-1.5 (subconjunto de las áreas del alcance) | Los ejemplares informales del PDF resultan insuficientes (pocos hits relevantes) | Deduplicación contra test (Fase 5.3) obligatoria | |
| | Subir a Qwen3-Embedding-4B / Reranker-4B | GPU ≥ 16 GB disponible y ganancia ≥ 3 puntos en nDCG@10 en MathlibQR | Re-embeber Mathlib (~1 h en L4) | |
| | Recuperación iterativa tipo LeanSearch v2 "sketch-retrieve-reflect" | Sobra presupuesto de llamadas (< 12 por problema) | +1–2 llamadas por subobjetivo | |
|
|
| --- |
|
|
| ## 11. Evaluación del RAG (resumen) |
|
|
| ### 11.1 Conjuntos |
| - **MathlibQR** (946 consultas / 200 decls) y **MathlibMPR** (69 teoremas con grupos de premisas), del repositorio de LeanSearch v2. |
| - **Premisas gold miniF2F-v2** (Fase 5.1). |
| - **Gold informal** (30 consultas, 15 con figura) sobre el PDF de ejemplo. |
| - **Gold de OCR** (10 páginas transcritas a mano). |
|
|
| ### 11.2 Métricas |
| - Retriever: Recall@k, nDCG@10, MRR, latencia p50/p95, tamaño del índice. |
| - OCR: distancia de edición de texto, exactitud de fórmulas, detección/descripción de figuras (rúbrica). |
| - End-to-end (de la propuesta): pass@1/pass@k con y sin RAG, llamadas LLM, tokens, tiempo; **precisión de uso de lemas**; éxito de re-recuperación tras `lema faltante`. |
|
|
| ### 11.3 Reglas metodológicas |
| - Partición dev/test estricta; prompts y umbrales se ajustan sólo en dev. |
| - Control de contaminación del corpus informal contra test (§10 Fase 5.3). |
| - Toda cifra del informe sale de un notebook reproducible con las versiones de `versions.yaml`. |
|
|
| ### 11.4 Disparadores de escalado (evitan sobre-ingeniería) |
| Definidos en la tabla de Fase 7: el canal visual, NuminaMath, modelos 4B y la recuperación iterativa sólo se construyen si las métricas de Fase 5 lo justifican. |
|
|
| --- |
|
|
| ## 12. Riesgos específicos del RAG y mitigaciones |
|
|
| | Riesgo | Impacto | Mitigación | |
| |---|---|---| |
| | Versión de Mathlib del índice ≠ la del verificador → nombres de lemas inexistentes | Alto | Una sola tag en `versions.yaml`; test de arranque que verifica 20 `decl_name` aleatorios del índice con `lean-interact` (`#check`) | |
| | MinerU clasifica mal diagramas de línea o fórmulas del Equation Editor | Alto | Red de seguridad vectorial (Fase 2.4), QA de fórmulas con VLM (2.6b), gold de 10 páginas (2.10), Plan B "página completa por VLM" | |
| | Vectorización en GPU AMD sin validar: MinerU no tiene ROCm como ruta oficial (sólo un chip validado por la comunidad); PyTorch/flash-attn requieren wheel e implementación de atención distintas | Medio | Smoke test en la máquina real en Fase 0 (§9.4, tarea 7); fallback a Perfil B (CPU/VLM por API) sin bloquear el cronograma | |
| | Descripciones de figuras genéricas e inútiles | Medio | Prompt con enunciado como contexto y salida estructurada (labels/relations/values); rúbrica manual | |
| | Ruido de Mathlib (instances, auxiliares) desplaza lemas útiles | Medio | Filtro de Fase 1.3 medido en MathlibQR | |
| | Presupuesto de llamadas (RNF-3) | Medio | Retriever con 0 llamadas; enriquecimiento sólo offline; `search_queries` dentro de la salida del Planificador | |
| | Contaminación del test con el corpus informal | Metodológico | Dedupe por similitud + revisión manual; reportar exclusiones | |
| | Coste/tiempo de embeber 311k declaraciones | Bajo | 0.6B local en T4 ≈ 15–30 min; API ≈ 7 USD; guardar embeddings en el dataset publicado | |
| | Licencias de PDFs | Legal | `redistributable` por documento; no publicar recortes ni texto de fuentes no redistribuibles; citar igual | |
| | Cambios de API en MinerU/LanceDB | Bajo | Versiones fijadas; lector de bloques con test sobre una salida de ejemplo guardada en `tests/fixtures/` | |
|
|
| --- |
|
|
| ## 13. Referencias consultadas |
|
|
| - LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving (2026) — https://arxiv.org/abs/2605.13137 · código https://github.com/frenzymath/LeanSearch-v2 · corpus https://huggingface.co/datasets/FrenzyMath/lsv2-mathlib-v4.28.0-rc1-jsonl · API https://leansearch.net/ |
| - Lean Finder: Semantic Search for Mathlib That Understands User Intents (2025) — https://arxiv.org/abs/2510.15940 |
| - TheoremGraph: Bridging Formal and Informal Mathematics (2026) — https://arxiv.org/pdf/2606.25363 |
| - miniF2F-Lean Revisited / miniF2F-v2 (2025) — https://arxiv.org/abs/2511.03108 · https://github.com/roozbeh-yz/miniF2F_v2 |
| - Anthropic, Contextual Retrieval (2024) — https://www.anthropic.com/engineering/contextual-retrieval |
| - OmniDocBench (CVPR 2025) y leaderboard — https://github.com/opendatalab/OmniDocBench |
| - MinerU (OpenDataLab) — https://github.com/opendatalab/MinerU · MinerU2.5-Pro (2026) https://arxiv.org/pdf/2604.04771 |
| - PaddleOCR-VL-1.6 (2026) — https://arxiv.org/abs/2606.03264 · GLM-OCR https://arxiv.org/pdf/2603.10910 |
| - When Good OCR Is Not Enough: Benchmarking OCR Robustness for RAG (2026) — https://arxiv.org/pdf/2605.00911 |
| - LlamaIndex, "OmniDocBench is saturated" — https://www.llamaindex.ai/blog/omnidocbench-is-saturated-what-s-next-for-ocr-benchmarks |
| - jina-embeddings-v4 (2025) — https://arxiv.org/abs/2506.18902 · ColQwen3 https://huggingface.co/OpenSearch-AI/Ops-Colqwen3-4B |
| - LanceDB: hybrid search y multivector — https://docs.lancedb.com/search/multivector-search · https://www.lancedb.com/blog/hybrid-search-combining-bm25-and-semantic-search-for-better-results-with-lan-1358038fe7e6 |
| - Qwen3-Embedding / Qwen3-Reranker (MTEB) — https://www.codesota.com/benchmarks/mteb · https://presenc.ai/research/best-open-weight-embedding-models-2026 |
| - Kimina Lean Server (2025) — https://arxiv.org/abs/2504.21230 · LeanInteract https://github.com/augustepoiroux/LeanInteract |
| - NuminaMath-1.5 (Apache 2.0) — https://huggingface.co/datasets/AI-MO/NuminaMath-1.5 · NuminaMath-LEAN https://huggingface.co/datasets/AI-MO/NuminaMath-LEAN |
| - Qwen3-VL Technical Report (2025) — https://arxiv.org/pdf/2511.21631 |
| |
