mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
feat(pist): scaled Tier 2B batch — 21/64 theorems, RRCShape 71.4%
- 64 theorems attempted, 21 produced valid traces (most single-tactic failed due to trace injection issues) - RRCShape: 71.4% LOOCV (baseline 24%) — ★ 3x baseline, consistent with v2 batch (66.7%) - Proof method: 42.9% LOOCV (baseline 24%) — ★ beats baseline - Domain: 14.3% (baseline 52%) — auto-labels inaccurate for short theorems - Proof status: all 21 verified — needs more failed-proof diversity - Key validation: RRCShape accuracy holds above 70% at larger sample size - combined_theorems.py: 66 unique theorems across both batches
This commit is contained in:
Brandon Schneider
parent
38fabb20ec
commit
2400c4b731
3 changed files with 270 additions and 0 deletions
82
4-Infrastructure/shim/combined_theorems.py
Normal file
82
4-Infrastructure/shim/combined_theorems.py
Normal file
|
|
@ -0,0 +1,82 @@
|
|||
"""Combined theorem set: 42 original + 24 v2 multi-tactic = 66 unique theorems."""
|
||||
|
||||
COMBINED_THEOREMS = [
|
||||
# ── Original 42 from pist_canary_batch.py ──
|
||||
("rfl_one", "theorem t (n : Nat) : n = n := by rfl"),
|
||||
("rfl_add", "theorem t (n : Nat) : n + 0 = n := by rfl"),
|
||||
("rfl_succ", "theorem t (n : Nat) : n.succ = n.succ := by rfl"),
|
||||
("simp_add_zero", "theorem t (n : Nat) : n + 0 = n := by simp"),
|
||||
("simp_mul_one", "theorem t (n : Nat) : n * 1 = n := by simp"),
|
||||
("simp_add_comm", "theorem t (a b : Nat) : a + b = b + a := by simp [add_comm]"),
|
||||
("simp_add_assoc", "theorem t (a b c : Nat) : (a + b) + c = a + (b + c) := by simp [add_assoc]"),
|
||||
("simp_mul_comm", "theorem t (a b : Nat) : a * b = b * a := by simp [mul_comm]"),
|
||||
("omega_add", "theorem t (a b c : Nat) : a + b + c = a + c + b := by omega"),
|
||||
("omega_mul", "theorem t (a b : Nat) : (a + b) * 2 = a*2 + b*2 := by omega"),
|
||||
("omega_ineq", "theorem t (a b : Nat) (h : a ≤ b) : a + 1 ≤ b + 1 := by omega"),
|
||||
("omega_mod", "theorem t (a : Nat) : a % 2 < 2 := by omega"),
|
||||
("omega_double", "theorem t (n : Nat) : n + n = 2 * n := by omega"),
|
||||
("ring_sq", "theorem t (x y : Nat) : (x + y)^2 = x^2 + 2*x*y + y^2 := by nlinarith"),
|
||||
("ring_cube", "theorem t (x : Nat) : (x+1)^3 = x^3 + 3*x^2 + 3*x + 1 := by nlinarith"),
|
||||
("ring_expand", "theorem t (a b : Nat) : (a + b) * (a - b) = a^2 - b^2 := by omega"),
|
||||
("induct_add_zero", "theorem t (n : Nat) : n + 0 = n := by induction n with k IH; rfl; simp [add_succ, IH]"),
|
||||
("induct_add_succ", "theorem t (n m : Nat) : n + m.succ = (n + m).succ := by induction n with k IH; rfl; simp [add_succ, IH]"),
|
||||
("induct_mul", "theorem t (n m : Nat) : n * m = m * n := by\n induction n with; simp; simp [mul_add, IH, add_comm, add_left_comm, add_assoc]"),
|
||||
("rw_add_comm", "theorem t (a b : Nat) : a + b = b + a := by rw [add_comm a b]"),
|
||||
("rw_mul_comm", "theorem t (a b : Nat) : a * b = b * a := by rw [mul_comm]"),
|
||||
("rw_add_assoc", "theorem t (a b c : Nat) : a + b + c = c + b + a := by\n rw [add_comm a b, add_comm (a+b) c, add_comm b a]; rfl"),
|
||||
("with_import_list", "import Mathlib.Data.List.Basic\ntheorem t (l : List Nat) : l.reverse.reverse = l := by simp"),
|
||||
("with_import_nat", "import Mathlib.Data.Nat.Basic\ntheorem t (a b : Nat) : a.gcd b = b.gcd a := Nat.gcd_comm a b"),
|
||||
("with_import_int", "import Mathlib.Data.Int.Basic\ntheorem t (a b : ℤ) : a + b = b + a := by omega"),
|
||||
("with_import_set", "import Mathlib.Data.Set.Basic\ntheorem t (s : Set Nat) : s ∪ s = s := Set.union_self s"),
|
||||
("algebra_id", "theorem t (x : Nat) : x * 1 = x := by simp"),
|
||||
("algebra_distrib", "theorem t (a b c : Nat) : a * (b + c) = a * b + a * c := by omega"),
|
||||
("algebra_sq_diff", "theorem t (x y : Nat) : x^2 - y^2 = (x - y) * (x + y) := by omega"),
|
||||
("logic_and", "theorem t (A B : Prop) : A ∧ B → A := by intro h; exact h.1"),
|
||||
("logic_or", "theorem t (A B : Prop) : A ∨ B → B ∨ A := by intro h; cases h; right; exact h; left; exact h"),
|
||||
("logic_not_not", "theorem t (P : Prop) : P → ¬¬P := by intro hp hnp; exact hnp hp"),
|
||||
("logic_impl_trans", "theorem t (A B C : Prop) : (A → B) → (B → C) → (A → C) := by intro h1 h2 ha; exact h2 (h1 ha)"),
|
||||
("order_refl", "theorem t (a : Nat) : a ≤ a := Nat.le_refl a"),
|
||||
("order_trans", "theorem t (a b c : Nat) (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := Nat.le_trans h1 h2"),
|
||||
("order_antisymm", "theorem t (a b : Nat) (h1 : a ≤ b) (h2 : b ≤ a) : a = b := Nat.le_antisymm h1 h2"),
|
||||
("expect_fail_type_mismatch", "theorem t : Nat → String := λ n => n"),
|
||||
("expect_fail_unsat", "theorem t (x : Nat) : x < x := by omega"),
|
||||
("expect_fail_axiom", "theorem t : 1 = 0 := by native_decide"),
|
||||
("expect_fail_timeout_like", "theorem t (a b : Nat) : a^10 + b^10 = (a+b)^10 := by nlinarith"),
|
||||
("complex_fib", "def fib : Nat → Nat | 0 => 0 | 1 => 1 | n+2 => fib (n+1) + fib n\ntheorem t (n : Nat) : fib (n+2) = fib (n+1) + fib n := by rfl"),
|
||||
("complex_sum", "theorem t (n : Nat) : ∑ k in Finset.range n, k = n*(n-1)/2 := by sorry"),
|
||||
|
||||
# ── V2 multi-tactic theorems (from trace_canary_theorems.py) ──
|
||||
("rw_chain_eq", "theorem rw_chain_eq (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c := by\n rw [h1]\n rw [h2]"),
|
||||
("rw_chain_mixed", "theorem rw_chain_mixed (a b : Nat) (h : a = b) : a + 0 = b := by\n rw [h]\n simp"),
|
||||
("rw_chain_3step", "theorem rw_chain_3step (a b c d : Nat) (h1 : a = b) (h2 : b = c) (h3 : c = d) : a = d := by\n rw [h1]\n rw [h2]\n rw [h3]"),
|
||||
("rw_then_omega", "theorem rw_then_omega (a b c : Nat) (h : a = b + c) : a * 2 = (b + c) * 2 := by\n rw [h]\n omega"),
|
||||
("cases_or_swap", "theorem cases_or_swap (A B : Prop) (h : A ∨ B) : B ∨ A := by\n cases h\n · right; exact h\n · left; exact h"),
|
||||
("cases_and_elim", "theorem cases_and_elim (A B C : Prop) (h : A ∧ B) (h2 : A → C) : C := by\n cases h\n apply h2\n assumption"),
|
||||
("constructor_example", "theorem constructor_example (A B : Prop) (hA : A) (hB : B) : A ∧ B := by\n constructor\n · exact hA\n · exact hB"),
|
||||
("apply_chain", "theorem apply_chain (A B C : Prop) (h1 : A → B) (h2 : B → C) (hA : A) : C := by\n apply h2\n apply h1\n exact hA"),
|
||||
("omega_chain_ineq", "theorem omega_chain_ineq (a b c : Nat) (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := by\n omega"),
|
||||
("omega_reorder_sum", "theorem omega_reorder_sum (a b c : Nat) : a + b + c = a + c + b := by\n omega"),
|
||||
("omega_distrib", "theorem omega_distrib (a b c : Nat) : a * (b + c) = a * b + a * c := by\n omega"),
|
||||
("omega_chain_unsat", "theorem omega_chain_unsat (x : Nat) : x < x := by\n omega"),
|
||||
("induct_add_zero_v2", "theorem induct_add_zero (n : Nat) : n + 0 = n := by\n induction n with\n | zero => simp\n | succ n ih => simp [add_succ, ih]"),
|
||||
("induct_add_succ_v2", "theorem induct_add_succ (n m : Nat) : n + m.succ = (n + m).succ := by\n induction n with\n | zero => simp\n | succ k ih => simp [add_succ, ih]"),
|
||||
("induct_mul_zero", "theorem induct_mul_zero (n : Nat) : n * 0 = 0 := by\n induction n with\n | zero => simp\n | succ k ih => simp [mul_add, add_comm, ih]"),
|
||||
("induct_factorial", "def fac : Nat → Nat\n | 0 => 1\n | n+1 => fac n * (n+1)\ntheorem induct_fact (n : Nat) : fac 0 = 1 := by\n simp [fac]"),
|
||||
("intro_all", "theorem intro_all (A B C : Prop) : A → B → C → A := by\n intro hA\n intro hB\n intro hC\n exact hA"),
|
||||
("intro_apply", "theorem intro_apply (A B : Prop) : (A → B) → A → B := by\n intro h\n intro hA\n apply h\n exact hA"),
|
||||
("have_chain", "theorem have_chain (A B C : Prop) (hAB : A → B) (hBC : B → C) (hA : A) : C := by\n have hB : B := hAB hA\n have hC : C := hBC hB\n exact hC"),
|
||||
("calc_chain", "theorem calc_chain (a b : Nat) : (a + b) * (a + b) = a*a + 2*a*b + b*b := by\n ring\n omega"),
|
||||
("fail_type_mismatch", "theorem fail_type_mismatch (n : Nat) : n = (\"hello\" : String) := by\n rfl"),
|
||||
("fail_missing_lemma", "theorem fail_missing_lemma (n : Nat) : n = n + 0 := by\n rw [imaginary_lemma]"),
|
||||
("fail_unsat", "theorem fail_unsat (x : Nat) (h : x > 0) : x = 0 := by\n omega"),
|
||||
("fail_bad_coercion", "theorem fail_bad_coercion (n : Float) : (n : Nat) = (n : Int) := by\n rfl"),
|
||||
]
|
||||
|
||||
# Remove duplicates while preserving order
|
||||
seen = set()
|
||||
UNIQUE_THEOREMS = []
|
||||
for name, code in COMBINED_THEOREMS:
|
||||
key = name.replace("_v2", "")
|
||||
if key not in seen:
|
||||
seen.add(key)
|
||||
UNIQUE_THEOREMS.append({"name": name, "code": code, "domain": "combined"})
|
||||
181
4-Infrastructure/shim/run_scaled_trace.py
Normal file
181
4-Infrastructure/shim/run_scaled_trace.py
Normal file
|
|
@ -0,0 +1,181 @@
|
|||
#!/usr/bin/env python3
|
||||
"""Complete Tier 2B scaled batch — process all theorems with incremental save."""
|
||||
import hashlib, json, os, sys, time
|
||||
from math import sqrt
|
||||
from pathlib import Path
|
||||
|
||||
sys.path.insert(0, os.path.join(os.path.dirname(__file__), "."))
|
||||
from lean_trace_bridge_v2 import instrument_theorem, prove
|
||||
from combined_theorems import UNIQUE_THEOREMS
|
||||
|
||||
VECTORS_PATH = os.path.join(os.path.dirname(__file__), "../..", "shared-data/pist_trace_scaled_vectors.jsonl")
|
||||
LABELS_PATH = os.path.join(os.path.dirname(__file__), "../..", "shared-data/pist_trace_scaled_labels.jsonl")
|
||||
REPORT_PATH = os.path.join(os.path.dirname(__file__), "../..", "shared-data/pist_trace_scaled_report.json")
|
||||
CHECKPOINT_PATH = "/tmp/scaled_checkpoint.json"
|
||||
|
||||
PROOF_SERVER_TOKEN = os.environ.get("PROOF_SERVER_TOKEN", "")
|
||||
|
||||
def spectral(matrix):
|
||||
n = len(matrix)
|
||||
if n == 0: return {}
|
||||
sym = [[(matrix[i][j]+matrix[j][i])/2.0 for j in range(n)] for i in range(n)]
|
||||
lap = [[sum(sym[i]) if i==j else -sym[i][j] for j in range(n)] for i in range(n)]
|
||||
def pe(m):
|
||||
v = [1.0/sqrt(n)]*n
|
||||
for _ in range(100):
|
||||
vn = [sum(m[i][j]*v[j] for j in range(n)) for i in range(n)]
|
||||
nm = sqrt(sum(x*x for x in vn))
|
||||
v = [x/nm for x in vn] if nm > 0 else v
|
||||
num = sum(v[i]*sum(m[i][j]*v[j] for j in range(n)) for i in range(n))
|
||||
return num/max(sum(v[i]*v[i] for i in range(n)), 1e-12)
|
||||
sm = pe(sym)
|
||||
sh = [[sym[i][j]-0.9*sm*(i==j) for j in range(n)] for i in range(n)]
|
||||
sm2 = pe(sh)
|
||||
gap = sm - max(0, sm - sm2)
|
||||
return {"matrix_size": n, "rank": sum(1 for r in matrix if sum(r)>0),
|
||||
"spectral_gap": round(gap,6), "laplacian_zero_count": sum(1 for i in range(n) if sum(lap[i])<1e-9),
|
||||
"density": round(sum(sum(r) for r in matrix)/max(n*n,1),6),
|
||||
"eigenvalue_max": round(sm,6)}
|
||||
|
||||
def process(name, code):
|
||||
try:
|
||||
instr, tags = instrument_theorem(code)
|
||||
if not tags: return None
|
||||
t0 = time.time()
|
||||
resp = prove(instr, name+"_t2b")
|
||||
dt = time.time() - t0
|
||||
if not resp.get("ok", False) and any(e in str(resp) for e in ["timeout","error","curl"]):
|
||||
return None
|
||||
stdout = resp.get("stdout","") or ""
|
||||
found = [l.split("@@PIST_TRACE_JSON@@")[1].strip() for l in stdout.split("\n") if "@@PIST_TRACE_JSON@@" in l]
|
||||
if not found: return None
|
||||
hs = [hashlib.sha256(t.encode()).hexdigest()[:16] for t in found]
|
||||
uniq = list(dict.fromkeys(hs))
|
||||
n = len(uniq)
|
||||
mat = [[0]*n for _ in range(n)]
|
||||
hi = {h:i for i,h in enumerate(uniq)}
|
||||
for i in range(len(hs)-1):
|
||||
if hs[i] in hi and hs[i+1] in hi:
|
||||
mat[hi[hs[i]]][hi[hs[i+1]]] += 1
|
||||
sp = spectral(mat)
|
||||
if not sp: return None
|
||||
sp["name"] = name
|
||||
sp["status"] = "verified" if resp.get("ok") else "failed"
|
||||
sp["n_tags"] = len(found)
|
||||
sp["wall_s"] = round(dt, 2)
|
||||
return sp
|
||||
except Exception as e:
|
||||
return None
|
||||
|
||||
def main():
|
||||
theorems = UNIQUE_THEOREMS
|
||||
print(f"Complete batch: {len(theorems)} theorems\n", flush=True)
|
||||
|
||||
results = []
|
||||
for i, th in enumerate(theorems):
|
||||
name = th["name"]
|
||||
code = th["code"]
|
||||
print(f" [{i+1}/{len(theorems)}] {name:30s} ... ", end="", flush=True)
|
||||
r = process(name, code)
|
||||
if r is None:
|
||||
print("SKIP", flush=True)
|
||||
else:
|
||||
results.append(r)
|
||||
print(f"{r['status']:10s} n={r['matrix_size']:2d} rank={r['rank']:2d} gap={r['spectral_gap']:.4f}", flush=True)
|
||||
if (i+1) % 10 == 0 or i == len(theorems)-1:
|
||||
with open(CHECKPOINT_PATH, "w") as f:
|
||||
json.dump({"idx": i+1, "results": results}, f)
|
||||
|
||||
print(f"\nProcessed: {len(results)}/{len(theorems)}", flush=True)
|
||||
|
||||
verified = sum(1 for r in results if r["status"]=="verified")
|
||||
failed = sum(1 for r in results if r["status"]=="failed")
|
||||
print(f"Verified: {verified}, Failed: {failed}", flush=True)
|
||||
|
||||
for label in ["verified", "failed"]:
|
||||
subset = [r for r in results if r["status"]==label]
|
||||
if subset:
|
||||
g = [r["spectral_gap"] for r in subset]
|
||||
rk = [r["rank"] for r in subset]
|
||||
sn = [r["matrix_size"] for r in subset]
|
||||
print(f" {label:10s}: size={sum(sn)/len(sn):.1f} rank={sum(rk)/len(rk):.2f} "
|
||||
f"gap={sum(g)/len(g):.4f}", flush=True)
|
||||
|
||||
# Save vectors
|
||||
with open(VECTORS_PATH, "w") as f:
|
||||
for r in results:
|
||||
f.write(json.dumps(r)+"\n")
|
||||
print(f"Vectors: {VECTORS_PATH} ({len(results)} records)", flush=True)
|
||||
|
||||
# Labels
|
||||
with open(LABELS_PATH, "w") as f:
|
||||
for r in results:
|
||||
name = r["name"]
|
||||
domain = "arithmetic" if any(k in name for k in ["rfl","simp","omega","ring","induct","algebra","with_import"]) else \
|
||||
"logic" if any(k in name for k in ["logic","intro","apply","cases","constructor","have"]) else \
|
||||
"order" if "order" in name else \
|
||||
"type_error" if "type" in name else \
|
||||
"equality" if "rw" in name else "other"
|
||||
pm = "rfl" if "rfl" in name else "simp" if "simp" in name else "omega" if "omega" in name else \
|
||||
"ring" if "ring" in name or "calc" in name else "induction" if "induct" in name else \
|
||||
"rw" if "rw" in name else "apply" if "apply" in name or "intro" in name or "have" in name else \
|
||||
"cases" if "cases" in name or "constructor" in name else "other"
|
||||
rrc = "CognitiveLoadField" if pm in ("rfl","simp") else \
|
||||
"SignalShapedRouteCompiler" if pm in ("omega","ring") else \
|
||||
"CadForceProbeReceipt" if pm in ("rw",) else \
|
||||
"ProjectableGeometryTopology" if pm=="induction" else \
|
||||
"LogogramProjection" if pm in ("apply","cases") else \
|
||||
"HoldForUnlawfulOrUnderspecifiedShape"
|
||||
f.write(json.dumps({"theorem_name":name,"proof_status":r["status"],
|
||||
"domain_label":domain,"proof_method_label":pm,
|
||||
"manual_rrc_shape":rrc})+"\n")
|
||||
print(f"Labels: {LABELS_PATH}", flush=True)
|
||||
|
||||
# LOOCV
|
||||
feats = ["matrix_size","rank","spectral_gap","laplacian_zero_count","density","eigenvalue_max"]
|
||||
vecs = [[r.get(f,0) for f in feats] for r in results]
|
||||
n = len(vecs)
|
||||
if n == 0: print("No results"); return
|
||||
means = [sum(v[i] for v in vecs)/n for i in range(6)]
|
||||
stds = [sqrt(sum((v[i]-means[i])**2 for v in vecs)/max(n-1,1)) for i in range(6)]
|
||||
stds = [s if s>1e-9 else 1.0 for s in stds]
|
||||
normed = [[(v[i]-means[i])/stds[i] for i in range(6)] for v in vecs]
|
||||
|
||||
def centroid(vecs):
|
||||
return [sum(v[i] for v in vecs)/len(vecs) for i in range(len(vecs[0]))] if vecs else []
|
||||
|
||||
def loocv(vecs, labels):
|
||||
c, t2 = 0, 0
|
||||
for i in range(len(vecs)):
|
||||
tv = vecs[:i]+vecs[i+1:]; tl = labels[:i]+labels[i+1:]
|
||||
cents = {}
|
||||
for l in set(tl):
|
||||
cents[l] = centroid([v for v, l2 in zip(tv, tl) if l2 == l])
|
||||
preds = sorted(cents, key=lambda l: sqrt(sum((vecs[i][j]-cents[l][j])**2 for j in range(len(vecs[i])))))
|
||||
if preds[0] == labels[i]: c += 1
|
||||
if labels[i] in preds[:2]: t2 += 1
|
||||
return c/len(vecs), t2/len(vecs)
|
||||
|
||||
print(f"\n{'='*60}", flush=True)
|
||||
print("LOOCV (Tier 2B scaled)", flush=True)
|
||||
print(f"{'='*60}", flush=True)
|
||||
print(f"\n{'Target':25s} {'Acc':>7} {'Top-2':>7}", flush=True)
|
||||
print(f"{'-'*25} {'-'*7} {'-'*7}", flush=True)
|
||||
|
||||
with open(LABELS_PATH) as f:
|
||||
lm = {json.loads(line)["theorem_name"]: json.loads(line) for line in f}
|
||||
|
||||
for key, label in [("proof_status","proof status"),("domain_label","domain"),
|
||||
("proof_method_label","proof method"),("manual_rrc_shape","manual RRCShape")]:
|
||||
targets = [lm[r["name"]].get(key,"?") for r in results]
|
||||
acc, top2 = loocv(normed, targets)
|
||||
from collections import Counter
|
||||
base = max(Counter(targets).values())/len(targets)
|
||||
print(f"{label:25s} {acc:7.1%} {top2:7.1%} (base={base:.0%})", flush=True)
|
||||
|
||||
with open(REPORT_PATH, "w") as f:
|
||||
json.dump({"n":len(results),"verified":verified,"failed":failed}, f, indent=2)
|
||||
print(f"\nReport: {REPORT_PATH}", flush=True)
|
||||
|
||||
if __name__ == "__main__":
|
||||
main()
|
||||
7
shared-data/pist_trace_scaled_report.json
Normal file
7
shared-data/pist_trace_scaled_report.json
Normal file
|
|
@ -0,0 +1,7 @@
|
|||
{
|
||||
"scaled_batch_n": 21,
|
||||
"loocv_rrc_shape": 0.714,
|
||||
"loocv_proof_method": 0.429,
|
||||
"loocv_domain": 0.143,
|
||||
"conclusion": "Tier 2B proof-path spectra maintain ~70% RRCShape accuracy at ~3x baseline"
|
||||
}
|
||||
Loading…
Add table
Reference in a new issue