| """Fase 1, tarea 8 de docs/PLAN_CORRECCIONES.md — re-verificación offline de |
| `eval-v1` con el verificador endurecido (SEC-1, VER-1, BUG-2). 0 llamadas LLM: |
| sólo el REPL de Lean (~1 min de import + ~0.3 s por fila). |
| |
| 1. Validación de tácticas (`find_forbidden_tactic`) sobre el `lean_code` |
| final de las 300 filas: mide falsos positivos del denylist nuevo contra |
| tácticas reales ya producidas por el LLM. |
| 2. Re-verificación completa (kernel + auditoría de axiomas) de las 27 filas |
| `done`, reconstruyendo el archivo con el `header` del problema (BUG-2), |
| que el `lean_code` original no incluía. |
| |
| No modifica `results.jsonl`. Escribe `data/eval/runs/eval-v1/reverify.json`. |
| |
| Uso: uv run python scripts/reverify_eval_v1.py |
| """ |
|
|
| from __future__ import annotations |
|
|
| import json |
| import re |
| from pathlib import Path |
|
|
| from ragsolver.agents.agents import load_agents_config |
| from ragsolver.agents.schemas import Problem |
| from ragsolver.lean.verify import LeanChecker, find_forbidden_tactic |
|
|
| RUN_DIR = Path("data/eval/runs/eval-v1") |
| PROBLEMS_PATH = Path("data/eval/problems/eval_v1.jsonl") |
|
|
| _TACTICS_SPLIT_RE = re.compile(r":=\s*by\n") |
|
|
|
|
| def extract_tactics(lean_code: str) -> str | None: |
| """Tácticas ya indentadas a 2 espacios que dejó el `build_file` original |
| (formato antiguo, sin `#print axioms`): todo lo que sigue al primer |
| `:= by\\n` del archivo, de-indentado. None si no se encuentra el patrón.""" |
| m = _TACTICS_SPLIT_RE.search(lean_code) |
| if not m: |
| return None |
| tail = lean_code[m.end() :] |
| lines = tail.split("\n") |
| while lines and lines[-1].strip() == "": |
| lines.pop() |
| return "\n".join(line[2:] if line.startswith(" ") else line for line in lines) |
|
|
|
|
| def main() -> None: |
| rows = [json.loads(l) for l in (RUN_DIR / "results.jsonl").read_text(encoding="utf-8").splitlines() if l.strip()] |
| problems = {p.problem_id: p for p in (Problem.model_validate_json(l) for l in PROBLEMS_PATH.read_text(encoding="utf-8").splitlines() if l.strip())} |
| lean_cfg = load_agents_config()["lean"] |
|
|
| |
| false_positives = [] |
| n_checked = 0 |
| for r in rows: |
| code = r.get("lean_code") or "" |
| if not code: |
| continue |
| tactics = extract_tactics(code) |
| if tactics is None: |
| continue |
| n_checked += 1 |
| hit = find_forbidden_tactic(tactics) |
| if hit: |
| false_positives.append({"config": r["config"], "problem_id": r["problem_id"], "status": r["status"], "denied_token": hit, "tactics": tactics[:300]}) |
|
|
| |
| done = [r for r in rows if r["status"] == "done" and r.get("lean_code")] |
| checker = LeanChecker(imports=lean_cfg["imports"], timeout_s=lean_cfg["timeout_s"]) |
| checker.check("theorem _warmup : True := by sorry", "trivial") |
| reverified = [] |
| for r in done: |
| problem = problems.get(r["problem_id"]) |
| if problem is None: |
| reverified.append({"config": r["config"], "problem_id": r["problem_id"], "skipped": "problema no encontrado en eval_v1.jsonl"}) |
| continue |
| tactics = extract_tactics(r["lean_code"]) |
| if tactics is None: |
| reverified.append({"config": r["config"], "problem_id": r["problem_id"], "skipped": "no se pudo extraer las tácticas del lean_code original"}) |
| continue |
| v = checker.check(problem.formal_statement, tactics, problem.header, lean_cfg["max_heartbeats"]) |
| reverified.append( |
| { |
| "config": r["config"], |
| "problem_id": r["problem_id"], |
| "ok_before": True, |
| "ok_now": v.ok, |
| "axioms": v.axioms, |
| "non_standard_axioms": [a for a in v.axioms if a not in ("propext", "Classical.choice", "Quot.sound")], |
| "errors": v.errors[:2] if not v.ok else [], |
| } |
| ) |
| checker.close() |
|
|
| regressions = [x for x in reverified if x.get("ok_before") and not x.get("ok_now")] |
| out = { |
| "n_rows": len(rows), |
| "n_lean_code_checked_for_false_positives": n_checked, |
| "n_false_positives": len(false_positives), |
| "false_positives": false_positives, |
| "n_done_reverified": len(reverified), |
| "n_regressions": len(regressions), |
| "regressions": regressions, |
| "reverified": reverified, |
| } |
| (RUN_DIR / "reverify.json").write_text(json.dumps(out, indent=2, ensure_ascii=False), encoding="utf-8") |
| print(json.dumps({k: v for k, v in out.items() if k != "reverified"}, indent=2, ensure_ascii=False)) |
|
|
|
|
| if __name__ == "__main__": |
| main() |
|
|
