"""Fase 5, tarea 6 — informe de evaluación (docs/eval_report.md) a partir de los JSON de data/eval/results/ y data/eval/runs//summary.json. Uso: python scripts/eval_report.py [--run-id run-...] """ from __future__ import annotations import argparse import json from pathlib import Path R = Path("data/eval/results") def _load(name: str) -> dict | None: p = R / name return json.loads(p.read_text(encoding="utf-8")) if p.exists() else None def _metrics_table(res: dict, variants: list[str], metrics: list[str]) -> list[str]: head = "| Variante | " + " | ".join(metrics) + " |" lines = [head, "|---|" + "---|" * len(metrics)] for v in variants: if v in res: lines.append(f"| {v} | " + " | ".join(f"{res[v][m]:.3f}" for m in metrics) + " |") return lines def _ablation_details(run_dir: Path) -> list[str]: """Matriz problema×config, McNemar exacto pareado, falsos positivos evitados, uso de lemas.""" from itertools import combinations from math import comb res = [json.loads(l) for l in (run_dir / "results.jsonl").read_text(encoding="utf-8").splitlines() if l.strip()] cfgs = list(dict.fromkeys(r["config"] for r in res)) probs = list(dict.fromkeys(r["problem_id"] for r in res)) by = {(r["config"], r["problem_id"]): r for r in res} ok = lambda c, p: by.get((c, p), {}).get("status") == "done" L = ["### Resultado por problema (✔ = prueba aceptada por el kernel)", "", "| Problema | " + " | ".join(cfgs) + " |", "|---|" + "---|" * len(cfgs)] for p in probs: L.append(f"| `{p}` | " + " | ".join("✔" if ok(c, p) else "–" for c in cfgs) + " |") L += ["", "### Comparación pareada (McNemar exacto, α = 0.05; n pequeño → poca potencia)", "", "| A | B | sólo A | sólo B | p |", "|---|---|---|---|---|"] for a, b in combinations([c for c in cfgs if c != "baseline_b"], 2): n01 = sum(1 for p in probs if ok(a, p) and not ok(b, p)) n10 = sum(1 for p in probs if ok(b, p) and not ok(a, p)) n = n01 + n10 pval = min(1.0, 2 * sum(comb(n, k) for k in range(0, min(n01, n10) + 1)) / 2**n) if n else 1.0 L.append(f"| {a} | {b} | {n01} | {n10} | {pval:.3f} |") if "baseline_b" in cfgs and "baseline_a" in cfgs: self_ok = [p for p in probs if by[("baseline_b", p)].get("self_assessed_correct")] fp = sum(1 for p in self_ok if not ok("baseline_a", p)) L += ["", f"**Falsos positivos evitados** (propuesta §8.3): la línea base B se autoevaluó como correcta en {len(self_ok)}/{len(probs)} problemas; en {fp} de ellos la formalización directa (línea base A) **no** pasa el kernel."] full = [r for r in res if r["config"] == "full"] if full: used = [(r["problem_id"], r["n_used_in_proof"], r["n_used_in_sketch"], r["n_retrieved"]) for r in full] L += ["", "### Uso de lemas recuperados (config `full`)", "", "| Problema | verificados en la prueba | usados en el boceto | recuperados |", "|---|---|---|---|"] L += [f"| `{p}` | {a} | {b} | {c} |" for p, a, b, c in used] L += ["", "Pruebas aceptadas (`full`):", ""] for r in full: if r["status"] == "done" and ":= by" in r["lean_code"]: body = r["lean_code"].split(":= by", 1)[1].strip().replace("\n", " · ")[:120] L.append(f"- `{r['problem_id']}`: `{body}`") models = sorted({m for r in res for m in r["models"]}) L += ["", f"Modelos LLM usados en la corrida (cadena por cuota diaria): {models}. Re-recuperaciones tras `lema faltante` en `full`: {sum(r['re_retrievals'] for r in full)} (exitosas: {sum(r['re_retrievals_ok'] for r in full)})."] return L def _strata(run_dir: Path, problems_path: Path) -> list[str]: """pass@1 por configuración desglosado por split (dev/test), área y nivel de dificultad (§8.1).""" from ragsolver.orchestrator.run import wilson meta = {json.loads(l)["problem_id"]: json.loads(l) for l in problems_path.read_text(encoding="utf-8").splitlines() if l.strip()} res = [json.loads(l) for l in (run_dir / "results.jsonl").read_text(encoding="utf-8").splitlines() if l.strip()] res = [r for r in res if r["problem_id"] in meta] cfgs = list(dict.fromkeys(r["config"] for r in res)) L = ["### Desglose por estrato (pass@1, n) — `" + problems_path.name + "`", ""] for key, title in (("split", "partición"), ("area", "área"), ("difficulty", "nivel de dificultad")): values = sorted({meta[r["problem_id"]].get(key) for r in res}, key=str) L += [f"**Por {title}**", "", "| " + title + " | " + " | ".join(cfgs) + " |", "|---|" + "---|" * len(cfgs)] for v in values: cells = [] for c in cfgs: rs = [r for r in res if r["config"] == c and meta[r["problem_id"]].get(key) == v] k = sum(r["status"] == "done" for r in rs) cells.append(f"{k}/{len(rs)} ({k / len(rs):.2f}) {wilson(k, len(rs))}" if rs else "–") L.append(f"| {v} | " + " | ".join(cells) + " |") L.append("") return L def main() -> None: ap = argparse.ArgumentParser() ap.add_argument("--run-id", default=None, help="carpeta en data/eval/runs con summary.json") ap.add_argument("--out", default="docs/eval_report.md") ap.add_argument("--problems", default=None, help="JSONL de problemas para desglosar por split/área/nivel") args = ap.parse_args() L = ["# Evaluación del RAG y del pipeline — RagSolver", "", "Generado por `scripts/eval_report.py`. Metodología: `docs/PLAN_RAG.md` §10-§11; decisiones y correcciones: `docs/DECISIONS.md`.", ""] full = _load("fase1_redo_mathlibqr_sample3903_norerank.json") s200 = _load("fase1_redo_mathlibqr_sample3903_100q.json") if full: L += ["## 1. Retriever sobre Mathlib (MathlibQR, LeanSearch v2)", "", f"Tabla de muestra: gold de MathlibQR/MPR + premisas de miniF2F + 3000 distractores. Cobertura del gold en la tabla: **{full['n_gold_covered_in_table']}/{full['n_queries']} ({full['coverage_ratio']:.1%})**. Métricas crudas (el recall condicionado a cobertura = crudo ÷ cobertura).", "", f"### 1a. {full['n_queries']} consultas, sin rerank", ""] L += _metrics_table(full, ["denso", "bm25", "hibrido"], ["recall@10", "ndcg@10", "mrr"]) if s200: L += ["", f"### 1b. Muestra aleatoria de {s200['n_queries']} consultas (semilla fija), 4 variantes", ""] L += _metrics_table(s200, ["denso", "bm25", "hibrido", "hibrido_rerank"], ["recall@10", "ndcg@10", "mrr"]) fidx = _load("fase1_full_mathlibqr_100q.json") if fidx: L += ["", f"### 1c. Misma muestra de {fidx['n_queries']} consultas sobre el **índice completo de Mathlib** (`mathlib_full`, 278 160 declaraciones; DECISIONS #48, #56)", ""] L += _metrics_table(fidx, ["denso", "bm25", "hibrido", "hibrido_rerank"], ["recall@10", "ndcg@10", "mrr"]) L += ["", "Los números de la tabla de muestra (1a-1b) están inflados por el tamaño del pool (3 903 candidatos); 1c es la medida realista del retriever en producción."] ann = _load("ann_mathlib_full.json") if ann: L += ["", f"**Índice ANN** (`{ann['index_type']}`, {ann['num_partitions']} particiones, nprobes {ann['nprobes']}, refine ×{ann['refine_factor']}; DECISIONS #60): recall@10 respecto de la búsqueda exacta **{ann['ann_recall@10_vs_exact']}**, recall@50 {ann['ann_recall@50_vs_exact']} ({ann['n_queries']} consultas sintéticas); latencia densa p50 {ann['latency_exact_s']['p50']} s → **{ann['latency_ann_s']['p50']} s** (p95 {ann['latency_exact_s']['p95']} → {ann['latency_ann_s']['p95']} s)."] fann = _load("fase1_full_ann_mathlibqr_100q.json") if fann: L += ["", f"### 1d. Misma muestra sobre el índice completo **con el índice ANN** (el que usan la demo y los agentes con `RAGSOLVER_MATHLIB_TABLE=mathlib_full`)", ""] L += _metrics_table(fann, ["denso", "bm25", "hibrido", "hibrido_rerank"], ["recall@10", "ndcg@10", "mrr"]) L.append("") prem = _load("fase5_premises.json") if prem: L += ["## 2. Premisas gold de miniF2F (pruebas verificadas de DeepSeek-Prover-V2)", "", f"Problemas: {prem['n_problems']} (con ≥1 premisa en la tabla: {prem['n_problems_with_covered_premises']}); cobertura de premisas en la tabla: {prem['premise_coverage']:.1%}; rerank: {prem['rerank']}.", "", "| Consulta | recall@8 | recall@20 | ndcg@10 | mrr |", "|---|---|---|---|---|"] pfull = _load("fase5_premises_full.json") for label, res in (("tabla de muestra", prem), ("índice completo", pfull)): for mode in ("nl", "formal"): m = (res or {}).get(f"query_{mode}") if m: L.append(f"| {'enunciado informal' if mode == 'nl' else 'enunciado formal (Lean)'} ({label}) | {m['recall@8']:.3f} | {m['recall@20']:.3f} | {m['ndcg@10']:.3f} | {m['mrr']:.3f} |") L.append("") inf = _load("fase5_informal_gold.json") if inf: fd = inf["figure_dependent"] L += ["## 3. Gold informal (30 consultas sobre el PDF de ejemplo)", "", f"- Recall@5: **{inf['recall@5']:.3f}** (Wilson 95 %: {inf['recall@5_wilson95']}); MRR: {inf['mrr']:.3f}", f"- Consultas dependientes de figura (n={fd['n']}): Recall@5 = {fd['recall@5']:.3f}; cobertura de entidades en las descripciones de figura = {fd['figure_coverage_mean']}", ""] cont = _load("fase5_contamination.json") if cont: L += ["## 4. Contaminación corpus informal ↔ miniF2F-v2", "", f"- Pares con similitud > {cont['threshold']}: **{cont['n_pairs_over_threshold']}** de {cont['n_cards']}×{cont['n_minif2f']}; similitud máxima observada: {cont['max_similarity']:.3f}", f"- Top-3 más parecidos (card, problema, sim): {cont['top10_most_similar'][:3]}", ""] if args.run_id: run_dir = Path("data/eval/runs") / args.run_id summ = json.loads((run_dir / "summary.json").read_text(encoding="utf-8")) L += [f"## 5. Ablaciones end-to-end (`{args.run_id}`)", "", "| Config | n | pass@1 | IC95 Wilson | llamadas LLM (media) | tokens (media) | wall s (mediana) | precisión uso de lemas | re-recuperación OK | taxonomía de errores |", "|---|---|---|---|---|---|---|---|---|---|"] for name, s in summ.items(): L.append(f"| {name} | {s['n']} | {s['pass@1']} | {s['pass@1_wilson95']} | {s['llm_calls_mean']} | {s['tokens_mean']} | {s['wall_s_median']} | {s['lemma_use_precision']} | {s['re_retrieval_success']} | {s['error_taxonomy']} |") L += ["", *_ablation_details(run_dir), ""] if args.problems: L += _strata(run_dir, Path(args.problems)) + [""] g = lambda c, m: summ.get(c, {}).get(m) if all(c in summ for c in ("full", "no_rag", "no_critic", "baseline_a")): res = [json.loads(l) for l in (run_dir / "results.jsonl").read_text(encoding="utf-8").splitlines() if l.strip()] ok = {(r["config"], r["problem_id"]) for r in res if r["status"] == "done"} probs = {r["problem_id"] for r in res} disc = lambda a, b: (sum((a, p) in ok and (b, p) not in ok for p in probs), sum((b, p) in ok and (a, p) not in ok for p in probs)) pba = g("full", "pass_by_attempt") or {} first = pba.get("1", pba.get(1)) claims = [r["problem_id"] for r in res if r["config"] == "baseline_b" and r.get("self_assessed_correct")] confirmed = sum(any((c, p) in ok for c in ("full", "no_rag", "no_critic", "baseline_a")) for p in claims) L += [ "### Lectura (métricas de la propuesta §8.3)", "", f"- **Contribución del RAG** = pass@1(full) − pass@1(sin RAG) = {g('full','pass@1')} − {g('no_rag','pass@1')} = **{round(g('full','pass@1') - g('no_rag','pass@1'), 3)}** (pares discordantes {disc('full', 'no_rag')}); el contexto recuperado multiplica los tokens por {round(g('full','tokens_mean') / g('no_rag','tokens_mean'), 1)}×; precisión de uso de lemas = {g('full','lemma_use_precision')}.", f"- **Robustez del refinamiento** = pass@1(full) − pass@1(sin Crítico) = **{round(g('full','pass@1') - g('no_critic','pass@1'), 3)}** (pares discordantes {disc('full', 'no_critic')}); dentro de `full`, pass@1 tras el 1.er intento = {first} y final = {g('full','pass@1')}: la ganancia atribuible a los reintentos es la diferencia entre ambos; el resto de la brecha con `sin Crítico` (mismo primer intento) es variación entre corridas.", f"- **Eficiencia**: {g('full','llm_calls_mean')} llamadas LLM por problema en `full` (tope RNF-3: 20), {g('baseline_a','llm_calls_mean')} en la línea base A.", f"- **Verificación formal vs. autoevaluación**: la línea base B se declaró correcta en {len(claims)}/{len(probs)} problemas; el kernel confirma {confirmed} de esos en alguna configuración verificada.", "", ] Path(args.out).write_text("\n".join(L), encoding="utf-8") print(args.out) if __name__ == "__main__": main()