diff --git a/4-Infrastructure/shim/compare_tier1_vs_tier2.py b/4-Infrastructure/shim/compare_tier1_vs_tier2.py index 9b016cd5..0bd34d7a 100644 --- a/4-Infrastructure/shim/compare_tier1_vs_tier2.py +++ b/4-Infrastructure/shim/compare_tier1_vs_tier2.py @@ -1,14 +1,5 @@ #!/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 -""" +"""Compare Tier 1 vs Tier 2 on independent labels — with alignment check + full reporting.""" import json import os import sys @@ -19,176 +10,185 @@ 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") +COMPARISON_PATH = os.path.join(os.path.dirname(__file__), "../..", + "shared-data/pist_tier1_vs_tier2_comparison.json") +CONFUSION_PATH = os.path.join(os.path.dirname(__file__), "../..", + "shared-data/pist_tier2b_confusion_matrices.json") +def load_jsonl(path): + rows = [] + with open(path) as f: + for line in f: + rows.append(json.loads(line)) + return rows 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 = [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): +def eval_loocv(vectors, labels): 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"] + results = {} + for method, k in [("centroid", 1), ("knn_1", 1), ("knn_3", 3)]: + correct = 0; top2 = 0; conf = defaultdict(lambda: defaultdict(int)) + for i in range(n): + tv = vectors[:i] + vectors[i+1:] + tl = labels[:i] + labels[i+1:] + test_v = vectors[i]; test_l = labels[i] + if method == "centroid": + 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] + else: + dists = [(euclidean(test_v, tv[j]), tl[j]) for j in range(len(tv))] + dists.sort(key=lambda x: x[0]) + votes = Counter(tl for _, tl in dists[:k]) + pred = votes.most_common(1)[0][0] + preds = [t[1] for t in dists[:2]] + conf[test_l][pred] += 1 + if pred == test_l: correct += 1 + if test_l in preds[:2]: top2 += 1 + cls = sorted(set(labels)) + results[method] = { + "accuracy": round(correct / n, 4), + "top2_accuracy": round(top2 / n, 4), + "confusion": {gt: {p: conf[gt][p] for p in cls} for gt in cls}, + } + return results +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) + t2 = load_jsonl(VECTORS_PATH) + labels = load_jsonl(LABELS_PATH) - # 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) + t2_map = {r["name"]: r for r in t2} + lmap = {r["theorem_name"]: r for r in labels} - # 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) + t2_names, label_names = set(t2_map), set(lmap) + matched = sorted(t2_names & label_names) + print(f"Tier 2 vectors: {len(t2_names)}", flush=True) + print(f"Labels: {len(label_names)}", flush=True) + print(f"Matched: {len(matched)}", flush=True) + missing_l = sorted(t2_names - label_names) + missing_v = sorted(label_names - t2_names) + if missing_l: print(f"Missing labels: {missing_l}", flush=True) + if missing_v: print(f"Missing vectors: {missing_v}", flush=True) + if len(matched) != len(t2_names): + print(f"WARNING: Only {len(matched)}/{len(t2_names)} vectors have labels", flush=True) + if len(matched) < 3: + print("Too few aligned samples. Aborting.", flush=True) + return 1 - # 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) + # Build vectors + vecs = [] + for name in matched: + r = t2_map[name] + vecs.append([r.get(f, 0) for f in FEATURES]) + normed, _, _ = normalize(vecs) TARGETS = [ ("proof_status", "proof_status"), ("proof_method_label", "proof method"), ("domain_label", "domain"), + ("joint_label", "joint"), + ("obstruction_label", "obstruction"), ("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) + all_results = {} + confusion_matrices = {} + + print(f"\n{'='*80}", flush=True) + print("TIER 2 PROOF-PATH SPECTRA — LABEL COMPARISON", flush=True) + print(f"{'='*80}", flush=True) + print(f"\n{'Target':30s} {'Method':12s} {'Acc':>6} {'Top-2':>6} {'Base':>6} {'Classes':>8} {'Samples':>8}", flush=True) + print(f"{'-'*30} {'-'*12} {'-'*6} {'-'*6} {'-'*6} {'-'*8} {'-'*8}", flush=True) for key, label in TARGETS: targets = [] - for name in t2_names: - val = labels[name].get(key, "unknown") or "none" + for name in matched: + val = lmap[name].get(key, "none") + if val is None: val = "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) + classes = sorted(dist.keys()) + base = max(dist.values()) / len(targets) + print(f"\n{label:30s} distribution: {dict(dist.most_common(5))}", 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), + res = eval_loocv(normed, targets) + all_results[key] = {} + for method in ["centroid", "knn_1", "knn_3"]: + r = res[method] + all_results[key][method] = { + "accuracy": r["accuracy"], + "top2_accuracy": r["top2_accuracy"], + "baseline": round(base, 4), } + print(f" {label:28s} {method:12s} {r['accuracy']:6.1%} {r['top2_accuracy']:6.1%} " + f"{base:6.1%} {len(classes):8d} {len(targets):8d}", flush=True) - # 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) + confusion_matrices[key] = res["centroid"]["confusion"] - # Save + # Read Tier 1 baselines if available + t1 = {} + try: + with open(os.path.join(os.path.dirname(__file__), "../..", + "shared-data/pist_canary_ground_truth_report.json")) as f: + t1d = json.load(f) + for tk, tl in [("proof_method_label", "proof_method"), + ("domain_label", "domain"), + ("manual_rrc_shape", "manual RRCShape")]: + for m in ["centroid", "knn_3"]: + k = f"{tk}_{m}" + if k in t1d.get("results", {}): + t1[k] = t1d["results"][k].get("accuracy", 0) + except: pass + + # Summary comparison table + print(f"\n{'='*80}", flush=True) + print("SUMMARY: Tier 2 vs Tier 1 vs Majority Baseline", flush=True) + print(f"{'='*80}", flush=True) + print(f"\n{'Target':25s} {'T2 best':>8} {'T1 best':>8} {'Baseline':>8} {'Verdict':>12}", flush=True) + print(f"{'-'*25} {'-'*8} {'-'*8} {'-'*8} {'-'*12}", flush=True) + for key, label in TARGETS: + t2_best = max(all_results.get(key, {}).get(m, {}).get("accuracy", 0) for m in ["centroid", "knn_3"]) + t1_best = max((t1.get(f"{key}_centroid", 0), t1.get(f"{key}_knn_3", 0)), default=0) + base = all_results.get(key, {}).get("centroid", {}).get("baseline", 0) + verdict = "★ BEATS" if t2_best > t1_best and t2_best > base else \ + "↑ T2>T1" if t2_best > t1_best else \ + "→ ties" if abs(t2_best - base) < 0.05 else "↓ below" + print(f"{label:25s} {t2_best:8.1%} {t1_best:8.1%} {base:8.1%} {verdict:>12s}", flush=True) + + # Save comparison 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, - } + "n_samples": len(matched), + "n_features": len(FEATURES), + "tier2_results": all_results, + "tier1_baselines": t1, } - with open(OUT_PATH, "w") as f: + with open(COMPARISON_PATH, "w") as f: json.dump(report, f, indent=2) - print(f"\nReport: {OUT_PATH}", flush=True) - return 0 + print(f"\nComparison: {COMPARISON_PATH}", flush=True) + with open(CONFUSION_PATH, "w") as f: + json.dump(confusion_matrices, f, indent=2) + print(f"Confusion: {CONFUSION_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 index 487f5984..a0bec998 100644 --- a/shared-data/pist_tier1_vs_tier2_comparison.json +++ b/shared-data/pist_tier1_vs_tier2_comparison.json @@ -1,150 +1,116 @@ { "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 + "n_features": 6, + "tier2_results": { + "proof_status": { + "centroid": { + "accuracy": 0.6667, + "top2_accuracy": 1.0, + "baseline": 0.5 + }, + "knn_1": { + "accuracy": 0.7917, + "top2_accuracy": 0.9167, + "baseline": 0.5 + }, + "knn_3": { + "accuracy": 0.8333, + "top2_accuracy": 0.9167, + "baseline": 0.5 } }, - "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": { + "accuracy": 0.2083, + "top2_accuracy": 0.25, + "baseline": 0.2083 + }, + "knn_1": { + "accuracy": 0.2083, + "top2_accuracy": 0.2083, + "baseline": 0.2083 + }, + "knn_3": { + "accuracy": 0.125, + "top2_accuracy": 0.2083, + "baseline": 0.2083 } }, - "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 + "domain_label": { + "centroid": { + "accuracy": 0.625, + "top2_accuracy": 0.75, + "baseline": 0.3333 + }, + "knn_1": { + "accuracy": 0.5, + "top2_accuracy": 0.5833, + "baseline": 0.3333 + }, + "knn_3": { + "accuracy": 0.5417, + "top2_accuracy": 0.5833, + "baseline": 0.3333 } }, - "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 + "joint_label": { + "centroid": { + "accuracy": 0.0, + "top2_accuracy": 0.0, + "baseline": 0.0417 + }, + "knn_1": { + "accuracy": 0.0, + "top2_accuracy": 0.0, + "baseline": 0.0417 + }, + "knn_3": { + "accuracy": 0.0, + "top2_accuracy": 0.0, + "baseline": 0.0417 } }, - "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 + "obstruction_label": { + "centroid": { + "accuracy": 0.5833, + "top2_accuracy": 0.7917, + "baseline": 0.7917 + }, + "knn_1": { + "accuracy": 0.625, + "top2_accuracy": 0.75, + "baseline": 0.7917 + }, + "knn_3": { + "accuracy": 0.75, + "top2_accuracy": 0.75, + "baseline": 0.7917 } }, - "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 + "manual_rrc_shape": { + "centroid": { + "accuracy": 0.6667, + "top2_accuracy": 0.9167, + "baseline": 0.2917 + }, + "knn_1": { + "accuracy": 0.5417, + "top2_accuracy": 0.7083, + "baseline": 0.2917 + }, + "knn_3": { + "accuracy": 0.5833, + "top2_accuracy": 0.7083, + "baseline": 0.2917 } } }, - "conclusion": { - "tier2_wins": 8, - "total_comparable": 6 + "tier1_baselines": { + "proof_method_label_centroid": 0.0952, + "proof_method_label_knn_3": 0.0714, + "domain_label_centroid": 0.1905, + "domain_label_knn_3": 0.3095, + "manual_rrc_shape_centroid": 0.381, + "manual_rrc_shape_knn_3": 0.3333 } } \ No newline at end of file diff --git a/shared-data/pist_tier2b_confusion_matrices.json b/shared-data/pist_tier2b_confusion_matrices.json new file mode 100644 index 00000000..b76c3714 --- /dev/null +++ b/shared-data/pist_tier2b_confusion_matrices.json @@ -0,0 +1,909 @@ +{ + "proof_status": { + "failed": { + "failed": 7, + "verified": 5 + }, + "verified": { + "failed": 3, + "verified": 9 + } + }, + "proof_method_label": { + "apply": { + "apply": 0, + "cases": 0, + "constructor": 1, + "have": 0, + "induction": 0, + "intro": 1, + "omega": 0, + "rewrite": 0, + "rfl": 0, + "ring": 0, + "simp": 0 + }, + "cases": { + "apply": 1, + "cases": 0, + "constructor": 1, + "have": 0, + "induction": 0, + "intro": 0, + "omega": 0, + "rewrite": 0, + "rfl": 0, + "ring": 0, + "simp": 0 + }, + "constructor": { + "apply": 0, + "cases": 0, + "constructor": 0, + "have": 1, + "induction": 0, + "intro": 0, + "omega": 0, + "rewrite": 0, + "rfl": 0, + "ring": 0, + "simp": 0 + }, + "have": { + "apply": 0, + "cases": 0, + "constructor": 1, + "have": 0, + "induction": 0, + "intro": 0, + "omega": 0, + "rewrite": 0, + "rfl": 0, + "ring": 0, + "simp": 0 + }, + "induction": { + "apply": 0, + "cases": 0, + "constructor": 0, + "have": 0, + "induction": 3, + "intro": 0, + "omega": 0, + "rewrite": 0, + "rfl": 0, + "ring": 0, + "simp": 0 + }, + "intro": { + "apply": 1, + "cases": 0, + "constructor": 0, + "have": 0, + "induction": 0, + "intro": 0, + "omega": 0, + "rewrite": 0, + "rfl": 0, + "ring": 0, + "simp": 0 + }, + "omega": { + "apply": 0, + "cases": 0, + "constructor": 0, + "have": 0, + "induction": 0, + "intro": 0, + "omega": 0, + "rewrite": 0, + "rfl": 0, + "ring": 3, + "simp": 2 + }, + "rewrite": { + "apply": 0, + "cases": 0, + "constructor": 1, + "have": 0, + "induction": 1, + "intro": 0, + "omega": 0, + "rewrite": 2, + "rfl": 0, + "ring": 1, + "simp": 0 + }, + "rfl": { + "apply": 0, + "cases": 0, + "constructor": 0, + "have": 0, + "induction": 0, + "intro": 0, + "omega": 0, + "rewrite": 0, + "rfl": 0, + "ring": 1, + "simp": 1 + }, + "ring": { + "apply": 0, + "cases": 0, + "constructor": 0, + "have": 0, + "induction": 0, + "intro": 0, + "omega": 1, + "rewrite": 0, + "rfl": 0, + "ring": 0, + "simp": 0 + }, + "simp": { + "apply": 0, + "cases": 0, + "constructor": 0, + "have": 0, + "induction": 0, + "intro": 0, + "omega": 0, + "rewrite": 0, + "rfl": 1, + "ring": 0, + "simp": 0 + } + }, + "domain_label": { + "algebra": { + "algebra": 2, + "arithmetic": 0, + "equality": 0, + "logic": 0, + "order": 0, + "type_error": 0 + }, + "arithmetic": { + "algebra": 1, + "arithmetic": 6, + "equality": 1, + "logic": 0, + "order": 0, + "type_error": 0 + }, + "equality": { + "algebra": 0, + "arithmetic": 1, + "equality": 0, + "logic": 1, + "order": 0, + "type_error": 0 + }, + "logic": { + "algebra": 0, + "arithmetic": 0, + "equality": 0, + "logic": 7, + "order": 0, + "type_error": 0 + }, + "order": { + "algebra": 2, + "arithmetic": 1, + "equality": 0, + "logic": 0, + "order": 0, + "type_error": 0 + }, + "type_error": { + "algebra": 1, + "arithmetic": 1, + "equality": 0, + "logic": 0, + "order": 0, + "type_error": 0 + } + }, + "joint_label": { + "coercion_mismatch": { + "coercion_mismatch": 0, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 1, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 0, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 0, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 0, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "conjunction_elim_then_apply": { + "coercion_mismatch": 0, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 1, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 0, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 0, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "conjunction_intro": { + "coercion_mismatch": 0, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 1, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 0, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 0, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "contradictory_goal": { + "coercion_mismatch": 0, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 0, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 0, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 1, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "definitional_unfold": { + "coercion_mismatch": 1, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 0, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 0, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 0, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "disjunction_swap": { + "coercion_mismatch": 0, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 0, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 0, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 1, + "reorder_summands": 0, + "ring_then_omega": 0, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "distributivity": { + "coercion_mismatch": 0, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 0, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 0, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 1, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "equality_chaining_2step": { + "coercion_mismatch": 0, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 0, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 0, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 0, + "rw_then_arithmetic": 0, + "rw_then_simp": 1, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "equality_chaining_3step": { + "coercion_mismatch": 0, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 1, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 0, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 0, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "implication_chaining": { + "coercion_mismatch": 0, + "conjunction_elim_then_apply": 1, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 0, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 0, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 0, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "inductive_mul": { + "coercion_mismatch": 0, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 0, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 1, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 0, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "inductive_proof": { + "coercion_mismatch": 0, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 0, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 1, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 0, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "inductive_succ": { + "coercion_mismatch": 0, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 0, + "inductive_mul": 0, + "inductive_proof": 1, + "inductive_succ": 0, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 0, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "intro_then_apply": { + "coercion_mismatch": 0, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 0, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 0, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 1, + "reorder_summands": 0, + "ring_then_omega": 0, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "lemma_chaining": { + "coercion_mismatch": 0, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 1, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 0, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 0, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "missing_dependency": { + "coercion_mismatch": 0, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 0, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 0, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 1, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "multiple_introductions": { + "coercion_mismatch": 0, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 0, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 0, + "intro_then_apply": 1, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 0, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "reorder_summands": { + "coercion_mismatch": 1, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 0, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 0, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 0, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "ring_then_omega": { + "coercion_mismatch": 0, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 0, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 0, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 1, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 0, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "rw_then_arithmetic": { + "coercion_mismatch": 0, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 0, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 1, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 0, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "rw_then_simp": { + "coercion_mismatch": 0, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 1, + "equality_chaining_3step": 0, + "implication_chaining": 0, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 0, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 0, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "transitivity_closure": { + "coercion_mismatch": 1, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 0, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 0, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 0, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "type_mismatch": { + "coercion_mismatch": 0, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 0, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 0, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 1, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + }, + "unsatisfiable_linear": { + "coercion_mismatch": 0, + "conjunction_elim_then_apply": 0, + "conjunction_intro": 0, + "contradictory_goal": 0, + "definitional_unfold": 0, + "disjunction_swap": 0, + "distributivity": 0, + "equality_chaining_2step": 0, + "equality_chaining_3step": 0, + "implication_chaining": 0, + "inductive_mul": 0, + "inductive_proof": 0, + "inductive_succ": 0, + "intro_then_apply": 0, + "lemma_chaining": 0, + "missing_dependency": 0, + "multiple_introductions": 0, + "reorder_summands": 0, + "ring_then_omega": 1, + "rw_then_arithmetic": 0, + "rw_then_simp": 0, + "transitivity_closure": 0, + "type_mismatch": 0, + "unsatisfiable_linear": 0 + } + }, + "obstruction_label": { + "missing_lemma": { + "missing_lemma": 0, + "none": 0, + "type_mismatch": 0, + "unsatisfiable_goal": 1 + }, + "none": { + "missing_lemma": 2, + "none": 14, + "type_mismatch": 3, + "unsatisfiable_goal": 0 + }, + "type_mismatch": { + "missing_lemma": 1, + "none": 1, + "type_mismatch": 0, + "unsatisfiable_goal": 0 + }, + "unsatisfiable_goal": { + "missing_lemma": 2, + "none": 0, + "type_mismatch": 0, + "unsatisfiable_goal": 0 + } + }, + "manual_rrc_shape": { + "CadForceProbeReceipt": { + "CadForceProbeReceipt": 2, + "CognitiveLoadField": 0, + "HoldForUnlawfulOrUnderspecifiedShape": 0, + "LogogramProjection": 1, + "ProjectableGeometryTopology": 1, + "SignalShapedRouteCompiler": 0 + }, + "CognitiveLoadField": { + "CadForceProbeReceipt": 0, + "CognitiveLoadField": 0, + "HoldForUnlawfulOrUnderspecifiedShape": 0, + "LogogramProjection": 0, + "ProjectableGeometryTopology": 0, + "SignalShapedRouteCompiler": 1 + }, + "HoldForUnlawfulOrUnderspecifiedShape": { + "CadForceProbeReceipt": 0, + "CognitiveLoadField": 1, + "HoldForUnlawfulOrUnderspecifiedShape": 4, + "LogogramProjection": 0, + "ProjectableGeometryTopology": 0, + "SignalShapedRouteCompiler": 0 + }, + "LogogramProjection": { + "CadForceProbeReceipt": 0, + "CognitiveLoadField": 0, + "HoldForUnlawfulOrUnderspecifiedShape": 0, + "LogogramProjection": 7, + "ProjectableGeometryTopology": 0, + "SignalShapedRouteCompiler": 0 + }, + "ProjectableGeometryTopology": { + "CadForceProbeReceipt": 0, + "CognitiveLoadField": 0, + "HoldForUnlawfulOrUnderspecifiedShape": 0, + "LogogramProjection": 0, + "ProjectableGeometryTopology": 3, + "SignalShapedRouteCompiler": 0 + }, + "SignalShapedRouteCompiler": { + "CadForceProbeReceipt": 0, + "CognitiveLoadField": 2, + "HoldForUnlawfulOrUnderspecifiedShape": 2, + "LogogramProjection": 0, + "ProjectableGeometryTopology": 0, + "SignalShapedRouteCompiler": 0 + } + } +} \ 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 index 77dc7492..12d4f530 100644 --- a/shared-data/pist_trace_v2_ground_truth_labels.jsonl +++ b/shared-data/pist_trace_v2_ground_truth_labels.jsonl @@ -1,23 +1,23 @@ {"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": "rw_then_omega", "proof_status": "failed", "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": "failed", "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": "omega_distrib", "proof_status": "failed", "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": "failed", "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": "failed", "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": "failed", "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": "failed", "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": "calc_chain", "proof_status": "failed", "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"}