diff --git a/4-Infrastructure/shim/compare_tier1_vs_tier2.py b/4-Infrastructure/shim/compare_tier1_vs_tier2.py new file mode 100644 index 00000000..9b016cd5 --- /dev/null +++ b/4-Infrastructure/shim/compare_tier1_vs_tier2.py @@ -0,0 +1,194 @@ +#!/usr/bin/env python3 +"""Compare Tier 1 hash-spectra vs Tier 2 proof-path spectra on independent labels. + +Reads: + - shared-data/pist_trace_tier2b_vectors.jsonl (Tier 2B spectral features) + - shared-data/pist_canary_ground_truth_labels.jsonl (independent labels) + - shared-data/pist_canary_ground_truth_report.json (Tier 1 baseline) + +Outputs: + - shared-data/pist_tier1_vs_tier2_comparison.json +""" +import json +import os +import sys +from collections import Counter, defaultdict +from math import sqrt + +VECTORS_PATH = os.path.join(os.path.dirname(__file__), "../..", + "shared-data/pist_trace_tier2b_vectors.jsonl") +LABELS_PATH = os.path.join(os.path.dirname(__file__), "../..", + "shared-data/pist_trace_v2_ground_truth_labels.jsonl") +TIER1_PATH = os.path.join(os.path.dirname(__file__), "../..", + "shared-data/pist_canary_ground_truth_report.json") +OUT_PATH = os.path.join(os.path.dirname(__file__), "../..", + "shared-data/pist_tier1_vs_tier2_comparison.json") + + +def normalize(vectors): + n = len(vectors) + if n == 0: return vectors, [], [] + dim = len(vectors[0]) + means = [sum(v[i] for v in vectors) / n for i in range(dim)] + stds = [sqrt(sum((v[i] - means[i])**2 for v in vectors) / max(n-1,1)) for i in range(dim)] + stds = [s if s > 1e-9 else 1.0 for s in stds] + return [[(v[i] - means[i]) / stds[i] for i in range(dim)] for v in vectors], means, stds + + +def centroid(vecs): + return [sum(v[i] for v in vecs) / len(vecs) for i in range(len(vecs[0]))] if vecs else [] + + +def euclidean(a, b): + return sqrt(sum((a[i] - b[i])**2 for i in range(len(a)))) + + +def eval_loocv(vectors, labels, k=3): + n = len(vectors) + correct = 0 + top2 = 0 + confusion = defaultdict(lambda: defaultdict(int)) + for i in range(n): + tv = vectors[:i] + vectors[i+1:] + tl = labels[:i] + labels[i+1:] + tv_v = test_v = vectors[i] + test_l = labels[i] + cls_vecs = defaultdict(list) + for v, l in zip(tv, tl): + cls_vecs[l].append(v) + cents = {l: centroid(vecs) for l, vecs in cls_vecs.items()} + preds = sorted(cents.keys(), key=lambda l: euclidean(test_v, cents[l])) + pred = preds[0] + if pred == test_l: correct += 1 + if test_l in preds[:2]: top2 += 1 + acc = correct / n + return acc, top2 / n, max(Counter(labels).values()) / n + + +BUILTIN_FEATURES = ["matrix_size", "rank", "spectral_gap", "laplacian_zero_count", "density", "eigenvalue_max"] + + +def main(): + # Load Tier 2B vectors + t2_records = {} + with open(VECTORS_PATH) as f: + for line in f: + r = json.loads(line) + t2_records[r["name"]] = r + print(f"Tier 2 vectors: {len(t2_records)}", flush=True) + + # Load ground-truth labels + labels = {} + with open(LABELS_PATH) as f: + for line in f: + lbl = json.loads(line) + labels[lbl["theorem_name"]] = lbl + print(f"Labels: {len(labels)}", flush=True) + + # Load Tier 1 report for baseline comparison + tier1_baselines = {} + try: + with open(TIER1_PATH) as f: + t1 = json.load(f) + for target_key, target_label in t1.get("targets", {}).items(): + for method in ["centroid", "knn_3"]: + key = f"{target_key}_{method}" + if key in t1.get("results", {}): + tier1_baselines[key] = t1["results"][key]["accuracy"] + except FileNotFoundError: + pass + print(f"Tier 1 baselines: {len(tier1_baselines)} targets", flush=True) + + # Align records by name + aligned = [(k, v) for k, v in t2_records.items() if k in labels] + print(f"Aligned: {len(aligned)}", flush=True) + + # Build feature vectors + t2_vectors = [] + t2_names = [] + for name, rec in aligned: + vec = [rec.get(f, 0) for f in BUILTIN_FEATURES] + t2_vectors.append(vec) + t2_names.append(name) + + t2_norm, _, _ = normalize(t2_vectors) + print(f"Tier 2 feature dim: {len(BUILTIN_FEATURES)}", flush=True) + + TARGETS = [ + ("proof_status", "proof_status"), + ("proof_method_label", "proof method"), + ("domain_label", "domain"), + ("manual_rrc_shape", "manual RRCShape"), + ] + + results = {} + print(f"\n{'='*70}", flush=True) + print("TIER 2 VS TIER 1 COMPARISON", flush=True) + print(f"{'='*70}", flush=True) + print(f"\n{'Target':30s} {'Method':12s} {'Tier 2':>8} {'Tier 1':>8} {'Majority':>8} {'Improves':>10}", + flush=True) + print(f"{'-'*30} {'-'*12} {'-'*8} {'-'*8} {'-'*8} {'-'*10}", flush=True) + + for key, label in TARGETS: + targets = [] + for name in t2_names: + val = labels[name].get(key, "unknown") or "none" + targets.append(val) + + dist = Counter(targets) + majority_baseline = max(dist.values()) / len(targets) + print(f"\n{label:30s} distribution: {dict(dist.most_common(3))}", flush=True) + + for method_name, method_key in [("centroid", "centroid"), ("knn_3", "knn_3")]: + acc, top2, majority = eval_loocv(t2_norm, targets, 3 if method_key != "centroid" else 1) + + t1_key = f"{key}_{method_key}" + tier1_acc = tier1_baselines.get(t1_key, None) + + improves = "YES" if tier1_acc is not None and acc > tier1_acc else ("NO" if tier1_acc is not None else "N/A") + + print(f" {label:28s} {method_name:12s} " + f"{acc:8.1%} {tier1_acc or 0:8.1%} {majority:8.1%} {improves:>10s}", + flush=True) + + results[f"{key}_{method_key}"] = { + "tier2_accuracy": round(acc, 4), + "tier2_top2": round(top2, 4), + "tier1_accuracy": round(tier1_acc, 4) if tier1_acc else None, + "majority_baseline": round(majority, 4), + "tier2_beats_tier1": acc > (tier1_acc or 0), + "improves_over_baseline": round((acc - majority) / max(majority, 0.01), 3), + "n_samples": len(targets), + "distribution": dict(dist), + } + + # Print summary + print(f"\n{'='*70}", flush=True) + print("SUMMARY: Does Tier 2 beat Tier 1?", flush=True) + print(f"{'='*70}", flush=True) + wins = sum(1 for k, v in results.items() if v.get("tier2_beats_tier1")) + total = sum(1 for k, v in results.items() if v.get("tier1_accuracy") is not None) + print(f"Tier 2 wins: {wins}/{total} targets", flush=True) + for k, v in sorted(results.items()): + if v.get("tier1_accuracy") is not None: + comp = "BEATS" if v["tier2_accuracy"] > v["tier1_accuracy"] else "behind" + print(f" {k:35s} T2={v['tier2_accuracy']:.1%} T1={v['tier1_accuracy']:.1%} ({comp})", flush=True) + + # Save + report = { + "n_samples": len(aligned), + "tier2_accuracy": {"proof_status": results.get("proof_status_centroid", {}).get("tier2_accuracy", 0)}, + "results": results, + "conclusion": { + "tier2_wins": wins, + "total_comparable": total, + } + } + with open(OUT_PATH, "w") as f: + json.dump(report, f, indent=2) + print(f"\nReport: {OUT_PATH}", flush=True) + return 0 + + +if __name__ == "__main__": + main() diff --git a/shared-data/pist_tier1_vs_tier2_comparison.json b/shared-data/pist_tier1_vs_tier2_comparison.json new file mode 100644 index 00000000..487f5984 --- /dev/null +++ b/shared-data/pist_tier1_vs_tier2_comparison.json @@ -0,0 +1,150 @@ +{ + "n_samples": 24, + "tier2_accuracy": { + "proof_status": 0.7083 + }, + "results": { + "proof_status_centroid": { + "tier2_accuracy": 0.7083, + "tier2_top2": 1.0, + "tier1_accuracy": null, + "majority_baseline": 0.8333, + "tier2_beats_tier1": true, + "improves_over_baseline": -0.15, + "n_samples": 24, + "distribution": { + "verified": 20, + "failed": 4 + } + }, + "proof_status_knn_3": { + "tier2_accuracy": 0.7083, + "tier2_top2": 1.0, + "tier1_accuracy": null, + "majority_baseline": 0.8333, + "tier2_beats_tier1": true, + "improves_over_baseline": -0.15, + "n_samples": 24, + "distribution": { + "verified": 20, + "failed": 4 + } + }, + "proof_method_label_centroid": { + "tier2_accuracy": 0.2083, + "tier2_top2": 0.25, + "tier1_accuracy": 0.0952, + "majority_baseline": 0.2083, + "tier2_beats_tier1": true, + "improves_over_baseline": 0.0, + "n_samples": 24, + "distribution": { + "apply": 2, + "ring": 1, + "cases": 2, + "constructor": 1, + "rfl": 2, + "rewrite": 5, + "omega": 5, + "have": 1, + "induction": 3, + "simp": 1, + "intro": 1 + } + }, + "proof_method_label_knn_3": { + "tier2_accuracy": 0.2083, + "tier2_top2": 0.25, + "tier1_accuracy": 0.0714, + "majority_baseline": 0.2083, + "tier2_beats_tier1": true, + "improves_over_baseline": 0.0, + "n_samples": 24, + "distribution": { + "apply": 2, + "ring": 1, + "cases": 2, + "constructor": 1, + "rfl": 2, + "rewrite": 5, + "omega": 5, + "have": 1, + "induction": 3, + "simp": 1, + "intro": 1 + } + }, + "domain_label_centroid": { + "tier2_accuracy": 0.625, + "tier2_top2": 0.75, + "tier1_accuracy": 0.1905, + "majority_baseline": 0.3333, + "tier2_beats_tier1": true, + "improves_over_baseline": 0.875, + "n_samples": 24, + "distribution": { + "logic": 7, + "algebra": 2, + "type_error": 2, + "arithmetic": 8, + "order": 3, + "equality": 2 + } + }, + "domain_label_knn_3": { + "tier2_accuracy": 0.625, + "tier2_top2": 0.75, + "tier1_accuracy": 0.3095, + "majority_baseline": 0.3333, + "tier2_beats_tier1": true, + "improves_over_baseline": 0.875, + "n_samples": 24, + "distribution": { + "logic": 7, + "algebra": 2, + "type_error": 2, + "arithmetic": 8, + "order": 3, + "equality": 2 + } + }, + "manual_rrc_shape_centroid": { + "tier2_accuracy": 0.6667, + "tier2_top2": 0.9167, + "tier1_accuracy": 0.381, + "majority_baseline": 0.2917, + "tier2_beats_tier1": true, + "improves_over_baseline": 1.286, + "n_samples": 24, + "distribution": { + "LogogramProjection": 7, + "SignalShapedRouteCompiler": 4, + "HoldForUnlawfulOrUnderspecifiedShape": 5, + "ProjectableGeometryTopology": 3, + "CognitiveLoadField": 1, + "CadForceProbeReceipt": 4 + } + }, + "manual_rrc_shape_knn_3": { + "tier2_accuracy": 0.6667, + "tier2_top2": 0.9167, + "tier1_accuracy": 0.3333, + "majority_baseline": 0.2917, + "tier2_beats_tier1": true, + "improves_over_baseline": 1.286, + "n_samples": 24, + "distribution": { + "LogogramProjection": 7, + "SignalShapedRouteCompiler": 4, + "HoldForUnlawfulOrUnderspecifiedShape": 5, + "ProjectableGeometryTopology": 3, + "CognitiveLoadField": 1, + "CadForceProbeReceipt": 4 + } + } + }, + "conclusion": { + "tier2_wins": 8, + "total_comparable": 6 + } +} \ No newline at end of file diff --git a/shared-data/pist_trace_v2_ground_truth_labels.jsonl b/shared-data/pist_trace_v2_ground_truth_labels.jsonl new file mode 100644 index 00000000..77dc7492 --- /dev/null +++ b/shared-data/pist_trace_v2_ground_truth_labels.jsonl @@ -0,0 +1,24 @@ +{"theorem_name": "rw_chain_eq", "proof_status": "verified", "proof_method_label": "rewrite", "domain_label": "equality", "joint_label": "equality_chaining_2step", "obstruction_label": null, "manual_rrc_shape": "CadForceProbeReceipt", "label_confidence": "auto"} +{"theorem_name": "rw_chain_mixed", "proof_status": "verified", "proof_method_label": "rewrite", "domain_label": "arithmetic", "joint_label": "rw_then_simp", "obstruction_label": null, "manual_rrc_shape": "CadForceProbeReceipt", "label_confidence": "auto"} +{"theorem_name": "rw_chain_3step", "proof_status": "verified", "proof_method_label": "rewrite", "domain_label": "equality", "joint_label": "equality_chaining_3step", "obstruction_label": null, "manual_rrc_shape": "CadForceProbeReceipt", "label_confidence": "auto"} +{"theorem_name": "rw_then_omega", "proof_status": "verified", "proof_method_label": "rewrite", "domain_label": "arithmetic", "joint_label": "rw_then_arithmetic", "obstruction_label": null, "manual_rrc_shape": "CadForceProbeReceipt", "label_confidence": "auto"} +{"theorem_name": "cases_or_swap", "proof_status": "verified", "proof_method_label": "cases", "domain_label": "logic", "joint_label": "disjunction_swap", "obstruction_label": null, "manual_rrc_shape": "LogogramProjection", "label_confidence": "auto"} +{"theorem_name": "cases_and_elim", "proof_status": "verified", "proof_method_label": "cases", "domain_label": "logic", "joint_label": "conjunction_elim_then_apply", "obstruction_label": null, "manual_rrc_shape": "LogogramProjection", "label_confidence": "auto"} +{"theorem_name": "constructor_example", "proof_status": "verified", "proof_method_label": "constructor", "domain_label": "logic", "joint_label": "conjunction_intro", "obstruction_label": null, "manual_rrc_shape": "LogogramProjection", "label_confidence": "auto"} +{"theorem_name": "apply_chain", "proof_status": "verified", "proof_method_label": "apply", "domain_label": "logic", "joint_label": "implication_chaining", "obstruction_label": null, "manual_rrc_shape": "LogogramProjection", "label_confidence": "auto"} +{"theorem_name": "omega_chain_ineq", "proof_status": "verified", "proof_method_label": "omega", "domain_label": "order", "joint_label": "transitivity_closure", "obstruction_label": null, "manual_rrc_shape": "SignalShapedRouteCompiler", "label_confidence": "auto"} +{"theorem_name": "omega_reorder_sum", "proof_status": "verified", "proof_method_label": "omega", "domain_label": "arithmetic", "joint_label": "reorder_summands", "obstruction_label": null, "manual_rrc_shape": "SignalShapedRouteCompiler", "label_confidence": "auto"} +{"theorem_name": "omega_distrib", "proof_status": "verified", "proof_method_label": "omega", "domain_label": "algebra", "joint_label": "distributivity", "obstruction_label": null, "manual_rrc_shape": "SignalShapedRouteCompiler", "label_confidence": "auto"} +{"theorem_name": "omega_chain_unsat", "proof_status": "verified", "proof_method_label": "omega", "domain_label": "order", "joint_label": "unsatisfiable_linear", "obstruction_label": "unsatisfiable_goal", "manual_rrc_shape": "HoldForUnlawfulOrUnderspecifiedShape", "label_confidence": "auto"} +{"theorem_name": "induct_add_zero", "proof_status": "verified", "proof_method_label": "induction", "domain_label": "arithmetic", "joint_label": "inductive_proof", "obstruction_label": null, "manual_rrc_shape": "ProjectableGeometryTopology", "label_confidence": "auto"} +{"theorem_name": "induct_add_succ", "proof_status": "verified", "proof_method_label": "induction", "domain_label": "arithmetic", "joint_label": "inductive_succ", "obstruction_label": null, "manual_rrc_shape": "ProjectableGeometryTopology", "label_confidence": "auto"} +{"theorem_name": "induct_mul_zero", "proof_status": "verified", "proof_method_label": "induction", "domain_label": "arithmetic", "joint_label": "inductive_mul", "obstruction_label": null, "manual_rrc_shape": "ProjectableGeometryTopology", "label_confidence": "auto"} +{"theorem_name": "induct_factorial", "proof_status": "verified", "proof_method_label": "simp", "domain_label": "arithmetic", "joint_label": "definitional_unfold", "obstruction_label": null, "manual_rrc_shape": "CognitiveLoadField", "label_confidence": "auto"} +{"theorem_name": "intro_all", "proof_status": "verified", "proof_method_label": "intro", "domain_label": "logic", "joint_label": "multiple_introductions", "obstruction_label": null, "manual_rrc_shape": "LogogramProjection", "label_confidence": "auto"} +{"theorem_name": "intro_apply", "proof_status": "verified", "proof_method_label": "apply", "domain_label": "logic", "joint_label": "intro_then_apply", "obstruction_label": null, "manual_rrc_shape": "LogogramProjection", "label_confidence": "auto"} +{"theorem_name": "have_chain", "proof_status": "verified", "proof_method_label": "have", "domain_label": "logic", "joint_label": "lemma_chaining", "obstruction_label": null, "manual_rrc_shape": "LogogramProjection", "label_confidence": "auto"} +{"theorem_name": "calc_chain", "proof_status": "verified", "proof_method_label": "ring", "domain_label": "algebra", "joint_label": "ring_then_omega", "obstruction_label": null, "manual_rrc_shape": "SignalShapedRouteCompiler", "label_confidence": "auto"} +{"theorem_name": "fail_type_mismatch", "proof_status": "failed", "proof_method_label": "rfl", "domain_label": "type_error", "joint_label": "type_mismatch", "obstruction_label": "type_mismatch", "manual_rrc_shape": "HoldForUnlawfulOrUnderspecifiedShape", "label_confidence": "auto"} +{"theorem_name": "fail_missing_lemma", "proof_status": "failed", "proof_method_label": "rewrite", "domain_label": "arithmetic", "joint_label": "missing_dependency", "obstruction_label": "missing_lemma", "manual_rrc_shape": "HoldForUnlawfulOrUnderspecifiedShape", "label_confidence": "auto"} +{"theorem_name": "fail_unsat", "proof_status": "failed", "proof_method_label": "omega", "domain_label": "order", "joint_label": "contradictory_goal", "obstruction_label": "unsatisfiable_goal", "manual_rrc_shape": "HoldForUnlawfulOrUnderspecifiedShape", "label_confidence": "auto"} +{"theorem_name": "fail_bad_coercion", "proof_status": "failed", "proof_method_label": "rfl", "domain_label": "type_error", "joint_label": "coercion_mismatch", "obstruction_label": "type_mismatch", "manual_rrc_shape": "HoldForUnlawfulOrUnderspecifiedShape", "label_confidence": "auto"}