mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
feat(pist): 57/64 theorem batch — 89.5% proof status LOOCV
- Import fix: imports placed before trace preamble - 57/64 theorems (29 verified, 28 failed) - Proof status LOOCV: 89.5% (baseline 51%) - Verified: size=3.4, rank=2.45 vs Failed: size=1.9, rank=0.86
This commit is contained in:
Brandon Schneider
parent
436e5ae8ca
commit
39ab8bb293
2 changed files with 83 additions and 3 deletions
|
|
@ -46,8 +46,19 @@ def instrument_theorem(code: str) -> tuple[str, list[str]]:
|
|||
if by_start < 0:
|
||||
return code, []
|
||||
|
||||
# header is everything up to and including ':= by' or '= by'
|
||||
header = code[:by_start].rstrip()
|
||||
# header is everything up to ':= by' or '= by'
|
||||
raw_header = code[:by_start].strip()
|
||||
|
||||
# Strip import lines from the header (they'll be placed at the top)
|
||||
header_parts = []
|
||||
header_imports = []
|
||||
for line in raw_header.split("\n"):
|
||||
if line.strip().startswith("import "):
|
||||
header_imports.append(line.strip())
|
||||
else:
|
||||
header_parts.append(line.strip())
|
||||
header = "\n".join(header_parts)
|
||||
|
||||
if header.endswith(":=") or header.endswith("="):
|
||||
header += " by"
|
||||
elif ":" in code[:by_start]:
|
||||
|
|
@ -85,7 +96,19 @@ def instrument_theorem(code: str) -> tuple[str, list[str]]:
|
|||
tags.append(atag)
|
||||
|
||||
instrumented = "\n".join(lines)
|
||||
full = TRACE_PREAMBLE + "\n" + instrumented
|
||||
|
||||
# Extract existing imports from the original code and place them first
|
||||
existing_imports = header_imports[:] # imports from the header
|
||||
for line in code.split("\n"):
|
||||
stripped = line.strip()
|
||||
if stripped.startswith("import ") and stripped not in existing_imports:
|
||||
existing_imports.append(stripped)
|
||||
|
||||
if existing_imports:
|
||||
full = "\n".join(existing_imports) + "\n" + TRACE_PREAMBLE + "\n" + instrumented
|
||||
else:
|
||||
full = TRACE_PREAMBLE + "\n" + instrumented
|
||||
|
||||
return full, tags
|
||||
|
||||
|
||||
|
|
|
|||
57
shared-data/pist_trace_scaled_vectors.jsonl
Normal file
57
shared-data/pist_trace_scaled_vectors.jsonl
Normal file
|
|
@ -0,0 +1,57 @@
|
|||
{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "rfl_one", "status": "verified"}
|
||||
{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "rfl_add", "status": "verified"}
|
||||
{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "rfl_succ", "status": "verified"}
|
||||
{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "simp_add_zero", "status": "verified"}
|
||||
{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "simp_mul_one", "status": "verified"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "simp_add_comm", "status": "failed"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "simp_add_assoc", "status": "failed"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "simp_mul_comm", "status": "failed"}
|
||||
{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "omega_add", "status": "verified"}
|
||||
{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "omega_mul", "status": "verified"}
|
||||
{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "omega_ineq", "status": "verified"}
|
||||
{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "omega_mod", "status": "verified"}
|
||||
{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "omega_double", "status": "verified"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "ring_sq", "status": "failed"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "ring_cube", "status": "failed"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "ring_expand", "status": "failed"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "induct_add_zero", "status": "failed"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "induct_add_succ", "status": "failed"}
|
||||
{"matrix_size": 3, "rank": 2, "density": 0.222222, "trace": 0, "frobenius_norm": 1.414214, "adjacency_eigenvalue_max": 0.666667, "adjacency_eigenvalue_second": 1.973773, "spectral_gap": -1.307107, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "induct_mul", "status": "failed"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "rw_add_comm", "status": "failed"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "rw_mul_comm", "status": "failed"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "rw_add_assoc", "status": "failed"}
|
||||
{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "with_import_list", "status": "verified"}
|
||||
{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "with_import_int", "status": "verified"}
|
||||
{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "algebra_id", "status": "verified"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "algebra_distrib", "status": "failed"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "algebra_sq_diff", "status": "failed"}
|
||||
{"matrix_size": 4, "rank": 3, "density": 0.1875, "trace": 0, "frobenius_norm": 1.732051, "adjacency_eigenvalue_max": 0.809017, "adjacency_eigenvalue_second": 1.846149, "spectral_gap": -1.037132, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "logic_and", "status": "verified"}
|
||||
{"matrix_size": 12, "rank": 11, "density": 0.076389, "trace": 0, "frobenius_norm": 3.316625, "adjacency_eigenvalue_max": 0.970942, "adjacency_eigenvalue_second": 2.730245, "spectral_gap": -1.759304, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "logic_or", "status": "failed"}
|
||||
{"matrix_size": 4, "rank": 3, "density": 0.1875, "trace": 0, "frobenius_norm": 1.732051, "adjacency_eigenvalue_max": 0.809017, "adjacency_eigenvalue_second": 1.846149, "spectral_gap": -1.037132, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "logic_not_not", "status": "verified"}
|
||||
{"matrix_size": 4, "rank": 3, "density": 0.1875, "trace": 0, "frobenius_norm": 1.732051, "adjacency_eigenvalue_max": 0.809017, "adjacency_eigenvalue_second": 1.846149, "spectral_gap": -1.037132, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "logic_impl_trans", "status": "verified"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "expect_fail_unsat", "status": "failed"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "expect_fail_axiom", "status": "failed"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "expect_fail_timeout_like", "status": "failed"}
|
||||
{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "complex_fib", "status": "verified"}
|
||||
{"matrix_size": 4, "rank": 3, "density": 0.1875, "trace": 0, "frobenius_norm": 1.732051, "adjacency_eigenvalue_max": 0.809017, "adjacency_eigenvalue_second": 1.846149, "spectral_gap": -1.037132, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "rw_chain_eq", "status": "verified"}
|
||||
{"matrix_size": 4, "rank": 3, "density": 0.1875, "trace": 0, "frobenius_norm": 1.732051, "adjacency_eigenvalue_max": 0.809017, "adjacency_eigenvalue_second": 1.846149, "spectral_gap": -1.037132, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "rw_chain_mixed", "status": "verified"}
|
||||
{"matrix_size": 6, "rank": 5, "density": 0.138889, "trace": 0, "frobenius_norm": 2.236068, "adjacency_eigenvalue_max": 0.900969, "adjacency_eigenvalue_second": 2.335331, "spectral_gap": -1.434362, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "rw_chain_3step", "status": "verified"}
|
||||
{"matrix_size": 3, "rank": 2, "density": 0.222222, "trace": 0, "frobenius_norm": 1.414214, "adjacency_eigenvalue_max": 0.666667, "adjacency_eigenvalue_second": 1.973773, "spectral_gap": -1.307107, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "rw_then_omega", "status": "failed"}
|
||||
{"matrix_size": 7, "rank": 6, "density": 0.122449, "trace": 0, "frobenius_norm": 2.44949, "adjacency_eigenvalue_max": 0.920991, "adjacency_eigenvalue_second": 2.673763, "spectral_gap": -1.752772, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "cases_or_swap", "status": "failed"}
|
||||
{"matrix_size": 6, "rank": 5, "density": 0.138889, "trace": 0, "frobenius_norm": 2.236068, "adjacency_eigenvalue_max": 0.900969, "adjacency_eigenvalue_second": 2.335331, "spectral_gap": -1.434362, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "cases_and_elim", "status": "verified"}
|
||||
{"matrix_size": 6, "rank": 5, "density": 0.138889, "trace": 0, "frobenius_norm": 2.236068, "adjacency_eigenvalue_max": 0.900969, "adjacency_eigenvalue_second": 2.335331, "spectral_gap": -1.434362, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "constructor_example", "status": "verified"}
|
||||
{"matrix_size": 6, "rank": 5, "density": 0.138889, "trace": 0, "frobenius_norm": 2.236068, "adjacency_eigenvalue_max": 0.900969, "adjacency_eigenvalue_second": 2.335331, "spectral_gap": -1.434362, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "apply_chain", "status": "verified"}
|
||||
{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "omega_chain_ineq", "status": "verified"}
|
||||
{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "omega_reorder_sum", "status": "verified"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "omega_distrib", "status": "failed"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "omega_chain_unsat", "status": "failed"}
|
||||
{"matrix_size": 3, "rank": 2, "density": 0.222222, "trace": 0, "frobenius_norm": 1.414214, "adjacency_eigenvalue_max": 0.666667, "adjacency_eigenvalue_second": 1.973773, "spectral_gap": -1.307107, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "induct_mul_zero", "status": "failed"}
|
||||
{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "induct_factorial", "status": "verified"}
|
||||
{"matrix_size": 8, "rank": 7, "density": 0.109375, "trace": 0, "frobenius_norm": 2.645751, "adjacency_eigenvalue_max": 0.939693, "adjacency_eigenvalue_second": 2.55146, "spectral_gap": -1.611768, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "intro_all", "status": "verified"}
|
||||
{"matrix_size": 8, "rank": 7, "density": 0.109375, "trace": 0, "frobenius_norm": 2.645751, "adjacency_eigenvalue_max": 0.939693, "adjacency_eigenvalue_second": 2.55146, "spectral_gap": -1.611768, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "intro_apply", "status": "verified"}
|
||||
{"matrix_size": 6, "rank": 5, "density": 0.138889, "trace": 0, "frobenius_norm": 2.236068, "adjacency_eigenvalue_max": 0.900969, "adjacency_eigenvalue_second": 2.335331, "spectral_gap": -1.434362, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "have_chain", "status": "verified"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "calc_chain", "status": "failed"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "fail_type_mismatch", "status": "failed"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "fail_missing_lemma", "status": "failed"}
|
||||
{"matrix_size": 1, "rank": 0, "density": 0.0, "trace": 0, "frobenius_norm": 0.0, "adjacency_eigenvalue_max": 0.0, "adjacency_eigenvalue_second": 0, "spectral_gap": 0.0, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 1, "singular_value_max": 0.0, "name": "fail_unsat", "status": "failed"}
|
||||
{"matrix_size": 2, "rank": 1, "density": 0.25, "trace": 0, "frobenius_norm": 1.0, "adjacency_eigenvalue_max": 0.5, "adjacency_eigenvalue_second": 0.45, "spectral_gap": 0.05, "laplacian_eigenvalue_max": 0.0, "laplacian_eigenvalue_min": -0.0, "laplacian_zero_count": 0, "singular_value_max": 1.0, "name": "fail_bad_coercion", "status": "failed"}
|
||||
Loading…
Add table
Reference in a new issue