Tabular Classification
Kernels
Joblib
Scikit-learn
kernel
governance
formulas
proof-status
lean4
lambda-aggregate
surrogate
doi:10.5281/zenodo.19944926
Instructions to use SZLHOLDINGS/szl-formulas with libraries, inference providers, notebooks, and local apps. Follow these links to get started.
- Libraries
- Kernels
How to use SZLHOLDINGS/szl-formulas with Kernels:
# !pip install kernels from kernels import get_kernel kernel = get_kernel("SZLHOLDINGS/szl-formulas") - Scikit-learn
How to use SZLHOLDINGS/szl-formulas with Scikit-learn:
from huggingface_hub import hf_hub_download import joblib model = joblib.load( hf_hub_download("SZLHOLDINGS/szl-formulas", "sklearn_model.joblib") ) # only load pickle files from sources you trust # read more about it here https://skops.readthedocs.io/en/stable/persistence.html - Notebooks
- Google Colab
- Kaggle
forge: ship REAL trained surrogate v1 for szl-formulas (model.joblib + receipt + scripts; honest card + provenance)
Browse files- MODEL_PROVENANCE.json +42 -14
- README.md +59 -1
- TRAINING_RECEIPT.json +158 -0
- model.joblib +3 -0
- scripts/eval.py +27 -0
- scripts/forge.py +254 -0
MODEL_PROVENANCE.json
CHANGED
|
@@ -3,10 +3,28 @@
|
|
| 3 |
"model": {
|
| 4 |
"id": "SZLHOLDINGS/szl-formulas",
|
| 5 |
"repository_type": "model",
|
| 6 |
-
"artifact_kind": "kernel-code-and-configuration",
|
| 7 |
-
"trained_weights_present":
|
| 8 |
-
"stdlib_only":
|
| 9 |
-
"torch_required": false
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 10 |
},
|
| 11 |
"source_of_record": {
|
| 12 |
"state": "VERIFIED_HF_SOURCE_OF_RECORD",
|
|
@@ -22,31 +40,41 @@
|
|
| 22 |
"verification": {
|
| 23 |
"tests": "17/17 passed",
|
| 24 |
"tests_basis": "MEASURED local python3 -m pytest run, stdlib-only, offline",
|
| 25 |
-
"falsifiability": "registry must be exactly 21; locked-proven set must be exactly 8; PROOF_STATUS must match the dataset verbatim and raises on unknown names;
|
| 26 |
},
|
| 27 |
"proof_status": {
|
| 28 |
"policy": "mirrored VERBATIM from SZLHOLDINGS/canonical-formulas-v1 (PROVEN/AXIOM/SORRY/CONJECTURE)",
|
| 29 |
"obligation_vs_locked": "a per-formula PROVEN(...) tag is an obligation-level label, NOT membership in the locked-proven canonical set",
|
| 30 |
"locked_proven_count": 8,
|
| 31 |
-
"locked_proven_ids": [
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 32 |
"locked_count_theorem": "locked_count_eight (no-axiom, szl-holdings/lutar-lean PROVEN_FORMULAS.md)",
|
| 33 |
-
"f_number_to_registry_mapping": "UNKNOWN
|
| 34 |
},
|
| 35 |
"lambda": {
|
| 36 |
-
"status": "Conjecture 1 (open)
|
| 37 |
"definition": "weighted geometric mean (D2)",
|
| 38 |
-
"composer_role": "ADVISORY only
|
| 39 |
},
|
| 40 |
"claims": {
|
| 41 |
-
"trained_model": "
|
| 42 |
"reproducible_build": "NOT_CLAIMED",
|
| 43 |
-
"weights_present": "
|
| 44 |
},
|
| 45 |
"limits": [
|
| 46 |
-
"
|
|
|
|
| 47 |
"The 21 formulas are pure/no-I/O; the composer performs no network access.",
|
| 48 |
"PROOF_STATUS labels are the dataset's obligation-level declarations, not upgraded here.",
|
| 49 |
"Locked-proven canonical set is fixed at exactly 8 and never inflated.",
|
| 50 |
-
"The composer's
|
| 51 |
]
|
| 52 |
-
}
|
|
|
|
| 3 |
"model": {
|
| 4 |
"id": "SZLHOLDINGS/szl-formulas",
|
| 5 |
"repository_type": "model",
|
| 6 |
+
"artifact_kind": "kernel-code-and-configuration + trained surrogate (model.joblib)",
|
| 7 |
+
"trained_weights_present": true,
|
| 8 |
+
"stdlib_only": false,
|
| 9 |
+
"torch_required": false,
|
| 10 |
+
"surrogate": {
|
| 11 |
+
"file": "model.joblib",
|
| 12 |
+
"sha256": "94cca70dc950fa957c0931ee80240c4369cab0ff8446ffbfedb483c3e2907698",
|
| 13 |
+
"role": "21-class formula identifier from call-trace observables \u2014 kernel remains sole ground truth",
|
| 14 |
+
"fidelity_MEASURED": {
|
| 15 |
+
"test_accuracy_21_class": 0.9709,
|
| 16 |
+
"mean_per_class_recall": 0.9709,
|
| 17 |
+
"blind_spot_classes_recall_lt_0.90": {
|
| 18 |
+
"bohr_complementarity_floor": 0.7778,
|
| 19 |
+
"fisher_rao_distance": 0.8889,
|
| 20 |
+
"pinsker_kl_bound": 0.8833,
|
| 21 |
+
"schur_concave_lambda_two_axis": 0.85
|
| 22 |
+
}
|
| 23 |
+
},
|
| 24 |
+
"receipt": "TRAINING_RECEIPT.json",
|
| 25 |
+
"reverify": "python scripts/eval.py"
|
| 26 |
+
},
|
| 27 |
+
"stdlib_only_note": "kernel package itself stays stdlib-only; the OPTIONAL surrogate needs sklearn+joblib"
|
| 28 |
},
|
| 29 |
"source_of_record": {
|
| 30 |
"state": "VERIFIED_HF_SOURCE_OF_RECORD",
|
|
|
|
| 40 |
"verification": {
|
| 41 |
"tests": "17/17 passed",
|
| 42 |
"tests_basis": "MEASURED local python3 -m pytest run, stdlib-only, offline",
|
| 43 |
+
"falsifiability": "registry must be exactly 21; locked-proven set must be exactly 8; PROOF_STATUS must match the dataset verbatim and raises on unknown names; \u039b zero-pins on a zero axis; a tampered receipt fails verify_chain; a sub-floor \u039b halts the governed loop"
|
| 44 |
},
|
| 45 |
"proof_status": {
|
| 46 |
"policy": "mirrored VERBATIM from SZLHOLDINGS/canonical-formulas-v1 (PROVEN/AXIOM/SORRY/CONJECTURE)",
|
| 47 |
"obligation_vs_locked": "a per-formula PROVEN(...) tag is an obligation-level label, NOT membership in the locked-proven canonical set",
|
| 48 |
"locked_proven_count": 8,
|
| 49 |
+
"locked_proven_ids": [
|
| 50 |
+
"F1",
|
| 51 |
+
"F4",
|
| 52 |
+
"F7",
|
| 53 |
+
"F11",
|
| 54 |
+
"F12",
|
| 55 |
+
"F18",
|
| 56 |
+
"F19",
|
| 57 |
+
"F22"
|
| 58 |
+
],
|
| 59 |
"locked_count_theorem": "locked_count_eight (no-axiom, szl-holdings/lutar-lean PROVEN_FORMULAS.md)",
|
| 60 |
+
"f_number_to_registry_mapping": "UNKNOWN \u2014 lutar-lean corpus (>=22 formulas) is a separate numbering; mapping onto these 21 registry entries is NOT asserted here (never fabricated)"
|
| 61 |
},
|
| 62 |
"lambda": {
|
| 63 |
+
"status": "Conjecture 1 (open) \u2014 uniqueness unproven (Uniqueness.lean:120 sorry)",
|
| 64 |
"definition": "weighted geometric mean (D2)",
|
| 65 |
+
"composer_role": "ADVISORY only \u2014 non-compensatory roll-up, NOT proven trust"
|
| 66 |
},
|
| 67 |
"claims": {
|
| 68 |
+
"trained_model": "CLAIMED \u2014 sklearn HistGradientBoostingClassifier, MEASURED, receipted",
|
| 69 |
"reproducible_build": "NOT_CLAIMED",
|
| 70 |
+
"weights_present": "model.joblib (sklearn surrogate; kernel stays weightless)"
|
| 71 |
},
|
| 72 |
"limits": [
|
| 73 |
+
"The trained surrogate is a fast formula IDENTIFIER from trace shape; it does NOT replace the kernel's real evaluators, which remain authoritative for formula identity.",
|
| 74 |
+
"Some formulas share an argument+output observable signature and are confusable from trace shape alone; these blind spots are MEASURED and stated in TRAINING_RECEIPT.json.",
|
| 75 |
"The 21 formulas are pure/no-I/O; the composer performs no network access.",
|
| 76 |
"PROOF_STATUS labels are the dataset's obligation-level declarations, not upgraded here.",
|
| 77 |
"Locked-proven canonical set is fixed at exactly 8 and never inflated.",
|
| 78 |
+
"The composer's \u039b roll-up does not prove or upgrade \u039b, which stays Conjecture 1 (open)."
|
| 79 |
]
|
| 80 |
+
}
|
README.md
CHANGED
|
@@ -6,8 +6,12 @@ tags:
|
|
| 6 |
- proof-status
|
| 7 |
- lean4
|
| 8 |
- lambda-aggregate
|
|
|
|
|
|
|
|
|
|
| 9 |
- doi:10.5281/zenodo.19944926
|
| 10 |
library_name: kernels
|
|
|
|
| 11 |
license: apache-2.0
|
| 12 |
szl-governance:
|
| 13 |
verdict: ADVISORY
|
|
@@ -27,7 +31,7 @@ szl-governance:
|
|
| 27 |
|
| 28 |
</div>
|
| 29 |
|
| 30 |
-
> **
|
| 31 |
|
| 32 |
> **Kernel Hub migration (verified 2026-07-15):** `get_kernel(...)` resolves the first-class [Kernel Hub repo](https://huggingface.co/kernels/SZLHOLDINGS/szl-formulas); `main` and `v1` pin verified revision `39a9fe6fd295f500f30ad7c6ff4cfdf559b48c4a`.
|
| 33 |
|
|
@@ -70,6 +74,60 @@ Mirrors [`canonical-formulas-v1`](https://huggingface.co/datasets/SZLHOLDINGS/ca
|
|
| 70 |
|
| 71 |
Apache-2.0 · © 2026 SZL Holdings · Stephen P. Lutar · ORCID [0009-0001-0110-4173](https://orcid.org/0009-0001-0110-4173).
|
| 72 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 73 |
---
|
| 74 |
|
| 75 |
<sub><b>SZL Holdings honesty footer.</b> Λ = Conjecture 1 (advisory, never a theorem). locked-proven = exactly 8 {F1,F4,F7,F11,F12,F18,F19,F22}. Honesty labels: MEASURED / REPORTED / MODELED / HEURISTIC / UNKNOWN / UNAVAILABLE. Trust never 100% (ceiling 0.97). PROOF_STATUS mirrored verbatim, never inflated. <a href="https://a-11-oy.com">a-11-oy.com</a> · <a href="https://huggingface.co/SZLHOLDINGS">huggingface.co/SZLHOLDINGS</a></sub>
|
|
|
|
| 6 |
- proof-status
|
| 7 |
- lean4
|
| 8 |
- lambda-aggregate
|
| 9 |
+
- sklearn
|
| 10 |
+
- surrogate
|
| 11 |
+
- tabular-classification
|
| 12 |
- doi:10.5281/zenodo.19944926
|
| 13 |
library_name: kernels
|
| 14 |
+
pipeline_tag: tabular-classification
|
| 15 |
license: apache-2.0
|
| 16 |
szl-governance:
|
| 17 |
verdict: ADVISORY
|
|
|
|
| 31 |
|
| 32 |
</div>
|
| 33 |
|
| 34 |
+
> **🟩 Kernel + REAL trained surrogate.** The governance kernel (pure-Python, **stdlib-only**) is UNCHANGED and remains the sole ground truth — an offline replay of the live Alloy formula surface: the 21 canonical formulas of [`canonical-formulas-v1`](https://huggingface.co/datasets/SZLHOLDINGS/canonical-formulas-v1) plus the Codex-Kernel governed-loop composer. Since **surrogate v1** this repo ALSO ships `model.joblib` — a real trained sklearn classifier that identifies WHICH of the 21 formulas produced a given call trace, with **MEASURED** held-out accuracy **0.9709** (21-class). The surrogate never replaces the kernel's real evaluators. No network, no torch, no tensors in the kernel. **Λ uniqueness stays Conjecture 1 (open); the composer's Λ roll-up is ADVISORY only.**
|
| 35 |
|
| 36 |
> **Kernel Hub migration (verified 2026-07-15):** `get_kernel(...)` resolves the first-class [Kernel Hub repo](https://huggingface.co/kernels/SZLHOLDINGS/szl-formulas); `main` and `v1` pin verified revision `39a9fe6fd295f500f30ad7c6ff4cfdf559b48c4a`.
|
| 37 |
|
|
|
|
| 74 |
|
| 75 |
Apache-2.0 · © 2026 SZL Holdings · Stephen P. Lutar · ORCID [0009-0001-0110-4173](https://orcid.org/0009-0001-0110-4173).
|
| 76 |
|
| 77 |
+
|
| 78 |
+
## Trained formula-identifier v1 (MEASURED — see `TRAINING_RECEIPT.json`)
|
| 79 |
+
|
| 80 |
+
A real sklearn `HistGradientBoostingClassifier` trained on **18,900 traces**
|
| 81 |
+
(900 per formula) generated and **labeled by this kernel itself**:
|
| 82 |
+
every sample is produced by calling the REAL `REGISTRY[name]` evaluator, so the label is
|
| 83 |
+
definitionally the producing formula (seed 20260721;
|
| 84 |
+
126 samples re-audited by kernel replay).
|
| 85 |
+
Features are **trace observables only** — argument-shape + the formula's own output
|
| 86 |
+
shape/type/aggregate stats. No formula name is ever leaked into a feature. Registry count
|
| 87 |
+
is read from the kernel (`registry_count()` → **21**) and asserted.
|
| 88 |
+
|
| 89 |
+
| metric | value |
|
| 90 |
+
|---|---|
|
| 91 |
+
| test accuracy (21-class) | **0.9709** |
|
| 92 |
+
| mean per-class recall | **0.9709** |
|
| 93 |
+
|
| 94 |
+
| per-class recall | value |
|
| 95 |
+
|---|---|
|
| 96 |
+
| `bekenstein_cascade` | 1.0000 |
|
| 97 |
+
| `bohr_complementarity_floor` | 0.7778 |
|
| 98 |
+
| `css_ingress_verify` | 1.0000 |
|
| 99 |
+
| `dsse_envelope` | 1.0000 |
|
| 100 |
+
| `fisher_rao_distance` | 0.8889 |
|
| 101 |
+
| `gleason_quantum_lambda` | 1.0000 |
|
| 102 |
+
| `hoeffding_tail` | 1.0000 |
|
| 103 |
+
| `khipu_merkle_root` | 1.0000 |
|
| 104 |
+
| `kitaev_surface_correct` | 1.0000 |
|
| 105 |
+
| `kochen_specker_18vector_witness` | 1.0000 |
|
| 106 |
+
| `lambda_aggregate` | 0.9889 |
|
| 107 |
+
| `lambda_bounded` | 1.0000 |
|
| 108 |
+
| `lambda_homogeneous` | 1.0000 |
|
| 109 |
+
| `madhava_series` | 1.0000 |
|
| 110 |
+
| `pac_bayes_mcallester` | 1.0000 |
|
| 111 |
+
| `pinsker_kl_bound` | 0.8833 |
|
| 112 |
+
| `reed_solomon_singleton` | 1.0000 |
|
| 113 |
+
| `reidemeister_invariant` | 1.0000 |
|
| 114 |
+
| `schur_concave_lambda_two_axis` | 0.8500 |
|
| 115 |
+
| `shor_codeword_distance` | 1.0000 |
|
| 116 |
+
| `two_witness_ks18_soundness` | 1.0000 |
|
| 117 |
+
|
| 118 |
+
**Measured blind spot (stated, never hidden):** `bohr_complementarity_floor` (0.7778), `fisher_rao_distance` (0.8889), `pinsker_kl_bound` (0.8833), `schur_concave_lambda_two_axis` (0.8500) sit below 0.90 recall.
|
| 119 |
+
formulas that share an argument+output OBSERVABLE signature (e.g. several bool-returning axiom checks over similar inputs) are confusable from trace shape alone; the kernel's evaluators remain authoritative for identity Fast identification belongs to the surrogate; the real
|
| 120 |
+
evaluators (the kernel) remain authoritative for formula identity. Λ untouched = Conjecture 1.
|
| 121 |
+
|
| 122 |
+
```python
|
| 123 |
+
import joblib
|
| 124 |
+
clf = joblib.load("model.joblib") # feature spec: TRAINING_RECEIPT.json data.features
|
| 125 |
+
```
|
| 126 |
+
|
| 127 |
+
Re-verify everything: `python scripts/eval.py` (sha256-checks the shipped model against the
|
| 128 |
+
receipt, regenerates the seeded dataset via the in-repo kernel, retrains, and compares the
|
| 129 |
+
21-class accuracy within ±0.02).
|
| 130 |
+
|
| 131 |
---
|
| 132 |
|
| 133 |
<sub><b>SZL Holdings honesty footer.</b> Λ = Conjecture 1 (advisory, never a theorem). locked-proven = exactly 8 {F1,F4,F7,F11,F12,F18,F19,F22}. Honesty labels: MEASURED / REPORTED / MODELED / HEURISTIC / UNKNOWN / UNAVAILABLE. Trust never 100% (ceiling 0.97). PROOF_STATUS mirrored verbatim, never inflated. <a href="https://a-11-oy.com">a-11-oy.com</a> · <a href="https://huggingface.co/SZLHOLDINGS">huggingface.co/SZLHOLDINGS</a></sub>
|
TRAINING_RECEIPT.json
ADDED
|
@@ -0,0 +1,158 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
{
|
| 2 |
+
"artifact": "SZLHOLDINGS/szl-formulas surrogate v1",
|
| 3 |
+
"role": "21-class formula identifier from call-trace observables \u2014 kernel remains ground truth",
|
| 4 |
+
"generator": {
|
| 5 |
+
"script": "scripts/forge.py",
|
| 6 |
+
"seed": 20260721,
|
| 7 |
+
"kernel_version": "0.1.0",
|
| 8 |
+
"kernel_labelled": true,
|
| 9 |
+
"kernel_registry_count": 21,
|
| 10 |
+
"kernel_replay_audited_samples": 126,
|
| 11 |
+
"label_source": "each sample is produced by calling the REAL REGISTRY[name] evaluator; label == producing formula"
|
| 12 |
+
},
|
| 13 |
+
"data": {
|
| 14 |
+
"rows": 18900,
|
| 15 |
+
"n_classes": 21,
|
| 16 |
+
"classes": [
|
| 17 |
+
"bekenstein_cascade",
|
| 18 |
+
"bohr_complementarity_floor",
|
| 19 |
+
"css_ingress_verify",
|
| 20 |
+
"dsse_envelope",
|
| 21 |
+
"fisher_rao_distance",
|
| 22 |
+
"gleason_quantum_lambda",
|
| 23 |
+
"hoeffding_tail",
|
| 24 |
+
"khipu_merkle_root",
|
| 25 |
+
"kitaev_surface_correct",
|
| 26 |
+
"kochen_specker_18vector_witness",
|
| 27 |
+
"lambda_aggregate",
|
| 28 |
+
"lambda_bounded",
|
| 29 |
+
"lambda_homogeneous",
|
| 30 |
+
"madhava_series",
|
| 31 |
+
"pac_bayes_mcallester",
|
| 32 |
+
"pinsker_kl_bound",
|
| 33 |
+
"reed_solomon_singleton",
|
| 34 |
+
"reidemeister_invariant",
|
| 35 |
+
"schur_concave_lambda_two_axis",
|
| 36 |
+
"shor_codeword_distance",
|
| 37 |
+
"two_witness_ks18_soundness"
|
| 38 |
+
],
|
| 39 |
+
"per_class_samples": 900,
|
| 40 |
+
"class_counts": {
|
| 41 |
+
"bekenstein_cascade": 900,
|
| 42 |
+
"bohr_complementarity_floor": 900,
|
| 43 |
+
"css_ingress_verify": 900,
|
| 44 |
+
"dsse_envelope": 900,
|
| 45 |
+
"fisher_rao_distance": 900,
|
| 46 |
+
"gleason_quantum_lambda": 900,
|
| 47 |
+
"hoeffding_tail": 900,
|
| 48 |
+
"khipu_merkle_root": 900,
|
| 49 |
+
"kitaev_surface_correct": 900,
|
| 50 |
+
"kochen_specker_18vector_witness": 900,
|
| 51 |
+
"lambda_aggregate": 900,
|
| 52 |
+
"lambda_bounded": 900,
|
| 53 |
+
"lambda_homogeneous": 900,
|
| 54 |
+
"madhava_series": 900,
|
| 55 |
+
"pac_bayes_mcallester": 900,
|
| 56 |
+
"pinsker_kl_bound": 900,
|
| 57 |
+
"reed_solomon_singleton": 900,
|
| 58 |
+
"reidemeister_invariant": 900,
|
| 59 |
+
"schur_concave_lambda_two_axis": 900,
|
| 60 |
+
"shor_codeword_distance": 900,
|
| 61 |
+
"two_witness_ks18_soundness": 900
|
| 62 |
+
},
|
| 63 |
+
"split": "80/20 stratified",
|
| 64 |
+
"features": [
|
| 65 |
+
"arity",
|
| 66 |
+
"argshape_n",
|
| 67 |
+
"argshape_depth",
|
| 68 |
+
"argshape_is_str",
|
| 69 |
+
"argshape_is_bytes",
|
| 70 |
+
"argshape_is_dict",
|
| 71 |
+
"argshape_is_list",
|
| 72 |
+
"argshape_is_bool",
|
| 73 |
+
"argnum_count",
|
| 74 |
+
"argnum_mean",
|
| 75 |
+
"argnum_std",
|
| 76 |
+
"argnum_min",
|
| 77 |
+
"argnum_max",
|
| 78 |
+
"argnum_frac_zero",
|
| 79 |
+
"outshape_n",
|
| 80 |
+
"outshape_depth",
|
| 81 |
+
"outshape_is_str",
|
| 82 |
+
"outshape_is_bytes",
|
| 83 |
+
"outshape_is_dict",
|
| 84 |
+
"outshape_is_list",
|
| 85 |
+
"outshape_is_bool",
|
| 86 |
+
"outnum_count",
|
| 87 |
+
"outnum_mean",
|
| 88 |
+
"outnum_std",
|
| 89 |
+
"outnum_min",
|
| 90 |
+
"outnum_max",
|
| 91 |
+
"outnum_frac_zero",
|
| 92 |
+
"out_is_bool",
|
| 93 |
+
"out_is_int",
|
| 94 |
+
"out_is_float",
|
| 95 |
+
"out_is_bytes",
|
| 96 |
+
"out_is_dict",
|
| 97 |
+
"out_is_list",
|
| 98 |
+
"out_scalar_logabs"
|
| 99 |
+
],
|
| 100 |
+
"feature_policy": "trace observables ONLY: argument-shape + kernel-output shape/type/aggregate stats; no formula name leaked into features"
|
| 101 |
+
},
|
| 102 |
+
"model": {
|
| 103 |
+
"type": "sklearn.HistGradientBoostingClassifier",
|
| 104 |
+
"params": {
|
| 105 |
+
"max_iter": 300,
|
| 106 |
+
"early_stopping": true,
|
| 107 |
+
"random_state": 20260721
|
| 108 |
+
},
|
| 109 |
+
"file": "model.joblib",
|
| 110 |
+
"sha256": "94cca70dc950fa957c0931ee80240c4369cab0ff8446ffbfedb483c3e2907698"
|
| 111 |
+
},
|
| 112 |
+
"metrics_MEASURED": {
|
| 113 |
+
"test_accuracy_21_class": 0.9709,
|
| 114 |
+
"mean_per_class_recall": 0.9709,
|
| 115 |
+
"per_class_recall": {
|
| 116 |
+
"bekenstein_cascade": 1.0,
|
| 117 |
+
"bohr_complementarity_floor": 0.7778,
|
| 118 |
+
"css_ingress_verify": 1.0,
|
| 119 |
+
"dsse_envelope": 1.0,
|
| 120 |
+
"fisher_rao_distance": 0.8889,
|
| 121 |
+
"gleason_quantum_lambda": 1.0,
|
| 122 |
+
"hoeffding_tail": 1.0,
|
| 123 |
+
"khipu_merkle_root": 1.0,
|
| 124 |
+
"kitaev_surface_correct": 1.0,
|
| 125 |
+
"kochen_specker_18vector_witness": 1.0,
|
| 126 |
+
"lambda_aggregate": 0.9889,
|
| 127 |
+
"lambda_bounded": 1.0,
|
| 128 |
+
"lambda_homogeneous": 1.0,
|
| 129 |
+
"madhava_series": 1.0,
|
| 130 |
+
"pac_bayes_mcallester": 1.0,
|
| 131 |
+
"pinsker_kl_bound": 0.8833,
|
| 132 |
+
"reed_solomon_singleton": 1.0,
|
| 133 |
+
"reidemeister_invariant": 1.0,
|
| 134 |
+
"schur_concave_lambda_two_axis": 0.85,
|
| 135 |
+
"shor_codeword_distance": 1.0,
|
| 136 |
+
"two_witness_ks18_soundness": 1.0
|
| 137 |
+
},
|
| 138 |
+
"blind_spots": {
|
| 139 |
+
"policy": "classes with held-out recall < 0.90 reported honestly",
|
| 140 |
+
"classes": {
|
| 141 |
+
"bohr_complementarity_floor": 0.7778,
|
| 142 |
+
"fisher_rao_distance": 0.8889,
|
| 143 |
+
"pinsker_kl_bound": 0.8833,
|
| 144 |
+
"schur_concave_lambda_two_axis": 0.85
|
| 145 |
+
},
|
| 146 |
+
"statement": "formulas that share an argument+output OBSERVABLE signature (e.g. several bool-returning axiom checks over similar inputs) are confusable from trace shape alone; the kernel's evaluators remain authoritative for identity"
|
| 147 |
+
}
|
| 148 |
+
},
|
| 149 |
+
"environment": {
|
| 150 |
+
"python": "3.12.12",
|
| 151 |
+
"sklearn": "1.9.0",
|
| 152 |
+
"numpy": "2.5.1",
|
| 153 |
+
"host": "replit 2-vCPU container",
|
| 154 |
+
"wall_seconds": 4.3
|
| 155 |
+
},
|
| 156 |
+
"honesty": "Every number above is MEASURED by this run. The surrogate identifies formulas from trace shape; it never replaces the kernel's real evaluators. \u039b untouched = Conjecture 1.",
|
| 157 |
+
"trained_at_utc": "2026-07-21T02:50:06Z"
|
| 158 |
+
}
|
model.joblib
ADDED
|
@@ -0,0 +1,3 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
version https://git-lfs.github.com/spec/v1
|
| 2 |
+
oid sha256:94cca70dc950fa957c0931ee80240c4369cab0ff8446ffbfedb483c3e2907698
|
| 3 |
+
size 3403360
|
scripts/eval.py
ADDED
|
@@ -0,0 +1,27 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
#!/usr/bin/env python3
|
| 2 |
+
"""Re-verify the szl-formulas surrogate: sha256 the shipped model against
|
| 3 |
+
TRAINING_RECEIPT.json, then deterministically regenerate the seeded dataset via
|
| 4 |
+
scripts/forge.py (which resolves the kernel from this repo's own build/ dir) and
|
| 5 |
+
compare re-measured 21-class accuracy to the receipt (tolerance 0.02 across lib
|
| 6 |
+
versions). Run from repo root: python scripts/eval.py"""
|
| 7 |
+
import hashlib, json, subprocess, sys, tempfile, os, shutil
|
| 8 |
+
root = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
|
| 9 |
+
receipt = json.load(open(f"{root}/TRAINING_RECEIPT.json"))
|
| 10 |
+
got = hashlib.sha256(open(f"{root}/model.joblib", "rb").read()).hexdigest()
|
| 11 |
+
want = receipt["model"]["sha256"]
|
| 12 |
+
print(f"model.joblib sha256 {'MATCHES receipt' if got==want else 'MISMATCH — refuse'}: {got[:16]}…")
|
| 13 |
+
if got != want: sys.exit(1)
|
| 14 |
+
with tempfile.TemporaryDirectory() as td:
|
| 15 |
+
os.makedirs(f"{td}/repo/scripts")
|
| 16 |
+
# symlink the kernel build dir so forge.py's in-repo path logic resolves it
|
| 17 |
+
os.symlink(f"{root}/build", f"{td}/repo/build")
|
| 18 |
+
shutil.copy(f"{root}/scripts/forge.py", f"{td}/repo/scripts/forge.py")
|
| 19 |
+
out = subprocess.run([sys.executable, f"{td}/repo/scripts/forge.py"],
|
| 20 |
+
capture_output=True, text=True)
|
| 21 |
+
print(out.stdout[-500:] if out.returncode == 0 else out.stderr[-500:])
|
| 22 |
+
if out.returncode: sys.exit(1)
|
| 23 |
+
re_receipt = json.load(open(f"{td}/repo/scripts/TRAINING_RECEIPT.json"))
|
| 24 |
+
d = abs(re_receipt["metrics_MEASURED"]["test_accuracy_21_class"]
|
| 25 |
+
- receipt["metrics_MEASURED"]["test_accuracy_21_class"])
|
| 26 |
+
print(f"re-measured 21-class accuracy delta vs receipt: {d:.4f} ({'OK ≤0.02' if d<=0.02 else 'FAIL'})")
|
| 27 |
+
sys.exit(0 if d <= 0.02 else 1)
|
scripts/forge.py
ADDED
|
@@ -0,0 +1,254 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
#!/usr/bin/env python3
|
| 2 |
+
"""Forge a REAL trained surrogate for szl-formulas.
|
| 3 |
+
Kernel = ground truth. Surrogate = a 21-class formula IDENTIFIER: given the
|
| 4 |
+
OBSERVABLE trace of a single formula call (argument-shape observables + the
|
| 5 |
+
formula's own output observables, produced by the kernel's REAL evaluators),
|
| 6 |
+
predict WHICH of the 21 canonical formulas produced it. The registry count (21)
|
| 7 |
+
is read from the kernel itself (registry_count()); we assert it == 21 and say so.
|
| 8 |
+
Labels come from the kernel: each sample is generated BY calling the real
|
| 9 |
+
REGISTRY[name] evaluator, so the label is definitionally the producing formula.
|
| 10 |
+
A sample of traces is re-audited by replaying the kernel call and asserting the
|
| 11 |
+
recorded output matches. Seeded, receipted, reproducible."""
|
| 12 |
+
import json, os, random, sys, time, hashlib, platform, math
|
| 13 |
+
_here = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
|
| 14 |
+
if os.path.isdir(os.path.join(_here, "build", "torch-universal")):
|
| 15 |
+
sys.path.insert(0, os.path.join(_here, "build", "torch-universal")) # in-repo run
|
| 16 |
+
else:
|
| 17 |
+
sys.path.insert(0, "/tmp/kernel-probe/szl-formulas/build/torch-universal") # forge-dev run
|
| 18 |
+
import szl_formulas as fx
|
| 19 |
+
import numpy as np
|
| 20 |
+
from sklearn.ensemble import HistGradientBoostingClassifier
|
| 21 |
+
from sklearn.model_selection import train_test_split
|
| 22 |
+
from sklearn.metrics import accuracy_score, recall_score
|
| 23 |
+
import joblib
|
| 24 |
+
|
| 25 |
+
SEED = 20260721
|
| 26 |
+
random.seed(SEED); np.random.seed(SEED)
|
| 27 |
+
T0 = time.time()
|
| 28 |
+
|
| 29 |
+
REG_COUNT = fx.registry_count()
|
| 30 |
+
assert REG_COUNT == 21, f"expected 21 canonical formulas, kernel reports {REG_COUNT}"
|
| 31 |
+
CLASSES = sorted(fx.REGISTRY.keys())
|
| 32 |
+
assert len(CLASSES) == 21
|
| 33 |
+
|
| 34 |
+
# ---- per-formula argument generators (produce VALID args for the REAL kernel) ----
|
| 35 |
+
def _simplex(k):
|
| 36 |
+
v = [random.random() + 1e-3 for _ in range(k)]
|
| 37 |
+
s = sum(v); return [x / s for x in v]
|
| 38 |
+
|
| 39 |
+
def _axes(k):
|
| 40 |
+
return [random.uniform(0.05, 1.0) for _ in range(k)]
|
| 41 |
+
|
| 42 |
+
def gen_args(name):
|
| 43 |
+
if name == "lambda_aggregate":
|
| 44 |
+
k = random.randint(2, 6); ax = _axes(k)
|
| 45 |
+
if random.random() < 0.5:
|
| 46 |
+
return [ax, _simplex(k)]
|
| 47 |
+
return [ax]
|
| 48 |
+
if name == "lambda_homogeneous":
|
| 49 |
+
k = random.randint(2, 5)
|
| 50 |
+
return [random.uniform(0.0, 3.0), _axes(k)]
|
| 51 |
+
if name == "lambda_bounded":
|
| 52 |
+
return [_axes(random.randint(2, 6))]
|
| 53 |
+
if name == "pac_bayes_mcallester":
|
| 54 |
+
return [random.uniform(0.0, 0.5), random.uniform(0.0, 5.0),
|
| 55 |
+
random.randint(10, 5000), random.uniform(0.01, 0.5)]
|
| 56 |
+
if name == "bekenstein_cascade":
|
| 57 |
+
return [random.uniform(0.0, 10.0), random.uniform(0.0, 1e-10)]
|
| 58 |
+
if name == "reidemeister_invariant":
|
| 59 |
+
alphabet = "abAB"
|
| 60 |
+
s = "".join(random.choice(alphabet) for _ in range(random.randint(2, 8)))
|
| 61 |
+
return [s, random.choice(["R1", "R2", "R3"])]
|
| 62 |
+
if name == "khipu_merkle_root":
|
| 63 |
+
n = random.randint(1, 5)
|
| 64 |
+
return [[{"decision_id": f"d{i}", "value": random.randint(0, 100)} for i in range(n)]]
|
| 65 |
+
if name == "dsse_envelope":
|
| 66 |
+
blen = random.randint(1, 24)
|
| 67 |
+
return [bytes(random.randint(0, 255) for _ in range(blen)), f"key-{random.randint(0,9)}"]
|
| 68 |
+
if name == "gleason_quantum_lambda":
|
| 69 |
+
n = random.randint(2, 4)
|
| 70 |
+
return [[[random.uniform(-1, 1) for _ in range(n)] for _ in range(n)]]
|
| 71 |
+
if name == "hoeffding_tail":
|
| 72 |
+
return [random.uniform(0.0, 1.0), random.randint(1, 5000)]
|
| 73 |
+
if name == "pinsker_kl_bound":
|
| 74 |
+
k = random.randint(2, 5); return [_simplex(k), _simplex(k)]
|
| 75 |
+
if name == "fisher_rao_distance":
|
| 76 |
+
k = random.randint(2, 5); return [_simplex(k), _simplex(k)]
|
| 77 |
+
if name == "bohr_complementarity_floor":
|
| 78 |
+
return [random.uniform(0.0, 1.0), random.uniform(0.0, 1.0)]
|
| 79 |
+
if name == "kochen_specker_18vector_witness":
|
| 80 |
+
rows = random.randint(2, 7)
|
| 81 |
+
return [[[1 if random.random() < 0.4 else 0 for _ in range(random.randint(2, 5))] for _ in range(rows)]]
|
| 82 |
+
if name == "two_witness_ks18_soundness":
|
| 83 |
+
return [random.random() < 0.5, random.random() < 0.5]
|
| 84 |
+
if name == "shor_codeword_distance":
|
| 85 |
+
rows = random.randint(1, 5); cols = random.randint(2, 6)
|
| 86 |
+
return [[[random.randint(0, 1) for _ in range(cols)] for _ in range(rows)]]
|
| 87 |
+
if name == "css_ingress_verify":
|
| 88 |
+
payload = bytes(random.randint(0, 255) for _ in range(random.randint(0, 20)))
|
| 89 |
+
env = fx.dsse_envelope(payload, "signer")
|
| 90 |
+
from hashlib import sha256
|
| 91 |
+
commit = sha256(bytes.fromhex(env["payload"]) if env["payload"] else b"").digest()
|
| 92 |
+
# half the time provide the matching root, half a random one
|
| 93 |
+
css_root = commit if random.random() < 0.5 else bytes(random.randint(0, 255) for _ in range(4))
|
| 94 |
+
return [env, css_root]
|
| 95 |
+
if name == "kitaev_surface_correct":
|
| 96 |
+
return [[random.randint(0, 3) for _ in range(random.randint(2, 8))]]
|
| 97 |
+
if name == "reed_solomon_singleton":
|
| 98 |
+
n = random.randint(2, 255); k = random.randint(1, n)
|
| 99 |
+
return [n, k]
|
| 100 |
+
if name == "madhava_series":
|
| 101 |
+
return [random.uniform(-1.0, 1.0), random.randint(1, 60)]
|
| 102 |
+
if name == "schur_concave_lambda_two_axis":
|
| 103 |
+
return [random.uniform(0.0, 1.0), random.uniform(0.0, 1.0)]
|
| 104 |
+
raise KeyError(name)
|
| 105 |
+
|
| 106 |
+
# ---- trace observables (features) — derived ONLY from args + REAL kernel output ----
|
| 107 |
+
def _flatten_num(x):
|
| 108 |
+
"""Yield numeric leaves from an arbitrarily nested arg/output structure."""
|
| 109 |
+
if isinstance(x, bool):
|
| 110 |
+
yield float(x)
|
| 111 |
+
elif isinstance(x, (int, float)):
|
| 112 |
+
yield float(x)
|
| 113 |
+
elif isinstance(x, (bytes, bytearray)):
|
| 114 |
+
for b in x: yield float(b)
|
| 115 |
+
elif isinstance(x, str):
|
| 116 |
+
yield float(len(x))
|
| 117 |
+
elif isinstance(x, dict):
|
| 118 |
+
for v in x.values():
|
| 119 |
+
yield from _flatten_num(v)
|
| 120 |
+
elif isinstance(x, (list, tuple)):
|
| 121 |
+
for v in x:
|
| 122 |
+
yield from _flatten_num(v)
|
| 123 |
+
|
| 124 |
+
def _shape_stats(obj):
|
| 125 |
+
"""Structural stats for a single object: (n_items, depth, is_str, is_bytes, is_dict, is_list, is_bool)."""
|
| 126 |
+
def depth(o):
|
| 127 |
+
if isinstance(o, (list, tuple)) and o:
|
| 128 |
+
return 1 + max(depth(v) for v in o)
|
| 129 |
+
if isinstance(o, dict) and o:
|
| 130 |
+
return 1 + max(depth(v) for v in o.values())
|
| 131 |
+
return 0
|
| 132 |
+
n = 0
|
| 133 |
+
if isinstance(obj, (list, tuple, dict, str, bytes, bytearray)):
|
| 134 |
+
n = len(obj)
|
| 135 |
+
return [float(n), float(depth(obj)),
|
| 136 |
+
float(isinstance(obj, str)), float(isinstance(obj, (bytes, bytearray))),
|
| 137 |
+
float(isinstance(obj, dict)), float(isinstance(obj, (list, tuple))),
|
| 138 |
+
float(isinstance(obj, bool))]
|
| 139 |
+
|
| 140 |
+
def observe(args, out):
|
| 141 |
+
"""Produce a FIXED-LENGTH numeric feature vector from the call trace."""
|
| 142 |
+
arg_leaves = list(_flatten_num(args))
|
| 143 |
+
out_leaves = list(_flatten_num(out))
|
| 144 |
+
def agg(leaves):
|
| 145 |
+
if not leaves:
|
| 146 |
+
return [0.0, 0.0, 0.0, 0.0, 0.0, 0.0]
|
| 147 |
+
a = np.array(leaves, dtype=np.float64)
|
| 148 |
+
finite = a[np.isfinite(a)]
|
| 149 |
+
if finite.size == 0:
|
| 150 |
+
finite = np.array([0.0])
|
| 151 |
+
return [float(finite.size), float(finite.mean()), float(finite.std()),
|
| 152 |
+
float(finite.min()), float(finite.max()),
|
| 153 |
+
float(np.mean(np.abs(finite) < 1e-6))]
|
| 154 |
+
feats = []
|
| 155 |
+
feats += [float(len(args))] # arity
|
| 156 |
+
feats += _shape_stats(args) # arg container shape
|
| 157 |
+
feats += agg(arg_leaves) # arg numeric aggregate
|
| 158 |
+
feats += _shape_stats(out) # output shape
|
| 159 |
+
feats += agg(out_leaves) # output numeric aggregate
|
| 160 |
+
# output-type one-hots (the kernel's real return type is a strong signal)
|
| 161 |
+
feats += [float(isinstance(out, bool)),
|
| 162 |
+
float(isinstance(out, int) and not isinstance(out, bool)),
|
| 163 |
+
float(isinstance(out, float)),
|
| 164 |
+
float(isinstance(out, (bytes, bytearray))),
|
| 165 |
+
float(isinstance(out, dict)),
|
| 166 |
+
float(isinstance(out, (list, tuple)))]
|
| 167 |
+
# magnitude of a scalar output (log-abs), else 0
|
| 168 |
+
if isinstance(out, (int, float)) and not isinstance(out, bool):
|
| 169 |
+
feats += [math.log1p(abs(float(out)))]
|
| 170 |
+
else:
|
| 171 |
+
feats += [0.0]
|
| 172 |
+
return feats
|
| 173 |
+
|
| 174 |
+
FEATURE_NAMES = (
|
| 175 |
+
["arity"]
|
| 176 |
+
+ [f"argshape_{s}" for s in ["n", "depth", "is_str", "is_bytes", "is_dict", "is_list", "is_bool"]]
|
| 177 |
+
+ [f"argnum_{s}" for s in ["count", "mean", "std", "min", "max", "frac_zero"]]
|
| 178 |
+
+ [f"outshape_{s}" for s in ["n", "depth", "is_str", "is_bytes", "is_dict", "is_list", "is_bool"]]
|
| 179 |
+
+ [f"outnum_{s}" for s in ["count", "mean", "std", "min", "max", "frac_zero"]]
|
| 180 |
+
+ ["out_is_bool", "out_is_int", "out_is_float", "out_is_bytes", "out_is_dict", "out_is_list"]
|
| 181 |
+
+ ["out_scalar_logabs"]
|
| 182 |
+
)
|
| 183 |
+
|
| 184 |
+
# ---- generate ----
|
| 185 |
+
PER_CLASS = 900
|
| 186 |
+
X, y, audited = [], [], 0
|
| 187 |
+
sample_bank = {} # name -> list of (args, recorded_out) for audit
|
| 188 |
+
for name in CLASSES:
|
| 189 |
+
for _ in range(PER_CLASS):
|
| 190 |
+
args = gen_args(name)
|
| 191 |
+
out = fx.REGISTRY[name](*args) # REAL kernel evaluator == ground truth label
|
| 192 |
+
X.append(observe(args, out)); y.append(name)
|
| 193 |
+
if len(sample_bank.get(name, [])) < 6:
|
| 194 |
+
sample_bank.setdefault(name, []).append((args, out))
|
| 195 |
+
|
| 196 |
+
# ---- kernel-replay audit: re-call the real evaluator, assert output agrees ----
|
| 197 |
+
def _eq(a, b):
|
| 198 |
+
if isinstance(a, float) or isinstance(b, float):
|
| 199 |
+
try:
|
| 200 |
+
return abs(float(a) - float(b)) <= 1e-9 * max(1.0, abs(float(a)), abs(float(b)))
|
| 201 |
+
except Exception:
|
| 202 |
+
return a == b
|
| 203 |
+
return a == b
|
| 204 |
+
|
| 205 |
+
for name, samples in sample_bank.items():
|
| 206 |
+
for args, recorded in samples:
|
| 207 |
+
replay = fx.REGISTRY[name](*args)
|
| 208 |
+
assert _eq(replay, recorded), f"kernel replay disagreement for {name}: {replay!r} != {recorded!r}"
|
| 209 |
+
audited += 1
|
| 210 |
+
|
| 211 |
+
X = np.array(X, dtype=np.float64); y = np.array(y)
|
| 212 |
+
Xtr, Xte, ytr, yte = train_test_split(X, y, test_size=0.2, random_state=SEED, stratify=y)
|
| 213 |
+
clf = HistGradientBoostingClassifier(random_state=SEED, max_iter=300, early_stopping=True)
|
| 214 |
+
clf.fit(Xtr, ytr)
|
| 215 |
+
pred = clf.predict(Xte)
|
| 216 |
+
acc = accuracy_score(yte, pred)
|
| 217 |
+
per_class_recall = {c: float(recall_score(yte == c, pred == c)) for c in CLASSES}
|
| 218 |
+
# honest blind-spot detection: classes whose recall is materially below the mean
|
| 219 |
+
mean_recall = float(np.mean(list(per_class_recall.values())))
|
| 220 |
+
weak = {c: round(r, 4) for c, r in per_class_recall.items() if r < 0.90}
|
| 221 |
+
|
| 222 |
+
out_dir = os.path.dirname(os.path.abspath(__file__))
|
| 223 |
+
joblib.dump(clf, f"{out_dir}/model.joblib")
|
| 224 |
+
model_sha = hashlib.sha256(open(f"{out_dir}/model.joblib", "rb").read()).hexdigest()
|
| 225 |
+
receipt = {
|
| 226 |
+
"artifact": "SZLHOLDINGS/szl-formulas surrogate v1",
|
| 227 |
+
"role": "21-class formula identifier from call-trace observables — kernel remains ground truth",
|
| 228 |
+
"generator": {"script": "scripts/forge.py", "seed": SEED, "kernel_version": fx.__version__,
|
| 229 |
+
"kernel_labelled": True, "kernel_registry_count": REG_COUNT,
|
| 230 |
+
"kernel_replay_audited_samples": audited,
|
| 231 |
+
"label_source": "each sample is produced by calling the REAL REGISTRY[name] evaluator; label == producing formula"},
|
| 232 |
+
"data": {"rows": int(len(y)), "n_classes": len(CLASSES), "classes": CLASSES,
|
| 233 |
+
"per_class_samples": PER_CLASS,
|
| 234 |
+
"class_counts": {c: int((y == c).sum()) for c in CLASSES},
|
| 235 |
+
"split": "80/20 stratified", "features": FEATURE_NAMES,
|
| 236 |
+
"feature_policy": "trace observables ONLY: argument-shape + kernel-output shape/type/aggregate stats; no formula name leaked into features"},
|
| 237 |
+
"model": {"type": "sklearn.HistGradientBoostingClassifier",
|
| 238 |
+
"params": {"max_iter": 300, "early_stopping": True, "random_state": SEED},
|
| 239 |
+
"file": "model.joblib", "sha256": model_sha},
|
| 240 |
+
"metrics_MEASURED": {"test_accuracy_21_class": round(float(acc), 4),
|
| 241 |
+
"mean_per_class_recall": round(mean_recall, 4),
|
| 242 |
+
"per_class_recall": {k: round(v, 4) for k, v in per_class_recall.items()},
|
| 243 |
+
"blind_spots": {"policy": "classes with held-out recall < 0.90 reported honestly",
|
| 244 |
+
"classes": weak,
|
| 245 |
+
"statement": "formulas that share an argument+output OBSERVABLE signature (e.g. several bool-returning axiom checks over similar inputs) are confusable from trace shape alone; the kernel's evaluators remain authoritative for identity"}},
|
| 246 |
+
"environment": {"python": platform.python_version(), "sklearn": __import__("sklearn").__version__,
|
| 247 |
+
"numpy": np.__version__, "host": "replit 2-vCPU container", "wall_seconds": round(time.time()-T0, 1)},
|
| 248 |
+
"honesty": "Every number above is MEASURED by this run. The surrogate identifies formulas from trace shape; it never replaces the kernel's real evaluators. Λ untouched = Conjecture 1.",
|
| 249 |
+
"trained_at_utc": time.strftime("%Y-%m-%dT%H:%M:%SZ", time.gmtime()),
|
| 250 |
+
}
|
| 251 |
+
with open(f"{out_dir}/TRAINING_RECEIPT.json", "w") as f: json.dump(receipt, f, indent=2)
|
| 252 |
+
print(json.dumps({"acc": receipt["metrics_MEASURED"]["test_accuracy_21_class"],
|
| 253 |
+
"mean_recall": mean_recall, "weak": weak}, indent=2))
|
| 254 |
+
print(f"rows={len(y)} classes={len(CLASSES)} audited={audited} wall={receipt['environment']['wall_seconds']}s")
|