| """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/<run_id>/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() |
|
|
