atlas(r1): #393 bounded proof repair — primary-tier arithmetic fixed (RULE 13 + ZERO_SHOT 3 = 16; residues demoted to secondary tags), zero-shot wording narrowed with residual risks, governor-replay terminology qualified, explicit mutation counts; gate PASS
This commit is contained in:
1 parent
70d53fab8c
commit
d2dd136897
4 files changed
+11
-10
No files matched your search
@@ -25,11 +25,11 @@ _2026-09-20. Per-function applicability: which tier each Rune decision belongs t
|
||||
|
||||
## Headline counts
|
||||
|
||||
**RULE/RULE_FIRST: 9 of 16** (6 pure RULE incl. 3 already deterministic; 3 RULE_FIRST with zero-shot/small-LLM residue). **ZERO-SHOT: 4** (rerank, applicability, contradiction, + residues). **SMALL-LLM residue: 3** (typing, failure, tool-routing edges). **FRONTIER: 1** (novel risk). **FUTURE: 1** (model routing). **Custom trained heads: 0 NOW** (adversarial O: demoted to FUTURE, ≤3 highest-volume functions, few-shot only, labels-gated). FUTURE-class rows per 07_qualification: model routing (Q18), custom heads (Q9), training path (Q17) = FUTURE 3.
|
||||
**PRIMARY EXECUTION TIER (exactly one per function; mechanically sums to 16): RULE 13 · ZERO_SHOT_PRETRAINED 3 · SMALL_GENERATIVE 0 · FRONTIER 0.** RULE_FIRST functions (entity, supersession, failure, tool routing) are RULE-primary with zero-shot/small-LLM residue as SECONDARY FALLBACK tags. **SECONDARY/FUTURE TAGS (zero or more per function):** FALLBACK 3 (typing, failure, tool-routing small-LLM edges) · ADVISORY 1 (risk→frontier) · FUTURE_CUSTOM_HEAD ≤3 (labels-gated) · EXPERIMENT (E1–E8). **Custom trained heads: 0 NOW** (adversarial O: demoted to FUTURE, ≤3 highest-volume functions, few-shot only, labels-gated). FUTURE-class rows per 07_qualification: model routing (Q18), custom heads (Q9), training path (Q17) = FUTURE 3.
|
||||
|
||||
## Ladder (re-scoped per adversarial union)
|
||||
|
||||
**TIER 0 — RULE:** exact lookups, state machines, hashes, budgets, ACLs, diffs. Default for 9/16.
|
||||
**TIER 0 — RULE:** exact lookups, state machines, hashes, budgets, ACLs, diffs. PRIMARY for 13/16.
|
||||
**TIER 1 — ZERO-SHOT PRETRAINED:** local NLI (contradiction/supersession/applicability) + local cross-encoder (rerank). No training, no labels, resident, auditable. The ONLY learned tier that survives O and G today.
|
||||
**TIER 2 — SMALL GENERATIVE LOCAL LLM (schema-constrained):** structured-output local model for residue cases (typing, failure-ambiguous, tool-NL, novel risk advisory). Default middle tier per attacks C/K — replaces custom classifiers.
|
||||
**TIER 3 — FRONTIER:** novel composition, genuinely hard cases, tail. Unchanged.
|
||||
|
||||
@@ -36,7 +36,7 @@ _2026-09-20. Synthesis after adversarial union. The hypothesis as stated did not
|
||||
|
||||
| Class | Open/closed out | Semantic ability | Calibration | OOD handling | Latency (local) | Training need | Explainability | Update burden | Authority suitability | Rune applicability |
|
||||
|---|---|---|---|---|---|---|---|---|---|---|
|
||||
| Rule engine | closed | none | n/a (exact) | n/a (explicit) | µs–ms | none | full | trivial | AUTHORITATIVE | default for 9/16 |
|
||||
| Rule engine | closed | none | n/a (exact) | n/a (explicit) | µs–ms | none | full | trivial | AUTHORITATIVE | PRIMARY for 13/16 |
|
||||
| Embedding + threshold | closed | similarity only | none | none | ms | none | low | re-tune | advisory only | dedupe lesson: never sole authority |
|
||||
| Cross-encoder | closed | relevance | threshold-empirical | poor | 5–30ms | none | low | swap model | advisory (CI-gated) | rerank accessory |
|
||||
| NLI classifier | closed + ABSTAIN | entailment triad | threshold-empirical | distance-based | 5–30ms | none | medium (premise shown) | swap model | advisory + governor | contradiction/supersession/applicability |
|
||||
|
||||
+5
-5
@@ -6,7 +6,7 @@ _2026-09-20. Full stage pipeline with four independent evidence arms (arm-1 Jev-
|
||||
|
||||
Jev is real, documented, and vendor-only: TypeSafe AI's "System One" model (launched Sep 15 2026) takes state + typed questions and returns only Choice/Score/Noul decisions — no free text. Its **interface is worth adopting; its numbers are worth nothing** (no independent replication; reference labels LLM-generated; calibration asserted, never demonstrated; its own docs show P(A)+P(not-A)=1.19 incoherence and adversarial steerability). The batched pass was directionally right (ADAPT interface, REJECT dependency) and has now been verified anchor by anchor, with one downgrade (softmax-partition "impossibility" is one preprint's proposal, not construction fact) and one upgrade (confidence DOCUMENTED as margin-like spread statistic — stronger support for #392's score semantics).
|
||||
|
||||
The semantic-micro-kernel hypothesis — deterministic rule → small typed judge → local LLM → frontier, with MODEL INTERPRETS / KERNEL AUTHORISES — **survived in shape and died in substance**: two independent adversarial passes (union: SUCCEEDS 10 · PARTIAL 7 · FAILS 1, plus two novel attacks) killed the trained-narrow-judge middle rung on volume (label starvation: ~7.5k labels/yr across 12 functions), fuel (self-training contamination), calibration (drift without ground truth), openness (closed-world confident failure), correlation (one encoder swap fails all heads same-day), and epistemics (typed outputs launder statistical bets into authorized facts). What the evidence supports is the **re-scoped ladder**: TIER-0 rules (9/16 functions, default) → TIER-1 zero-shot pretrained (local NLI for contradiction/supersession/applicability + local cross-encoder for rerank; no training, immune to starvation and contamination by construction) → TIER-2 schema-constrained small generative LLM (the actual middle tier per attacks C/K) → TIER-3 frontier tail — with a deterministic governor over every transition (fail-closed, per-decision audit records, content-hashed expiring verdicts) and the training path demoted to a LOGGING path until verified-label volume exists. Custom discriminative heads: FUTURE, ≤3 highest-volume functions, few-shot only, labels-gated. Each rung earned by pre-registered measurement on Rune's own eval set — never assumed.
|
||||
The semantic-micro-kernel hypothesis — deterministic rule → small typed judge → local LLM → frontier, with MODEL INTERPRETS / KERNEL AUTHORISES — **survived in shape and died in substance**: two independent adversarial passes (union: SUCCEEDS 10 · PARTIAL 7 · FAILS 1, plus two novel attacks) killed the trained-narrow-judge middle rung on volume (label starvation: ~7.5k labels/yr across 12 functions), fuel (self-training contamination), calibration (drift without ground truth), openness (closed-world confident failure), correlation (one encoder swap fails all heads same-day), and epistemics (typed outputs launder statistical bets into authorized facts). What the evidence supports is the **re-scoped ladder**: TIER-0 rules (13/16 primary) → TIER-1 zero-shot pretrained (local NLI for applicability/contradiction + local cross-encoder for rerank; zero-shot pretrained models avoid Rune-specific label starvation and Rune-self-training contamination IF never fine-tuned on Rune's unverified logs — residual risks remain: pretrained-data contamination, OOD failure, domain shift, calibration drift, correlated model-family failure) → TIER-2 schema-constrained small generative LLM (the actual middle tier per attacks C/K) → TIER-3 frontier tail — with a deterministic governor over every transition (fail-closed, per-decision audit records, content-hashed expiring verdicts) and the training path demoted to a LOGGING path until verified-label volume exists. Custom discriminative heads: FUTURE, ≤3 highest-volume functions, few-shot only, labels-gated. Each rung earned by pre-registered measurement on Rune's own eval set — never assumed.
|
||||
|
||||
Two candidate innovations survived adversarial search with no found prior art (both defensive): **I1 content-hashed expiring verdicts** (judge decisions bound to exact input versions; edits tombstone dependents) and **I2 judge-log exclusion** (judges never train on own logs without independent verification). Both carry explicit falsifiers.
|
||||
|
||||
@@ -14,7 +14,7 @@ Two candidate innovations survived adversarial search with no found prior art (b
|
||||
|
||||
Which semantic decisions can leave the generative LLM without capability loss, and what authority must surround the learned remainder?
|
||||
|
||||
**Answer:** 9 of 16 leave entirely (rules already decide or can). 4 move to zero-shot pretrained judges that need no training. 3 keep a small-generative residue. 1 (novel risk) stays frontier-advised with RULE gates authoritative. The learned remainder is surrounded by: closed outputs + mandatory ABSTAIN/UNKNOWN classes, novelty scoring (distance-to-training, never softmax max), calibration timestamps with auto-demotion on expiry, k≥2 independent signals for auto-act, content-hashed verdicts with expiry, per-decision audit records, per-head kill-switches defaulting to generative fallback, and regular head-count reviews where deletion is celebrated. Full matrices: §29 (06_synthesis.md §§A–D).
|
||||
**Answer (primary execution tier, exactly one per function, mechanically computed — sums to 16):** RULE 13 (incl. the 6 RULE_FIRST functions whose residue is a SECONDARY tag, model routing's current budget/offline gates, and risk's authoritative gates) · ZERO_SHOT_PRETRAINED 3 (rerank, applicability, contradiction) · SMALL_GENERATIVE 0 primary (residue/fallback only — a SECONDARY tag) · FRONTIER 0 primary (advisory only). Secondary/future tags (zero or more per function): FALLBACK (small-LLM residues on typing/failure/tool-routing), ADVISORY (frontier on risk), FUTURE_CUSTOM_HEAD (≤3 functions, labels-gated), EXPERIMENT (E1–E8). The learned remainder is surrounded by: closed outputs + mandatory ABSTAIN/UNKNOWN classes, novelty scoring (distance-to-training, never softmax max), calibration timestamps with auto-demotion on expiry, k≥2 independent signals for auto-act, content-hashed verdicts with expiry, per-decision audit records, per-head kill-switches defaulting to generative fallback, and regular head-count reviews where deletion is celebrated. Full matrices: §29 (06_synthesis.md §§A–D).
|
||||
|
||||
## 3. Rune inward baseline (read-only audit, 2026-09-20)
|
||||
|
||||
@@ -42,11 +42,11 @@ Selective classification (Chow 1970 → SelectiveNet → Deep Gamblers → ReCoV
|
||||
|
||||
## 10. Per-function verdicts (mandate §10/§20/§21)
|
||||
|
||||
Deterministic alternatives FIRST: 7 of 16 RULE_SUFFICIENT/RULE_FIRST outright (typing, task-state, resume, capability, world-state-change, + source-scope as governor turf, + risk gates). Reverse question (what NEEDS generative): novel risk framings, compositional explanations, OOD-abstention dialogues, unseen-API composition — everything else has a RULE core or small-model precedent. Per-function table (16 rows with evidence, consequence, labels): 02_outward/arm3_functions_training_semantics.md §1; applicability rollup: 03_applicability.md. Headline: RULE 9 · ZERO-SHOT 4 · SMALL-LLM residue 3 · FRONTIER 1 · FUTURE 3 (rerank-gated CI promotion path aside, model routing, custom heads, training path) · custom heads 0 NOW.
|
||||
Deterministic alternatives FIRST: 7 of 16 RULE_SUFFICIENT/RULE_FIRST outright (typing, task-state, resume, capability, world-state-change, + source-scope as governor turf, + risk gates). Reverse question (what NEEDS generative): novel risk framings, compositional explanations, OOD-abstention dialogues, unseen-API composition — everything else has a RULE core or small-model precedent. Per-function table (16 rows with evidence, consequence, labels): 02_outward/arm3_functions_training_semantics.md §1; applicability rollup: 03_applicability.md. Headline (PRIMARY EXECUTION TIER, one per function, sums to 16): RULE 13 · ZERO_SHOT_PRETRAINED 3 · SMALL_GENERATIVE 0 · FRONTIER 0. Secondary tags: FALLBACK 3 (typing/failure/tool-routing small-LLM residues), ADVISORY 1 (risk→frontier), FUTURE_CUSTOM_HEAD ≤3, EXPERIMENT E1–E8. (Earlier 9+4+3+1=17 double-counting corrected per repair mandate §A: RULE_FIRST rows counted in both buckets.)
|
||||
|
||||
## 11. Governance (mandate §11 — MODEL INTERPRETS; KERNEL AUTHORISES)
|
||||
|
||||
In-repo precedent PROVEN: ci_event_wait (events wake, Gitea authority verifies, model never authorizes — R8). Named analogues (unread, flagged): ISO-26262 monitor-actuator, OPA/Cedar PDP-vs-PEP, Temporal idempotency, CBF certified envelopes, selective-prediction regulator split. Learned-NEVER-authoritative: irreversible/consequential actions, authority crossings, unrecoverable false accepts. Enforcement fails closed + independently auditable (decision log + deterministic replay). Testable ownership matrix: 06_synthesis.md §D.
|
||||
In-repo precedent PROVEN: ci_event_wait (events wake, Gitea authority verifies, model never authorizes — R8). Named analogues (unread, flagged): ISO-26262 monitor-actuator, OPA/Cedar PDP-vs-PEP, Temporal idempotency, CBF certified envelopes, selective-prediction regulator split. Learned-NEVER-authoritative: irreversible/consequential actions, authority crossings, unrecoverable false accepts. Enforcement fails closed + independently auditable (decision log + fixed-model deterministic execution of the governor over logged inputs — the governor itself is deterministic rule code, per the §26 terminology discipline; bounded statistical judges beneath it are never described as deterministic). Testable ownership matrix: 06_synthesis.md §D.
|
||||
|
||||
## 12. Shared encoder + tiny heads (mandate §12/§25)
|
||||
|
||||
@@ -82,7 +82,7 @@ Six-output table (logit: none; softmax: relative-only + Guo miscalibration; cali
|
||||
|
||||
## 20. Deterministic alternatives first (mandate §20)
|
||||
|
||||
Applied per function (§10): SQL/IDs/timestamps/hashes/schema/state-machine/metadata/parser logic decide 9/16 outright. The learned layer exists ONLY for irreducibly semantic ambiguity (paraphrase openness, entailment relations, relevance ordering, NL→tool residue).
|
||||
Applied per function (§10): SQL/IDs/timestamps/hashes/schema/state-machine/metadata/parser logic are the PRIMARY tier for 13/16 (6 outright + 7 RULE_FIRST/gated whose residue is secondary). The learned layer exists ONLY for irreducibly semantic ambiguity (paraphrase openness, entailment relations, relevance ordering, NL→tool residue).
|
||||
|
||||
## 21. Generative alternative (mandate §21)
|
||||
|
||||
|
||||
@@ -8,7 +8,7 @@ _DRAFT — FINAL-STATE section appended after closeout actions (mandate §32)._
|
||||
- **PRODUCTION_SCHEMA_MUTATION = NONE.** Memory store accessed read-only (recall queries) or via normal `add` for session summaries only. No ALTER, no production-table writes.
|
||||
- **PRODUCTION_RUNTIME_BEHAVIOR_MUTATION = NONE.** No packages installed, no services changed, no cron changes.
|
||||
- **CANONICAL_MEMORY_WRITE = session summaries only** (normal memory-store mechanism; provenance, not production mutation).
|
||||
- **RESEARCH_TOOLING_MUTATION = NONE this tranche** (gate script unchanged; #392 repair's H-extension reused as-is).
|
||||
- **RESEARCH_TOOLING_MUTATION = YES (one):** scripts/research_gate_check.py parse_adversarial_rows extended to accept P17-style letter+number attack keys (needed for the union table's novel attacks; regression-verified on Q domain). Research governance tooling only.
|
||||
- **GITEA_MUTATION:** #393 reopened + R1_DEEP_REQUALIFICATION_STARTED comment; closeout comment + close (pending — FINAL-STATE section). #394 untouched.
|
||||
- **RESEARCH_ARTIFACT_MUTATION:** R-jev-deterministic-routing/ created (00, 01, 02_outward/×3, 03, 04, 05 + 2 verbatim pass files, 06, 07, claims.json, r0/preliminary/saturation, master); batched output preserved byte-for-byte (PRELIMINARY + DISTILLED stub, never patched); registry R row updated at closeout; compendium rebuild noted.
|
||||
- **RESEARCH_RESULT_AFFECTED = NO.**
|
||||
@@ -22,7 +22,8 @@ Any action after the FINAL-STATE section that performs a canonical memory write,
|
||||
|
||||
Closeout sequence executed: mirror → Dolphin select → Gitea closeout (see stale-audit rule; this section is the newest write).
|
||||
|
||||
- **CANONICAL_MEMORY_WRITE = session summaries only** (unchanged from draft; no further production-store writes).
|
||||
- **CANONICAL_MEMORY_WRITE = 1** — the post-closeout project-summary `add` carrying the #393 verdict (importance 0.85). The store DEDUPLICATED it at sim 0.85 against the unrelated RP8/#271 entry #182498 (dedupe_receipt 1496; second finding-G instance; text survives in the receipt + Gitea closeout comment). No further production-store writes.
|
||||
- **SESSION_NOTES_WRITE = 1** — session scratchpad append (non-canonical, session-scoped).
|
||||
- **GITEA_MUTATION (complete):** #393 reopened + R1_DEEP_REQUALIFICATION_STARTED comment (comment 5751); closeout comment posted; issue CLOSED R1_QUALIFIED (R1_FULL); parent #375 note; #394 untouched (verified).
|
||||
- **RESEARCH_ARTIFACT_MUTATION (complete):** R-jev-deterministic-routing/ = 00, 01, 02_outward/×4 (3 arm files + sources.md), 03, 04, 05 + 2 verbatim passes, 06, 07, claims.json (12 claims), r0/preliminary/saturation, master; batched outputs preserved byte-for-byte (PRELIMINARY + DISTILLED stub); registry R row → R1_FULL; compendium rebuild deferred to next scheduled rebuild (noted, consistent with Q-tranche precedent).
|
||||
- **RESEARCH_RESULT_AFFECTED = NO** (adversarial re-scoping happened DURING the tranche, not after closeout).
|
||||
|
||||
Reference in new issue
Block a user