| |
| """ |
| Evaluate baseline ``trans_query.txt`` outputs against ``datasets/query_translation_eval.csv``. |
| |
| Metrics (per row): |
| - exact_match: normalized equality vs **reference-XML-adapted** gold (same identifier space |
| as ``artifacts/baselines/claude/*.xml`` and verifyta on those models) |
| - exact_match_dataset_csv: same vs raw ``ground_query`` from CSV |
| - token_precision / recall / f1: vs adapted gold; ``*_dataset_csv`` vs CSV gold |
| - semantic_correct (optional --verifyta): ``verdict(pred) == verdict(gold)`` on the same XML |
| - csv_answer_agree (optional): whether ``verdict(pred)`` matches CSV ``answer`` (T/F) |
| |
| Gold model layout: |
| Pass ``--gold-models-dir D`` so that ``D/1.xml`` ... ``D/10.xml`` exist (``spec_id`` in CSV). |
| |
| Usage: |
| python scripts/eval_baseline_trans_query.py \\ |
| --csv datasets/query_translation_eval.csv \\ |
| --pred artifacts/baselines/gpt/trans_query.txt \\ |
| --gold-models-dir artifacts/_gold_modelbuild_runs_20260501_182558 |
| |
| python scripts/eval_baseline_trans_query.py ... --verifyta --json-out artifacts/eval_gpt.json |
| """ |
|
|
| from __future__ import annotations |
|
|
| import argparse |
| import csv |
| import json |
| import re |
| import sys |
| from collections import Counter |
| from pathlib import Path |
| from typing import Any |
|
|
| ROOT = Path(__file__).resolve().parents[1] |
| sys.path.insert(0, str(ROOT / "src")) |
|
|
| from frame.evaluation.natural2ctl_query_normalize import normalize_natural2ctl_gold_query |
| from frame.evaluation.reference_xml_gold_adapt import adapt_csv_gold_to_reference_xml |
| from frame.pipeline.nl_uppaal_query import parse_verifyta_text_verdict |
|
|
| try: |
| from frame.pipeline.model_checking_pipeline import ModelCheckingPipeline |
| except ImportError: |
| ModelCheckingPipeline = None |
|
|
|
|
| def normalize_query(s: str) -> str: |
| return normalize_natural2ctl_gold_query(re.sub(r"\s+", " ", s.strip())) |
|
|
|
|
| _TOK_RE = re.compile( |
| r""" |
| (A\s*\[\]|E\s*<>|A\s*<>|E\s*\[\]) |
| |(-->) |
| |(&&|\|\||<=|>=|==|!=) |
| |([(){}\[\],]) |
| |(\bforall\b|\bexists\b|\bimply\b|\bnot\b|\bdeadlock\b) |
| |([A-Za-z_]\w*) |
| |(\d+) |
| """, |
| re.VERBOSE | re.IGNORECASE, |
| ) |
|
|
|
|
| def token_f1(pred: str, gold: str) -> tuple[float, float, float]: |
| p = normalize_query(pred) |
| g = normalize_query(gold) |
| pt = [t for t in _TOK_RE.findall(p) for t in t if t] |
| gt = [t for t in _TOK_RE.findall(g) for t in t if t] |
| pc = Counter(pt) |
| gc = Counter(gt) |
| inter = sum((pc & gc).values()) |
| p_tot = sum(pc.values()) |
| g_tot = sum(gc.values()) |
| if p_tot == 0 and g_tot == 0: |
| return 1.0, 1.0, 1.0 |
| if p_tot == 0 or g_tot == 0: |
| return 0.0, 0.0, 0.0 |
| prec = inter / p_tot |
| rec = inter / g_tot |
| if prec + rec == 0: |
| return 0.0, 0.0, 0.0 |
| return prec, rec, 2 * prec * rec / (prec + rec) |
|
|
|
|
| def _strip_inline_comment(line: str) -> str: |
| if "//" in line: |
| line = line.split("//", 1)[0] |
| return line.strip() |
|
|
|
|
| def _strip_backticks(s: str) -> str: |
| s = s.strip() |
| if s.startswith("`") and s.endswith("`") and len(s) >= 2: |
| return s[1:-1].strip() |
| return s |
|
|
|
|
| def parse_trans_query_file(path: Path) -> list[str]: |
| """ |
| Parse baseline text: numbered lines ``1. ...`` / ``2) ...``, optional ``Spec N`` headers, |
| or one formula per non-empty line (Grok-style). |
| """ |
| text = path.read_text(encoding="utf-8", errors="replace") |
| raw_lines = text.splitlines() |
| lines: list[str] = [] |
| for ln in raw_lines: |
| ln = _strip_inline_comment(ln).strip() |
| if not ln or re.match(r"^Spec\s+\d+\s*$", ln, re.IGNORECASE): |
| continue |
| lines.append(ln) |
|
|
| numbered: list[tuple[int, str]] = [] |
| for ln in lines: |
| m = re.match(r"^\s*(\d+)\s*[\.)]\s*(.+)$", ln) |
| if m: |
| numbered.append((int(m.group(1)), _strip_backticks(m.group(2)))) |
|
|
| |
| if len(numbered) >= max(3, len(lines) // 2): |
| by_id: dict[int, str] = {} |
| for idx, q in numbered: |
| by_id[idx] = q |
| order = sorted(by_id.keys()) |
| return [by_id[i] for i in order] |
|
|
| out: list[str] = [] |
| for ln in lines: |
| m = re.match(r"^\s*(\d+)\s*[\.)]\s*(.+)$", ln) |
| if m: |
| out.append(_strip_backticks(m.group(2))) |
| else: |
| out.append(_strip_backticks(ln)) |
| return out |
|
|
|
|
| def _csv_answer_to_verdict(ans: str) -> str | None: |
| t = (ans or "").strip().upper() |
| if t == "T": |
| return "satisfied" |
| if t == "F": |
| return "not_satisfied" |
| return None |
|
|
|
|
| def load_eval_csv(path: Path) -> list[dict[str, str]]: |
| rows: list[dict[str, str]] = [] |
| with path.open(encoding="utf-8", newline="") as f: |
| r = csv.DictReader(f) |
| for row in r: |
| if not row.get("spec_id"): |
| continue |
| rows.append(row) |
| return rows |
|
|
|
|
| def resolve_model_path(spec_id: str, models_dir: Path | None) -> Path | None: |
| if models_dir is None: |
| return None |
| p = models_dir / f"{int(spec_id)}.xml" |
| return p if p.is_file() else None |
|
|
|
|
| def main() -> int: |
| ap = argparse.ArgumentParser(description=__doc__) |
| ap.add_argument("--csv", type=Path, default=ROOT / "datasets" / "query_translation_eval.csv") |
| ap.add_argument("--pred", type=Path, required=True, help="Baseline trans_query.txt") |
| ap.add_argument( |
| "--gold-models-dir", |
| type=Path, |
| default=None, |
| help="Directory with 1.xml .. 10.xml (must match spec_id in CSV for --verifyta)", |
| ) |
| ap.add_argument("--verifyta", action="store_true", help="Run verifyta (needs pyuppaal + verifyta)") |
| ap.add_argument("--json-out", type=Path, default=None) |
| args = ap.parse_args() |
|
|
| rows = load_eval_csv(args.csv.resolve()) |
| preds = parse_trans_query_file(args.pred.resolve()) |
|
|
| if len(preds) != len(rows): |
| print( |
| f"Count mismatch: CSV has {len(rows)} rows, parsed {len(preds)} predictions from {args.pred}", |
| file=sys.stderr, |
| ) |
| return 1 |
|
|
| if args.verifyta and args.gold_models_dir is None: |
| print("--verifyta requires --gold-models-dir", file=sys.stderr) |
| return 1 |
| if args.verifyta and ModelCheckingPipeline is None: |
| print("Could not import ModelCheckingPipeline", file=sys.stderr) |
| return 1 |
|
|
| checkers: dict[str, Any] = {} |
| if args.verifyta and args.gold_models_dir: |
| for r in rows: |
| sid = str(int(r["spec_id"])) |
| if sid in checkers: |
| continue |
| xm = resolve_model_path(sid, args.gold_models_dir.resolve()) |
| if xm is None: |
| print(f"Missing model for spec_id={sid}: {args.gold_models_dir / (sid + '.xml')}", file=sys.stderr) |
| return 1 |
| checkers[sid] = ModelCheckingPipeline(str(xm)) |
|
|
| per_row: list[dict[str, Any]] = [] |
| tot_exact = 0 |
| tot_exact_csv = 0 |
| tot_f1 = 0.0 |
| tot_f1_csv = 0.0 |
| sem_ok = 0 |
| sem_att = 0 |
| csv_agree = 0 |
| csv_att = 0 |
| gold_parse_fail = 0 |
|
|
| for i, row in enumerate(rows): |
| gold_q = (row.get("ground_query") or "").strip() |
| gold_ref = adapt_csv_gold_to_reference_xml(gold_q) |
| nl = (row.get("nl_query") or "").strip() |
| spec_id = str(int(row["spec_id"])) |
| pred = preds[i] |
| ex_ref = normalize_query(pred) == normalize_query(gold_ref) |
| ex_csv = normalize_query(pred) == normalize_query(gold_q) |
| if ex_ref: |
| tot_exact += 1 |
| if ex_csv: |
| tot_exact_csv += 1 |
| prec, rec, f1 = token_f1(pred, gold_ref) |
| prec_c, rec_c, f1_c = token_f1(pred, gold_q) |
| tot_f1 += f1 |
| tot_f1_csv += f1_c |
|
|
| rec_out: dict[str, Any] = { |
| "index": i + 1, |
| "spec_id": spec_id, |
| "nl_query": nl, |
| "ground_query": gold_q, |
| "ground_query_adapted_ref_xml": gold_ref, |
| "pred_query": pred, |
| "exact_match": ex_ref, |
| "exact_match_dataset_csv": ex_csv, |
| "token_precision": prec, |
| "token_recall": rec, |
| "token_f1": f1, |
| "token_precision_dataset_csv": prec_c, |
| "token_recall_dataset_csv": rec_c, |
| "token_f1_dataset_csv": f1_c, |
| } |
|
|
| if args.verifyta: |
| ch = checkers[spec_id] |
| g_res, _gt, g_err = ch.verify(gold_ref) |
| p_res, _pt, p_err = ch.verify(pred) |
| g_ver = parse_verifyta_text_verdict(g_res, errors=g_err) |
| p_ver = parse_verifyta_text_verdict(p_res, errors=p_err) |
| sem = ( |
| g_ver == p_ver |
| and g_ver in ("satisfied", "not_satisfied") |
| and p_ver in ("satisfied", "not_satisfied") |
| ) |
| if g_ver not in ("satisfied", "not_satisfied"): |
| gold_parse_fail += 1 |
| if g_ver in ("satisfied", "not_satisfied") and p_ver in ("satisfied", "not_satisfied"): |
| sem_att += 1 |
| if sem: |
| sem_ok += 1 |
|
|
| exp = _csv_answer_to_verdict(row.get("answer") or "") |
| rec_out["gold_verdict"] = g_ver |
| rec_out["pred_verdict"] = p_ver |
| rec_out["semantic_correct"] = sem |
| rec_out["gold_errors"] = (g_err or [])[:2] |
| rec_out["pred_errors"] = (p_err or [])[:2] |
| if exp is not None and p_ver in ("satisfied", "not_satisfied"): |
| csv_att += 1 |
| if p_ver == exp: |
| csv_agree += 1 |
| rec_out["csv_answer_agree"] = p_ver == exp |
|
|
| per_row.append(rec_out) |
|
|
| n = len(rows) |
| summary = { |
| "csv": str(args.csv), |
| "pred": str(args.pred), |
| "gold_models_dir": str(args.gold_models_dir) if args.gold_models_dir else None, |
| "n": n, |
| "exact_match_rate": tot_exact / n, |
| "exact_match_rate_dataset_csv": tot_exact_csv / n, |
| "mean_token_f1": tot_f1 / n, |
| "mean_token_f1_dataset_csv": tot_f1_csv / n, |
| "verifyta": bool(args.verifyta), |
| } |
| if args.verifyta: |
| summary["semantic_correct_rate"] = sem_ok / sem_att if sem_att else None |
| summary["semantic_compared"] = sem_att |
| summary["csv_answer_agree_rate"] = csv_agree / csv_att if csv_att else None |
| summary["gold_verdict_fail_count"] = gold_parse_fail |
|
|
| print(json.dumps(summary, indent=2)) |
| if args.json_out: |
| args.json_out.parent.mkdir(parents=True, exist_ok=True) |
| out_obj = {"summary": summary, "rows": per_row} |
| args.json_out.write_text(json.dumps(out_obj, indent=2, ensure_ascii=False), encoding="utf-8") |
| print(f"Wrote {args.json_out}", file=sys.stderr) |
|
|
| return 0 |
|
|
|
|
| if __name__ == "__main__": |
| raise SystemExit(main()) |
|
|