Hugging Face's logo

CamiloS1111
/
ragsolver

lean4
mathlib
retrieval
rag
theorem-proving
olympiad
multi-agent
Model card Files
xet
 Community
ragsolver / docs /PLAN_RAG.md
CamiloS1111's picture
CamiloS1111
Upload folder using huggingface_hub
ee54756 verified
preview code
|
Raw History Blame Contribute Delete
59.4 kB

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 

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