Spaces:
Running
Running
File size: 4,530 Bytes
1bc7926 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 | """Standalone cumulative verifier for arXiv 2605.01702.
The verifier uses only the Python standard library. It checks the immutable
raw JSON summaries produced by formal Hugging Face CPU runs and exits nonzero
if any accepted result, independent check, or negative control regresses.
BLOCKED is an intentional theorem-level verdict, never a failed assertion.
"""
from __future__ import annotations
import json
import struct
from fractions import Fraction
from pathlib import Path
DATA = Path(__file__).resolve().parents[1] / "data"
def load(name: str) -> dict:
return json.loads((DATA / name).read_text(encoding="utf-8"))
def bits64(value: float) -> bytes:
return struct.pack(">d", value)
def verify_claim_1() -> None:
raw = load("claim1_full_network.json")
assert raw["verdict"] == "BLOCKED"
assert raw["network_depth"] >= 9
assert len(raw["rows"]) == len(raw["domain"]) == 6
assert all(row["value_exact"] and row["gradient_exact"] for row in raw["rows"])
assert raw["off_domain_controls_zero"] == 6
assert raw["indicator_matrix_identity_exact"]
assert raw["negative_control"]["mismatch_count"] == 6
assert raw["negative_control"]["fires"]
def verify_claim_2() -> None:
raw = load("claim2_activations.json")
expected = {"ReLU", "ELU", "GELU", "Swish", "Sigmoid", "tanh"}
assert raw["verdict"] == "BLOCKED"
assert {row["activation"] for row in raw["rows"]} == expected
assert all(all(row["condition2_bullets"]) for row in raw["rows"])
assert all(row["condition3_pass"] for row in raw["rows"])
assert all(row["analytic_autograd_agree"] for row in raw["rows"])
assert raw["negative_control"]["rejected"]
def verify_claim_3() -> None:
raw = load("claim3_theorem32.json")
linear = raw["linear_antisymmetric_family"]
assert raw["verdict"] == "BLOCKED"
assert raw["theorem_depth"] == 2 ** (8 + 1) + 2 * 23 + 11 == 569
assert raw["executed_padding_layers"] == 556
assert linear == {"values_exact": 60, "gradients_exact": 60, "evaluated": 60}
assert raw["negative_control"]["antisymmetry_violations"] == 30
assert raw["negative_control"]["rejected"]
assert len(raw["attempts"]) == 4
assert raw["falsification_route"]["target_antisymmetric"]
assert not raw["falsification_route"]["valid_falsification"]
def verify_claim_4() -> None:
raw = load("claim4_zero_gradient.json")
assert raw["verdict"] == "BLOCKED"
assert raw["evaluated"] == 48
assert raw["active_value_and_zero_gradient_exact"] == 48
assert raw["off_point_zero_zero_exact"] == 48
assert raw["composition_network_depth"] >= 9
assert raw["negative_control"]["target_gradient_lost"]
def verify_claim_5() -> None:
raw = load("claim5_zero_output_gradient.json")
assert raw["verdict"] == "BLOCKED"
assert raw["released_normalization_audit"]["active_exact"] == 0
assert raw["calibration"]["active_zero_output_target_gradient_exact"] == 24
assert raw["calibration"]["off_zero_zero_exact"] == 24
assert raw["calibration"]["correction"] == 0.5
assert raw["full_composition"]["values_exact"] == 6
assert raw["full_composition"]["gradients_exact"] == 6
assert raw["negative_control"]["fires"]
def verify_claim_6() -> None:
raw = load("claim6_raw.json")
triple = raw["triple"]
a, b, c = triple["a"], triple["b"], triple["c"]
left, right = (a * b) * c, a * (b * c)
assert raw["verdict"] == "VERIFIED"
assert bits64(left) != bits64(right)
assert bits64(left) == bits64(triple["left"])
assert bits64(right) == bits64(triple["right"])
exact_left = (Fraction.from_float(a) * Fraction.from_float(b)) * Fraction.from_float(c)
exact_right = Fraction.from_float(a) * (Fraction.from_float(b) * Fraction.from_float(c))
assert exact_left == exact_right
control = raw["negative_control"]
ca, cb, cc = control["operands"]
assert bits64((ca * cb) * cc) == bits64(ca * (cb * cc))
assert control["pass"] and not control["nonassociativity_detector_fires"]
def main() -> None:
checks = [
verify_claim_1,
verify_claim_2,
verify_claim_3,
verify_claim_4,
verify_claim_5,
verify_claim_6,
]
for number, check in enumerate(checks, start=1):
check()
verdict = "VERIFIED" if number == 6 else "BLOCKED"
print(f"claim={number} evidence_check=PASS theorem_verdict={verdict}")
print("cumulative_regression=PASS controls=PASS")
if __name__ == "__main__":
main()
|