allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat(pist): Tier 2 beats Tier 1 on every independent target

Browse source 
- Domain: 62.5% vs 19.1% (baseline 33.3%) — BEATS both
- RRCShape: 66.7% vs 38.1% (baseline 29.2%) — BEATS both
- Proof method: 20.8% vs 9.5% (baseline 20.8%) — BEATS T1
- Proof status: 70.8% — useful signal
- 8/8 targets: Tier 2 outperforms Tier 1
- First proof-path spectra that beat hash-based features
This commit is contained in:
Brandon Schneider 2026-05-26 03:10:22 -05:00
parent df3e37d263
commit d86c73b774
3 changed files with 368 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

194
4-Infrastructure/shim/compare_tier1_vs_tier2.py Normal file
View file

@ -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()

150
shared-data/pist_tier1_vs_tier2_comparison.json Normal file
View file

@ -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
}
}

24
shared-data/pist_trace_v2_ground_truth_labels.jsonl Normal file
View file

@ -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"}