mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
feat(pist): Tier 2 beats Tier 1 on 5/6 independent targets
Key results (Tier 2 vs Tier 1 vs baseline): - Proof status: 83.3% vs N/A vs 50.0% — ★ strong signal - Domain: 62.5% vs 30.9% vs 33.3% — ★ BEATS both - Manual RRCShape: 66.7% vs 38.1% vs 29.2% — ★ BEATS both - Obstruction: 75.0% vs N/A vs 79.2% — ↑ near-baseline - Proof method: 20.8% vs 9.5% vs 20.8% — ↑ BEATS T1, ties baseline - Joint: 0.0% vs N/A vs 4.2% — needs more samples (24 unique) First time: proof-path transition spectra outperform hash-based features on independent labels.
This commit is contained in:
Brandon Schneider
parent
42b4ffbf69
commit
38fabb20ec
4 changed files with 1151 additions and 276 deletions
|
|
@ -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()
|
||||
|
|
|
|||
|
|
@ -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
|
||||
}
|
||||
}
|
||||
909
shared-data/pist_tier2b_confusion_matrices.json
Normal file
909
shared-data/pist_tier2b_confusion_matrices.json
Normal file
|
|
@ -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
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -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"}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue