Contratos de interfaz (RNF-4)
Todos los contratos son modelos Pydantic v2; los JSON Schema en docs/interfaces/*.schema.json se regeneran con python scripts/export_schemas.py y son derivados del código, no al revés.
Módulo RAG (src/ragsolver/rag/schema.py, PLAN_RAG.md §7-§8)
| Esquema | Uso |
|---|---|
Document |
metadatos por fuente (doc_id, licencia, redistributable, parser) |
ChunkBase / MathlibChunk / InformalChunk |
filas de las tablas LanceDB mathlib / informal |
Figure |
tabla figures (recorte, bbox, descripción VLM, detected_by) |
RetrievalRequest |
entrada del retriever: queries[1-4], mode, corpora, k, n_candidates, filters, rerank, include_figures, context |
RetrievalResult |
hits[] (con figures[] y citation), citations[], trace |
Citation |
citation_id (M1../I1..), locator, scores, used_in_proof, used_in_sketch, snippet |
TraceEvent |
evento JSONL por búsqueda/llamada (RNF-5) con VersionsPin; en llamadas LLM request lleva model, tokens_in, tokens_out, cost_usd (exacto, OpenRouter) y decision (salida validada) |
Agentes (src/ragsolver/agents/schemas.py, propuesta §6.3)
| Esquema | Agente | Campos clave |
|---|---|---|
Problem |
entrada | informal_statement, formal_statement (... := by sorry), header (open ...), imports |
PlannerOutput |
Planificador | strategy, subgoals[1-6] con statement_nl, formal_hint, search_queries[≤3], math_area |
GeneratorOutput |
Generador | sketch, used_citations[] |
FormalizerOutput |
Autoformalizador | proof_tactics (sólo el bloque tras := by), notes |
CriticOutput |
Crítico | error_type, action (retry/replan/abandon), missing_identifiers[], feedback |
BaselineAOutput / BaselineBOutput |
líneas base A / B | A: proof_tactics (obligatorio); B: natural_language_proof + self_assessed_correct (obligatorios) |
Verdict |
Verificador | ok, errors[{line,col,message}], uses_sorry, axioms[] (auditoría VER-1: ok=true exige subconjunto de propext/Classical.choice/Quot.sound), seconds |
SolutionReport |
orquestador | estado, intentos, llamadas, tokens, lean_code, citations[] clasificadas, taxonomía de errores, re-recuperaciones |
Configuración
configs/versions.yaml: pins (Lean/Mathlib, modelos, proveedor LLM y cadena de modelos, índice).configs/retrieval.yaml: plantillas de consulta por modo,rrf_k,max_per_module, flags de ablación del retriever.configs/agents.yaml:k_max,llm_budget, recuperación de los agentes, backend Lean, configuraciones de ablación, prompts versionados.configs/ingest.yaml: filtros de Mathlib, parámetros del PDF, prompts de enriquecimiento (versionados).